SMT-based Verification of Timed Systems and Software

Roland Kindermann

    Research output: ThesisDoctoral ThesisCollection of Articles

    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.
    Original languageEnglish
    QualificationDoctor's degree
    Awarding Institution
    • Aalto University
    Supervisors/Advisors
    • Niemelä, Ilkka, Supervisor
    • Junttila, Tommi, Advisor
    Publisher
    Print ISBNs978-952-60-5977-8
    Electronic ISBNs978-952-60-5978-5
    Publication statusPublished - 2014
    MoE publication typeG5 Doctoral dissertation (article)

    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

    Fingerprint Dive into the research topics of 'SMT-based Verification of Timed Systems and Software'. Together they form a unique fingerprint.

  • Cite this

    Kindermann, R. (2014). SMT-based Verification of Timed Systems and Software. Aalto University.