PLASMA Lab case studies library
You can access a PLASMA Lab project library containing a selection of case studies and examples of various types. These project are compatible with the latest version of PLASMA Lab.
Use cases
These uses cases have been developed for different projects, some of them using project specific simulators.
- Motion planning (DALI Project)
- Systems of Systems (DANSE Project)
- Fault-tolerant fuel control system – Simulink
- Temperature controller of a pig shed – Simulink
- Multi-lift system – SystemC
- Embedded control system – SystemC
- Train interlocking system – Custom proprietary simulator
- Dynamic Software Architectures – Pi-ADL
Examples
Here you can find several examples demonstrating the different simulators, checkers and some specific algorithms of PLASMA Lab (besides Monte-Carlo methods).
| Example | Simulator(s) | Checker(s) | Algorithm(s) |
|---|---|---|---|
| Dining philosophers | RML (DTMC) | BLTL Observer |
Importance splitting |
| Probabilistic Broadcast protocols | RML (DTMC) | BLTL | |
| Synchronous Leader Election Protocol | RML (DTMC) | BLTL | |
| Hubble | RML (CTMC) | BLTL | |
| Chemical | Bio | BLTL | |
| Genetic oscillator | RML (CTMC), Bio | BLTL | |
| IEEE 802.11 wireless LAN | RML (MDP) | BLTL | Probability estimation for MDPs |
| IEEE 802.3 CSMA/CD | RML (MDP) | BLTL | Probability estimation for MDPs |
| Network virus infection | RML (MDP) | BLTL | Probability estimation for MDPs Reward estimation for MDPs |
| Gossip protocol | RML (MDP) | BLTL | Probability estimation for MDPs Reward estimation for MDPs |
| Choice coordination | RML (MDP) | BLTL | Probability estimation for MDPs Reward estimation for MDPs |
| Self-stabilisation | RML (MDP) | BLTL | Probability estimation for MDPs Reward estimation for MDPs |
| Randomised Consensus Shared Coin Protocol | RML (MDP) | BLTL | Probability estimation for MDPs Reward estimation for MDPs |
| Process partitioning | RML (MDP) | BLTL | |
| Simple chain | RML (DTMC) | Observer | Importance splitting |
