Saturation based analysis of timed models

OData support
Vörös András
Department of Measurement and Information Systems

Today, there is general stereotype that modern IT systems are typically unreliable. However, this assumption cannot be present if we are talking about a system like a nuclear power plant, an aircraft or a pacemaker. The common characteristics of these systems is that strict rules must be followed during the design and the roll-out. Moreover the smallest malfunction is intolerable. It would be desired state when all the IT systems had such availability.

There are many research in this field for a long time ago in order to achive the mentioned error-free operation. This step of the system design process, which examines the correctness of the designed system, is called verification. There are various methods to perform verification such as exhaustive testing, simulation, model checking and theorem proving. During my research I dealt with model checking.

When we use model checkings we have to create a formal model of the examined system based on the given specification. The next step is the formal verification whose aim is to prove the correctness and completeness. The verification algorithm decides whether the model meets the expected requirements. If an error is found, the model has to be fixed and refined. The aim of my work was to extend the timed Petri-net formalism to be able to create more expressive models. Besides this improving some algorithm I have broadened the area where verification can be applied.

In my thesis I have shown how I extended the timed Petri-net formalism with new kind of transitions. Then I studied two saturation [1] based algorithm thoroughly. The first one is Timed Reachability [2], which finds all markings where the model can be at a given finite time. The second one is Earliest Reachability [2], which finds the minimum time when each reachable markings is entered. After that I developed them further to be able to deal with new type of transitions introduced in my thesis. At the end of my work, I made the implementation of the algorithms as well. To do this I used the PetriDotNet framework developed at the Budapest University of Technology and Economics, Department of Measurement and Information Systems.

[1] Gianfranco Ciardo, Gerald Lüttgen, and Radu Siminiceanu. Saturation: an efficient iteration strategy for symbolic state space generation. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 2031, pages 328–342. Springer-Verlag, 2001.

[2] MinWan and Gianfranco Ciardo. Symbolic reachability analysis of integer timed petri nets. In Mogens Nielsen, Antonín Kučera, PeterBro Miltersen, Catuscia Palamidessi, Petr Tůma, and Frank Valencia, editors, SOFSEM 2009: Theory and Practice of Computer Science, volume 5404 of Lecture Notes in Computer Science, pages 595–608. Springer Berlin Heidelberg, 2009.


Please sign in to download the files of this thesis.