Verifying Incomplete Networks of Timed Automata.
Christian Miller, Christoph Scholl, Bernd Becker · MBMV · 2011
Verification of real-time systems – e.g. communication protocols or embedded controllers – is an important task. One method to detect errors is called bounded model checking (BMC). In BMC a system is iteratively unfolded and then transformed into a satisfiability problem. If an appropriate solver finds the k-th instance to be satisfiable, a counterexample for a given safety property has been found. In this paper, we present a novel approach to apply BMC to networks of timed automata (i.e. a system of several interacting subautomata) where parts of the network are unspecified (so-called blackboxes). Here, we would like to answer the question of unrealizability, that is, is there a path of a certain length violating a safety property regardless of the implementation of the blackboxes. Focusing on two prevalent communication models for networks of interacting timed automata, we introduce two methods to solve these types of BMC problems. The first is based on fixed transitions, which in some cases is too coarse of an abstraction. In the second approach we prove unrealizability by introducing universal quantification, yielding more advanced quantified SAT-Modulo-Theory formulas.