Embedded systems are increasingly being deployed in a wide variety of applications. Most, if not all, of these applications involve an electronic controller with discrete behaviour controlling a continuously evolving plant. Because of their hybrid behaviour (discrete and continuous) and reactive behaviour, the formal verification of embedded systems pose new challenges.
In my PhD dissertation, on which this talk is based, proposed are two techniques to verify Linear Hybrid Automata (LHA) models, namely: (a) reachability analysis – where the technique of static program analysis and the theory of abstract interpretation are applied and (b) abstract model checking - where the technique of model checking and the theory of abstract interpretation are synergistically applied. We implemented these techniques resulting in a systematic framework to verify LHA models with respect to properties specified in the language of Computation Tree Logic (CTL). In this framework: (i) an LHA model is encoded in the language of Constraint Logic Programming (CLP), (ii) reachable state space of an LHA is computed as the minimum model of the equivalent CLP encoding. So computed reachable state space forms the basis to do reachability analysis and abstract model checking.
We demonstrate the applicability of the proposed techniques/framework with examples taken from the literature.
