SMT-based Verification of Timed Systems and Software

Julkaistu vain painettuna, saatavuus katso Bibid. Published only in printed form, availability see BibidDefects 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