Formal Methods in System DesignFormal modeling and verication of systems is the set of techniques that employ rigorous mathematical reasoning to analyze properties of a system. Model Checking—pioneered by Clarke, Sifakis and Emerson—is a widely used formal verification technique that, given a formal description of a system (implementation) and a property (specification), systematically checks whether this property holds for a given state of the system model. Three key steps of this framework are the following.
- formal modeling: modeling a system under consideration using mathematically precise syntax that approximate a given system to a desired level of abstraction;
- formal specification: specify the properties of the system using some mathematically precise specification language (typically in formal logic); and
- formal analysis: analyze the formal model with respect to the formal specification and report counter-example in case the system model violates the specification.
Cyber-Physical SystemsCyber-physical systems (CPS) consist of a network of digital and analog systems whose operation is governed by the interactions between the continuous dynamics of the analog subsystem and the real-time switching decisions made by the digital subsystem. A typical CPS may consist of several processors connected with physical systems via sensors and actuators over wired or wireless communication networks. Such systems are increasingly performing safety- critical tasks in modern life, where a design fault or a security vulnerability can be catastrophic. Autonomous vehicles, implantable medical devices, and smart & connected communities are some of the prominent examples that underscore the ubiquity as well as the safety- and security-critical nature of modern CPS.
For more information about formal modeling and verification of cyber-physical systems, we refer the interested reader to the following paper.
Hybrid Automata for Formal Modeling
and Verification of Cyber-Physical Systems.
Shankara Narayanan Krishna and Ashutosh Trivedi.
Journal of the Indian Institute of Science, 2013.