## 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 |