Improved verification of networks of timed automata

Timed Automata (TA) are a de facto modeling standard for systems with time-sensitive prop- erties. A common task is to verify if a given network of TA satisfy a given property for every possible execution of the network. These questions lend themselves to being expressed in Linear Temporal Logics (LTLs), which allows for expressions over atomic propositions that are defined over time positions in N. We build upon the TA solver TACK, which supports properties ex- pressed in the rich Metric Interval Temporal Logic (MITL), and encodes both the TA network and property to be verified into a variant of Linear Temporal Logic, Constraint LTL over clocks (CLTLoc). The produced CLTLoc formula can then be solved by tools such as Zot, which trans- form CLTLoc properties into SMT-LIB2, a standardized SMT solver language with support for BitVector and real-valued logics. We present a novel method that preserves TACK’s encoding of MITL properties while en- coding the Timed Automata network directly into SMT-LIB2, making use of both the BitVector logic and the logic of real-valued functions. Our primary targeted SMT solver is Microsoft’s Z3, which supports many standardized formats, including SMT-LIB2 and has strong support for sev- eral SMT logics. We introduce several optimizations that allow us to significantly outperform the CLTLoc encoding, and correct deficiencies in the original encoding.

Gli Automi temporizzati (TA) sono de facto lo standard di modellazione per sistemi con propri- età dipendenti dal tempo. Un’importante attività è quella di verificare se una data rete di TA soddisfa una data proprietà, per ogni possibile esecuzione della rete. Molte proprietà interassanti si possono esprimere in modo sintetico e efficace in Logica Temporale Lineare (LTL), che perme- tte di predicare su proposizioni atomiche variabili nel tempo. In questa tesi ci basiamo sul TA solver TACK, che supporta proprietà espresse nella logica temporale Metric Interval Temporal Logic (MITL), più espressiva di LTL, e codifica sia la rete TA che la proprietà da verificare in una variante di LTL, Constraint LTL over clocks (CLTLoc). La formula CLTLoc risultante può quindi essere risolta con strumenti di verifica come Zot, che trasformano CLTLoc in SMT-LIB2, un linguaggio standardizzato per solutori SMT con supporto per BitVector e logiche reali. In questa tesi presentiamo un nuovo metodo di verifica che conserva la codifica TACK delle proprietà MITL ma che codifica la rete di TA direttamente in SMT-LIB2, utilizzando sia la logica BitVector che la logica delle funzioni a valore reale. Il nostro principale risolutore SMT mirato è lo Z3 di Microsoft, che supporta molti formati standardizzati, compreso SMT-LIB2 e ha un forte supporto per diverse logiche SMT. Abbiamo introdotto varie ottimizzazioni che ci hanno permesso di migliorare in modo significativo le prestazioni di verifica rispetto alla codifica CLTLoc e di correggere alcune carenze nella codifica originale.