▲
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 counterexample in case the system model violates the specification.
CyberPhysical Systems
Cyberphysical 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 realtime 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 securitycritical nature of modern CPS.For more information about formal modeling and verification of cyberphysical systems, we refer the interested reader to the following paper.

Hybrid Automata for Formal Modeling
and Verification of CyberPhysical Systems.
Shankara Narayanan Krishna and Ashutosh Trivedi.
Journal of the Indian Institute of Science, 2013.