SMT-based Verification of Timed Systems and Software

Loading...
Thumbnail Image
Journal Title
Journal ISSN
Volume Title
School of Science | Doctoral thesis (article-based) | Defence date: 2014-12-09
Checking the digitized thesis and permission for publishing
Instructions for the author
Date
2014
Major/Subject
Mcode
Degree programme
Language
en
Pages
230
Series
Aalto University publication series DOCTORAL DISSERTATIONS, 191/2014
Abstract
Defects in hardware or software can have disastrous consequences. Traditionally, testing has been used to address this threat. While often able to expose bugs, testing can, however, not guarantee that a given system is correct, as has been demonstrated by catastrophic failures of well-tested systems in the past. Verification approaches such as model checking address this shortcoming, not only searching for flaws in a limited set of scenarios, but by trying to prove a system correct, guaranteeing the absence of defects if successful. The main part of this dissertation discusses various topics in the area of symbolic model checking of timed systems. Unlike finite state systems, most commonly used for verification, timed systems allow to faithfully model timing aspects of the verified system. Symbolic model checking methods attempt to efficiently handle large sets of states using concise representa-tions. This work contributes to different areas in the field of symbolic verification of timed systems. Firstly, several different symbolic verification methods are explored: bounded model checking, a timed variant of the IC3 algorithm, timed k-induction, and verification by reduction to finite state model checking. Apart from the reduction approach, a common theme among the methods addressed is that they leverage the power of modern SMT solvers to efficiently verify timed systems. Secondly, this work addresses the symbolic verification of quantitative specifications on the timing of events in a system, made in a PSPACE-verifiable subset of the logic MITL. Thirdly, a new representations of timed systems designed to facilitate symbolic verification is introduced. While not providing the same guarantees as model checking, testing has the advantage that it can usually be performed using the original system instead of a model of the system. The approach of concolic testing aims to combine the advantages of both approaches, executing the system at hand instead of analyzing a model, while at the same time using an SMT solver to guide the executions to maximize coverage. This dissertation evaluates the use of concolic testing for the purpose of differential testing of Java smart card applets.
Description
Supervising professor
Niemelä, Ilkka, Prof., Aalto University, Department of Information and Computer Science, Finland
Thesis advisor
Junttila, Tommi, Dr., Aalto University, Department of Information and Computer Science, Finland
Keywords
verification, model checking, timed systems, bounded model checking, metric interval temporal logic, symbolic model checking, timed automata, k-induction, property directed reachability, IC3 algorithm, concolic testing, differential testing
Other note
Parts
  • [Publication 1]: Kari Kähkönen, Roland Kindermann, Keijo Heljanko, and Ilkka Niemelä. Experimental Comparison of Concolic and Random Testing for Java Card Applets. In Proceedings of Model Checking Software - 17th International SPIN Workshop (SPIN 2010), volume 6349 of Lecture Notes in Computer Science, pages 22–39, Springer, September 2010
  • [Publication 2]: Roland Kindermann, Tommi Junttila and Ilkka Niemelä. Modeling for symbolic analysis of safety instrumented systems with clocks. In Proceedings of the 11th International Conference on Application of Concurrency to System Design (ACSD 2011), pages 185-194, IEEE, June 2011
    DOI: 10.1109/ACSD.2011.29 View at publisher
  • [Publication 3]: Roland Kindermann, Tommi Junttila and Ilkka Niemelä. Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata. In Proceedings of Formal Techniques for Distributed Systems – Joint 14th IFIP WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP WG 6.1 International Conference (FORTE 2012), volume 7273 of Lecture Notes in Computer Science, pages 84–100, Springer, June 2012
  • [Publication 4]: Roland Kindermann, Tommi Junttila and Ilkka Niemelä. SMT-based Induction Methods for Timed Systems. In Proceedings of Formal Modeling and Analysis of Timed Systems (FORMATS 2012), volume 7595 of Lecture Notes in Computer Science, pages 171-187, Springer, September 2012
  • [Publication 5]: Roland Kindermann, Tommi Junttila and Ilkka Niemelä. Bounded Model Checking of an MITL Fragment for Timed Automata. In Proceedings of the 13th International Conference on Application of Concurrency to System Design (ACSD 2013), pages 223-232, IEEE, July 2013.
    DOI: 10.1109/ACSD.2013.25 View at publisher
Citation