Menu Close

Reseña: Formalized timed automata

Buenos días

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Formalized timed automata.

Su autor es [Simon Wimmer] (de la Technische Universität München)

Su resumen es

Timed automata are a widely used formalism for modeling real-time systems, which is employed in a class of successful model check- ers such as UPPAAL. These tools can be understood as trust-multipliers: we trust their correctness to deduce trust in the safety of systems checked by these tools. However, mistakes have previously been made. This par- ticularly regards an approximation operation, which is used by model- checking algorithms to obtain a finite search space. The use of this op- eration left a soundness problem in the tools employing it, which was only discovered years after the first model checkers were devised. This work aims to provide certainty to our knowledge of the basic theory via formalization in Isabelle/HOL: we define the main concepts, formalize the classic decidability result for the language emptiness problem, prove correctness of the basic forward analysis operations, and finally outline how both streams of work can be combined to show that forward analysis with the common approximation operation correctly decides emptiness for the class of diagonal-free timed automata.

El trabajo se presentará en el ITP 2016: Interactive Theorem Proving

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.