Nytt datum: 2021-08-18
Examinator: Bengt Lennartson, Inst för elektroteknik
Opponenter: Sarah Torstensson och Joakim Lönn
Many real-world systems can be modelled as discrete event systems (DESs), which have a number of events and discrete states. When an event occurs, the system transitions from one state to another. Two ways of representing such systems are transition systems and Petri nets. Finding the reachable states in transition systems is a very central problem within DESs, and solving more complex problems often requires finding them. This makes it very interesting to create an efficient reachability algorithm, which this thesis contributes to by re-implementing a Matlab algorithm in C++ and Python. Interesting differences between the implementations in terms of efficiency are observed. Another important problem within DESs is to verify that systems have certain desirable properties. These properties can be described using temporal logic, where logical formulas can specify not only what should be true in the present, but also what should become true in the future. These specifications can then be verified using nuXmv, which is a symbolic model checker. While transition systems are easy to describe in nuXMV code, Petri nets are not. This thesis presents a parser that translates a Petri net description into nuXmv code, which is shown to greatly reduce the code that the user needs to write. This effectively extends nuXmv such that it may be used for formal verification of Petri nets as well.