Keywords

Formal Methods in System Design

Formal 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.

The success of the model checking framework in formal verification of systems is largely due to it being highly automatic—a push-button technology—in comparison to other competing approaches like theorem proving. The counterexamples generated in the model-checking process often are used to automatically refine—known as counterexample-guided abstraction refinement (CEGAR) framework—the model and/or the property and the entire procedure can be repeated and thus removing the need of a very accurate initial model or specification.

Cyber-Physical Systems

Cyber-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.
  

---