Advanced Saturation-based Model Checking of Well-formed Coloured Petri Nets

Vörös, András; Budapest University of Technology and Economics

Darvas, Dániel

Jámbor, Attila

Bartha, Tamás

MFB Hungarian Development Bank Plc. & ARTEMIS JU and the Hungarian National Development Agency (NFÜ) in frame of the R3-COP project

Budapest University of Technology and Economics (BME)

2014-04-07

model checking, saturation, safety-critical system, nuclear power plant, verification, Coloured Petri Net

The failure of safety-critical embedded systems may have catastrophic consequences, therefore their development process requires a strong verification procedure to obtain a high confidence of correctness in the specification and implementation. Formal modelling and model checking provides a rigorous, mathematically precise verification method. Practical embedded systems are typically complex, distributed and asynchronous, thus they need expressive and compact formal models, and efficient model checking approaches. The saturation algorithm has an efficient iteration strategy. Combined with symbolic data structures, it can be used for state space generation and model checking of asynchronous systems. Coloured Petri nets are a good choice for modelling distributed and asynchronous systems, however their integration with saturation has not been solved in the past. In this paper we describe a new approach for applying saturation-based state space generation and model checking to coloured Petri nets. We demonstrate the performance of our new algorithm on the verification of a safety function used in the Reactor Protection System of a nuclear power plant.

angol

info:eu-repo/semantics/article

info:eu-repo/semantics/publishedVersion

application/pdf

https://pp.bme.hu/eecs/article/view/2080

10.3311/PPee.2080

Periodica Polytechnica Electrical Engineering and Computer Science; Vol. 58, No. 1 (2014); 3-13

https://pp.bme.hu/eecs/article/view/2080/6336

https://pp.bme.hu/eecs/article/downloadSuppFile/2080/24

Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access). As soon as the paper is accepted, finally submitted and edited, the npaper will appear in the "OnlineFirst" page of the journal, thus from this point no other internet-based publication is necessary.