Paper Info
Title
A Decomposition Method for the Verification of a Real-Time Safety-Critical Protocol
Abstract
Formal methods, especially model checking techniques, are often used for the verification of the resilience of safety critical systems. The usual complexity of the verification problem in real life systems due to state space explosion and the handling of time dependent behavior demands efficient techniques. In this paper we propose a decomposition approach: the layered structure of the system is exploited to decompose the verification problem to smaller and tractable ones. In addition, the structure of the requirements formalized as the combination of reachability and liveness properties is also exploited to construct simpler verification problems for the model checker. The decomposition approach is demonstrated in case of the verification of a distributed protocol in a SCADA system that shall provide functionality even after the occurrence of a finite number of transient faults.
Year
DOI
Venue
2015
10.1007/978-3-319-23129-7_3
SERENE 2015 Proceedings of the 7th International Workshop on Software Engineering for Resilient Systems - Volume 9274
Field
DocType
Volume
Functional verification,Model checking,Intelligent verification,Computer science,Runtime verification,Formal methods,High-level verification,State space,Reliability engineering,Liveness,Distributed computing
Conference
9274
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
7
3
Name
Order
Citations
PageRank
Tamás Tóth162.56
András Vörös2368.41
Istvan Majzik320123.46