An automated approach to the interpretation of counter-examples

van den Berg, Lionel, Strooper, Paul and Johnston, Wendy (2007). An automated approach to the interpretation of counter-examples. In: , Proceedings of the Workshop on Verification and Debugging (V&D 2006). Workshop on Verification and Debugging (V&D 2006), Seattle, WA, United States, (19-35). 21 August 2006.


Author van den Berg, Lionel
Strooper, Paul
Johnston, Wendy
Title of paper An automated approach to the interpretation of counter-examples
Conference Paper Type Fully Published Paper
Conference name Workshop on Verification and Debugging (V&D 2006)
DOI 10.1016/j.entcs.2006.12.027
Conference location Seattle, WA, United States
Conference dates 21 August 2006
Proceedings title Proceedings of the Workshop on Verification and Debugging (V&D 2006)  (ERA 2012 Listed)    (ERA 2010 Rank C)   Check publisher's open access policy
Journal name Electronic Notes in Theoretical Computer Science  (ERA 2012 Listed)    (ERA 2010 Rank C)   Check publisher's open access policy
Place published Amsterdam, Netherlands
Publisher Elsevier
Publication date 2007
Volume number 174
Issue number 4
ISSN 1571-0661
Start page 19
End page 35
Total pages 17
Collection year 2008
Language eng
Abstract/Summary Model checking is an automatic technique used for the verification of finite systems. A model checker explores the full state space of a given model and checks it against a set of requirements. If a state exists in which a requirement is not satisfied most tools will generate a counter-example. Counter-examples are useful for debugging a model and determining if an error exists in the modelled system. However, they can be difficult for end users to understand and this may limit the take-up of model checking in industry. This paper describes a domain-specific approach to automatically interpreting counter-examples and presenting the results in an intuitive form to the end user. Our research extends previous work on model checking railway signalling control tables with signalling engineers from Queensland Rail.
Subjects 280302 Software Engineering
700102 Application tools and system utilities
E1
Keyword Model checking
counter-example
interpretation
railway signalling
verification
animation
Q-Index Code E1
Q-Index Status Confirmed Code
Institutional Status UQ

 
Versions
Version Filter Type
Citation counts: Scopus Citation Count Cited 1 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Access Statistics: 51 Abstract Views  -  Detailed Statistics
Created: Thu, 10 Apr 2008, 15:07:33 EST by Donna Clark on behalf of School of Information Technol and Elec Engineering