Optimising ordering strategies for symbolic model checking of railway interlockings

Winter, Kirsten (2012). Optimising ordering strategies for symbolic model checking of railway interlockings. In: Tiziana Margaria and Bernhard Steffen, Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies: 5th International Symposium, ISoLA 2012. International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, Heraklion, Crete, Greece, (246-260). 15-18 October 2012. doi:10.1007/978-3-642-34032-1_24

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads

Author Winter, Kirsten
Title of paper Optimising ordering strategies for symbolic model checking of railway interlockings
Conference name International Symposium on Leveraging Applications of Formal Methods, Verification and Validation
Conference location Heraklion, Crete, Greece
Conference dates 15-18 October 2012
Proceedings title Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies: 5th International Symposium, ISoLA 2012   Check publisher's open access policy
Journal name Lecture Notes in Computer Science   Check publisher's open access policy
Series Lecture Notes in Computer Science
Place of Publication Heidelberg, Germany
Publisher Springer
Publication Year 2012
Sub-type Fully published paper
DOI 10.1007/978-3-642-34032-1_24
Open Access Status
ISBN 9783642340321
3642340326
9783642340314
3642340318
ISSN 0302-9743
0302-9743
Editor Tiziana Margaria
Bernhard Steffen
Volume 7610
Start page 246
End page 260
Total pages 15
Collection year 2013
Language eng
Formatted Abstract/Summary
Interlockings implement Railway Signalling Principles which ensure the safe movements of trains along a track system. They are safety critical systems which require a thorough analysis. We are aiming at supporting the safety analysis by automated tools, namely model checkers.

Model checking provides a full state space exploration and is thus intrinsically limited in the problem’s state space. Current research focuses on extending these limits and pushing the boundaries. In our work we investigate possible optimisations for symbolic model checking. Symbolic model checkers exploit a compact representation of the model using Binary Decision Diagram. These structures provide a canonical representation which allows for reductions. The compactness of this data structure and possible reductions are dependent on two orderings: the ordering of variables and the ordering in which sub-structures are manipulated. This paper reports on findings of how a near to optimal ordering can be generated for the domain of interlocking verification.
Q-Index Code C1
Q-Index Status Confirmed Code
Institutional Status UQ

 
Versions
Version Filter Type
Citation counts: Scopus Citation Count Cited 11 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Wed, 10 Oct 2012, 13:36:18 EST by Dr Kirsten Winter on behalf of School of Information Technol and Elec Engineering