2018/06/22 by Claudio Menghi, Marcello M. Bersani, Menghi, Claudio +5
Computer Science · #Formal Methods in Verification #Model-Driven Software Engineering Techniques #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1806.08684
Timed Automata (TA) is de facto a standard modelling formalism to represent\nsystems when the interest is the analysis of their behaviour as time\nprogresses. This modelling formalism is mostly used for checking whether the\nbehaviours of a system satisfy a set of properties of interest. Even if\nefficient model-checkers for Timed Automata exist, these tools are not easily\nconfigurable. First, they are not designed to easily allow adding new Timed\nAutomata constructs, such as new synchronization mechanisms or communication\nprocedures, but they assume a fixed set of Timed Automata constructs. Second,\nthey usually do not support the full Metric Interval Temporal Logic (MITL) and\nrely on a precise semantics for the logic in which the property of interest is\nspecified which cannot be easily modified and customized. Finally, they do not\neasily allow using different solvers that may speed up verification in\ndifferent contexts. This paper presents a novel technique to perform model\nchecking of full Metric Interval Temporal Logic (MITL) properties on TA. The\ntechnique relies on the translation of both the TA and the MITL formula into an\nintermediate Constraint LTL over clocks (CLTLoc) formula which is verified\nthrough an available decision procedure. The technique is flexible since the\nintermediate logic allows the encoding of new semantics as well as new TA\nconstructs, by just adding new CLTLoc formulae. Furthermore, our technique is\nnot bound to a specific solver as the intermediate CLTLoc formula can be\nverified using different procedures.\n