Symbolic model checking for interlocking systems

Winter, Kirsten (2012). Symbolic model checking for interlocking systems. In Francesco Flammini (Ed.), Railway safety, reliability, and security: technologies and systems engineering (pp. 298-315) Hersey, PA, U.S.A.: IGI Global. doi:10.4018/978-1-4666-1643-1.ch013

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 chapter Symbolic model checking for interlocking systems
Title of book Railway safety, reliability, and security: technologies and systems engineering
Place of Publication Hersey, PA, U.S.A.
Publisher IGI Global
Publication Year 2012
Sub-type Chapter in textbook
DOI 10.4018/978-1-4666-1643-1.ch013
ISBN 9781466616431
Editor Francesco Flammini
Chapter number 13
Start page 298
End page 315
Total pages 18
Total chapters 19
Collection year 2013
Language eng
Formatted Abstract/Summary
Model checking is a fully automated technique for the analysis of a model of a system. Due to its degree of automation it is in principle suitable for application in industry but at the same time its scalability is limited. Symbolic model checking is one approach that improves scalability through the use of Binary Decision Diagrams (BDDs) as an internal data structure. This approach allows the user to increase the efficiency by customising the ordering of state variables occurring in the model to be checked. In the domain of railway interlockings represented as control tables, it is found that this task can be supported using an algorithm that has access to the track layout information. In our work we propose optimisation strategies that render symbolic model checking feasible for large scale interlocking systems. Our results yield a verification tool suitable for use in industry.
Q-Index Code BX
Q-Index Status Confirmed Code
Institutional Status UQ

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