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

Automotive CPS

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.