Parallel Model Checking of Asynchronous Systems

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

Abstract

Safety-critical systems require a high degree of assurance of design correctness. The verification of these systems is often based on formal methods, and especially on model checking, which is a widely used approach to investigate the behavior of discrete state models. Model checking examines the requirements of a system based on its mathematical representation using an exhaustive state-space exploration. Petri nets are often used as the high-level formalism to describe the behavior of asynchronous systems and requirements are expressed as CTL temporal logic predicates. Within my thesis work I focused only on system models and requirements captured as Petri nets and CTL predicates, respectively.

Unfortunately, most of the techniques are limited by the state explosion problem: as the complexity of a system increases, the memory and time required to store the combinatorially expanding state space can easily become excessive. To overcome this problem research in this area mainly focuses on symbolic techniques [1]. These approaches store the state space in compact data structures, such as decision diagrams. With this representation it became achievable to store state space over 10^20 states [2].

Furthermore, the period of the model checking is as important as storage requirement. Nevertheless, most of today’s hardware are built with multi-core processors so the need for parallel symbolic techniques is growing to utilize these additional resources. Several promising directions have been investigated to build such algorithms that work on shared memory architectures [3], but most of them ended with limited speed-ups due to the highly sequential manner of symbolic model checking algorithms.

The main aspects of my work is to apply novel synchronization techniques for the parallel symbolic model checking algorithm described in [3] and integrate it into the PetriDotNet [4] framework developed at the Department of Measurement and Information Systems. Besides this I turnd the CTL module of the PetriDotNet framework into parallel so I made a complete parallel model checking module. As part of my work, I measured and compared the different synchronization mechanisms, the parallel algorithm against its sequential implementation.

[1] Ciardo G, Marmorstein R, Siminiceanu R.: The saturation algorithm for symbolic state-space exploration. International Journal on Software Tools for Technology Transfer., 8(1):4-25., 2005.

[2] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, L. J. Hwang: Symbolic model checking: 10^20 states and beyond., Information and Computation 98(2):142-170, 1992.

[3] Ezekiel J, Lüttgen G, Siminiceanu R.: Can saturation be parallelised? On the parallelisation of a symbolic state-space generator. PDMC conference on Formal methods: Applications and technology., 331-346., 2006.

[4] PetriDotNet információs oldal: https://www.inf.mit.bme.hu/research/tools/petridotnet

Downloads

Please sign in to download the files of this thesis.