(2021) A Web Interface for Petri Nets with Transits and Petri Games.
|
Text
GHY21.pdf Download (1MB) | Preview |
Abstract
Developing algorithms for distributed systems is an error-prone task. Formal models like Petri nets with transits and Petri games can prevent errors when developing such algorithms. Petri nets with transits allow us to follow the data flow between components in a distributed system. They can be model checked against specifications in LTL on both the local data flow and the global behavior. Petri games allow the synthesis of local controllers for distributed systems from safety specifications. Modeling problems in these formalisms requires defining extended Petri nets which can be cumbersome when performed textually. In this paper, we present a web interface that allows an intuitive, visual definition of Petri nets with transits and Petri games. The corresponding model checking and synthesis problems are solved directly on a server. In the interface, implementations, counterexamples, and all intermediate steps can be analyzed and simulated. Stepwise simulations and interactive state space generation support the user in detecting modeling errors.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Divisions: | Bernd Finkbeiner (Reactive Systems Group, RSG) |
| Conference: | TACAS Tools and Algorithms for Construction and Analysis of Systems |
| Depositing User: | Jesko Hecking-Harbusch |
| Date Deposited: | 31 Mar 2021 08:14 |
| Last Modified: | 14 Apr 2021 11:08 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/3387 |
Actions
Actions (login required)
 |
View Item |