Introducing time in an industrial application of model-checking

van den Berg, L., Strooper, P. and Winter, K. (2008). Introducing time in an industrial application of model-checking. In: Leue, S. and Merino, P., Lecture Notes in Computer Science ; Formal Methods for Industrial Critical Systems. 12th International Workshop on Formal Methods for Industrial Critical Systems, Berlin, Germany, (56-67). 1-2 July, 2008. doi:10.1007/978-3-540-79707-4_6

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

Author van den Berg, L.
Strooper, P.
Winter, K.
Title of paper Introducing time in an industrial application of model-checking
Conference name 12th International Workshop on Formal Methods for Industrial Critical Systems
Conference location Berlin, Germany
Conference dates 1-2 July, 2008
Proceedings title Lecture Notes in Computer Science ; Formal Methods for Industrial Critical Systems   Check publisher's open access policy
Journal name Formal Methods for Industrial Critical Systems   Check publisher's open access policy
Place of Publication Berlin, Germany
Publisher Springer Verlag
Publication Year 2008
Year available 2008
Sub-type Fully published paper
DOI 10.1007/978-3-540-79707-4_6
Open Access Status DOI
ISBN 978-3-540-79706-7
ISSN 0302-9743
1611-3349
Editor Leue, S.
Merino, P.
Volume 4916
Start page 56
End page 67
Total pages 12
Language eng
Abstract/Summary The safety of many industrial systems is directly related to time. Model checking has been used to verify that safety requirements are met by a model of the system. In many cases, however, time is excluded to limit the state space explosion. Two approaches to include time constraints are either to use model checking for timed systems, or to integrate an explicit model of time using standard model checking. This paper presents a case study using the latter approach. We have worked closely with one of Australia’s largest railway companies, Queensland Rail, on a real industrial environment to produce models to verify the safety of railway interlockings. Our models are written and optimised for the symbolic model checker NuSMV. In this paper we introduce time into our existing models and examine time in the context of level crossings. We also present quantitative data to show the feasibility of the approach.
Subjects E1
080309 Software Engineering
890299 Computer Software and Services not elsewhere classified
Keyword Model checking
Railway interlockings
Real-time system
Q-Index Code E1
Q-Index Status Confirmed Code
Institutional Status UQ

 
Versions
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 0 times in Thomson Reuters Web of Science Article
Scopus Citation Count Cited 4 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Fri, 17 Apr 2009, 22:18:55 EST by Donna Clark on behalf of School of Information Technol and Elec Engineering