Vérification de propriétés temporisées et hybrides: théorie et applications
Dejan Ničković · HAL (Le Centre pour la Communication Scientifique Directe) · 2008
The growth of consumer embedded devices, where digital, analog and software components are often combined together on a single chip, results in an increase of complexity of the design and verification processes. The validation of such analog and mixed-signal systems largely relies on simulation-based techniques combined with often ad-hoc analysis methods. This thesis is motivated by the export of property-based formal techniques to the validation of analog and mixed-signal systems, at their continuous and timed levels of abstraction. Since the formal verification of non-trivial continuous systems remains very difficult, we resort to a lighter validation technique, that is, property-based monitoring.We define signal temporal logic STL as a high-level specification language that allows expressing temporal properties of continuous and timed signals. STL is as an extension of the realtime metric interval temporal logic MITL, where continuous signals are transformed into Boolean ones using numerical predicates, and the temporal relations between them are expressed using standard real-time temporal operators whose atomic propositions correspond to those predicates.We develop two monitoring procedures, offline and incremental, for checking the correctness of simulation traces with respect to STL properties and implement them into a stand alone analog monitoring tool (AMT). The property-based monitoring framework is applied, using the AMT tool, to two real-world case studies, considering properties of a FLASH memory cell and a DDR2 memory interface. We also consider the problem of property-based formal verification of timed systems, and develop a modular translation from MITL formulae with past and future operators to timed automata. The construction that we propose is based on temporal testers, a special class of input/output timed automata that realize the sequential functions defined by the semantics of MITL operators. We first show how every MITL formula can be expressed using six basic temporal operators (three for past and three for future) and show how to build a temporal tester for each of these operators. Temporal testers for arbitrary MITL formulae are obtained by composing these elementary testers. Finally, we develop a procedure for automatic synthesis of controllers from high-level specifications expressed in the bounded fragment of metric temporal logic (MTL). We propose a translation from properties specified in this real-time logic and under bounded variability assumption, into deterministic timed automata to which we apply safety synthesis algorithms to build a controller that satisfies the specification by construction.