Improved Bounded Model Checking of Timed Automata
Timed Automata (TA) are a very popular modeling formalism for systems with time-sensitive properties. A common task is to verify if a network of TA satisfies a given property, usually expressed in Linear Temporal Logic (LTL), or in a subset of Timed Computation Tree Logic (TCTL). In this paper, we build upon the TACK bounded model checker for TA, which supports a signal-based semantics of TA and the richer Metric Interval Temporal Logic (MITL). TACK encodes both the TA network and property into a variant of LTL, Constraint LTL over clocks (CLTLOC). The produced CLTLOC formula can then be solved by tools such as Zot, which transforms CLTLOC properties into the input logics of Satisfiability Modulo Theories (SMT) solvers. We present a novel method that preserves TACK’s encoding of MITL properties while encoding the TA network directly into the SMT solver language, making use of both the BitVector logic and the logic of real arithmetics. We also introduce several optimizations that allow us to significantly outperform the CLTLOC encoding in many practical scenarios.
Wed 19 MayDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 15:00
|Formally Verified Credentials Management for Industrial Control Systems|
FormaliSE 2021Pre-print Media Attached
|Improved Bounded Model Checking of Timed Automata|
Robert L. Smith Politecnico di Milano, Marcello Bersani Politecnico di Milano, Italy, Matteo Rossi Politecnico di Milano, Pierluigi San Pietro Politecnico di MilanoPre-print Media Attached