Abstraction Refinement-Based Verification of Timed Automata
Creators: name: Tóth, Tamás
Publisher: name: Zenodo
Year: 2021

description: Formal methods are mathematical techniques that enable the rigorous specification and verification of hardware and software systems, typically in design time. Formal verification techniques are formal methods for reasoning about the correctness of systems with respect to a formal specification or property. Model checking is an automatic formal verification technique that is based on exhaustive traversal of the design model’s state space. Its main advantage to more conventional verification methods (e.g. testing) is that it is not only able to detect faults in faulty systems, but can also show that a correct system is fault-free. However, a major difficulty in the successful application of model checking to verification of practical systems is its high computational cost: the cardinality of a system’s state space is typically exponential in the size of the input specification describing the system’s behavior, a phenomenon commonly known as state space explosion. In addition, the state space is not necessarily finite, in particular for real-time systems, where continuous variables with time dimension are part of the specification. <br> Therefore, to make the problem more tractable, advanced model checkers rely on symbolic techniques, where, instead of individual states, sets of states are considered during state space traversal; and abstraction, where only parts of the system that are relevant for the requirement are considered. As a result, the abstracted system is a simpler system whose behavior overapproximates that of the original system, therefore, if the abstract system is correct, so is the original one. However, as the abstracted system might admit false negatives, that is, spurious faulty behavior that is not present in the original system, the key challenge is finding the right abstraction granularity. This process can be automated using abstraction refinement techniques: in case of a false negative, the abstraction is refined in a way that excludes the discovered faulty behavior. <br> Our goal is to provide a generic, modular and configurable model checking framework that supports the development and evaluation of abstraction refinement-based algorithms for checking safety properties over different formalisms. In particular, by specific instantiations of our framework, we aim to provide efficient algorithms for the model checking of real-time systems. We focus primarily on classical timed automata with continuous clock variables, a formalism prominently used in the area of model checking real-time systems, and its extension with discrete variables. Moreover, we investigate methods for proving liveness properties of industrial real-time systems with asynchronous message passing. We propose several contributions towards these goals. <br> First, we introduce Theta, a generic, modular and configurable model checking framework for abstraction refinement-based reachability analysis of different formalisms. For the specific case of timed automata with discrete variables, we present a specialization of our framework that enables the combination of various abstraction and refinement strategies for the location reachability problem. <br> Second, we propose an abstraction technique for timed automata based on interpolation for zones. We propose two refinement strategies, both a combination of forward search, backward search and interpolation. We show that our method is competitive in performance with the state of the art. <br> Third, we propose an abstraction technique for timed automata with discrete variables, where refinement is based on controlling the visibility of discrete variables using interpolation for valuations. We demonstrate that our method, combined with methods for the abstraction of clock variables, can achieve a significant reduction in the size of the state space. <br> Fourth, we investigate methods for liveness checking of industrial real-time protocols with asynchronous message passing. We propose the calendar system formalism, and suggest a k-induction based approach for checking liveness properties of such models. For systems with a hierarchical structure in functionality, we propose a decomposition method that can be used to split the original liveness checking problem into more tractable ones.