## Formal Verification of Cyber-Physical Systems using Theorem Proving
Adnan Rashid 1 , Umair Siddique 2 , and Sofine Tahar 2
1 School of Electrical Engineering and Computer Science (SEECS) National University of Sciences and Technology (NUST) Islamabad, Pakistan
2 Department of Electrical and Computer Engineering adnan.rashid@seecs.nust.edu.pk Concordia University, Montreal, Canada
{muh\_sidd,tahar}@ece.concordia.ca
Abstract. Due to major breakthroughs in software and engineering technologies, embedded systems are increasingly being utilized in areas ranging from aerospace and next-generation transportation systems, to smart grid and smart cities, to health care systems, and broadly speaking to what is known as Cyber-Physical Systems (CPS). A CPS is primarily composed of several electronic, communication and controller modules and some actuators and sensors. The mix of heterogeneous underlying smart technologies poses a number of technical challenges to the design and more severely to the verification of such complex infrastructure. In fact, a CPS shall adhere to strict safety, reliability, performance and security requirements, where one needs to capture both physical and random aspects of the various CPS modules and then analyze their interrelationship across interlinked continuous and discrete dynamics. Oftentimes however, system bugs remain uncaught during the analysis and in turn cause unwanted scenarios that may have serious consequences in safety-critical applications. In this paper, we introduce some of the challenges surrounding the design and verification of contemporary CPS with the advent of smart technologies. In particular, we survey recent developments in the use of theorem proving, a formal method, for the modeling, analysis and verification of CPS, and overview some real world CPS case studies from the automotive, avionics and healthtech domains from system level to physical components.
Keywords: Cyber-Physical Systems (CPS), Formal Methods, Theorem Proving, Physical Systems, Hybrid Systems, Performance, Dependability
## 1 Introduction
Cyber-Physical systems (CPS) [74] are engineered systems involving a cyber component that controls the physical components, as shown in Figure 1. The cyber elements include embedded systems and network controllers, which are usually modeled as discrete events. Whereas, the physical components exhibit continuous dynamics, such as the physical motion of a robot in space or the working of an analog circuit, and are commonly modeled using differential equations. CPS are capable of performing two main functionalities (a) constructing the cyber space using intelligent data management, computational and analytical capabilities; and (b) real-time data acquisition from the physical world and information feedback from the cyber space using some advanced connectivity, as depicted in Figure 1. They can be small, such as artificial pancreas, or very large and complex, such as a smart car or smart energy grid. The development of powerful embedded system hardware, low-power sensing and widely deployed communication networks has drastically increased the dependence of system functionality on CPS. CPS are widely used in advanced automotive systems (autonomous vehicles and smart cars), avionics, medical systems and devices, optical systems, industrial process control, smart grids, traffic safety and control, robotics and telecommunication networks, etc. For example, smart (self-driving) cars are considered as a highly complex autonomous CPS composed of over one hundred processors, and an array of sensors and actuators that interact with the external environment, like the road infrastructure and internet.
Fig. 1. Components of a CPS [2]
<details>
<summary>Image 1 Details</summary>
### Visual Description
\n
## Diagram: Cyber-Physical Systems Model
### Overview
The image depicts a triangular diagram representing a model of Cyber-Physical Systems. The triangle's corners are labeled with "Computation", "Communication", and "Control", while the sides are labeled "Cyber", "Physical", and "Systems". The center of the triangle contains the word "Information". The diagram illustrates the interconnectedness of these elements within a cyber-physical system.
### Components/Axes
* **Central Element:** "Information" (located in the center of the triangle)
* **Corners:**
* "Computation" (top center)
* "Communication" (bottom-left)
* "Control" (bottom-right)
* **Sides:**
* "Cyber" (left side, connecting "Computation" and "Information") - Red text
* "Physical" (right side, connecting "Control" and "Information") - Red text
* "Systems" (bottom side, connecting "Communication" and "Control") - Red text
### Detailed Analysis or Content Details
The diagram is a conceptual model and does not contain numerical data or specific values. It visually represents relationships between components. The triangle shape suggests a strong interdependence between the elements. The labels are positioned to indicate the relationships:
* **Computation** is linked to the **Cyber** domain.
* **Communication** is linked to the **Systems** domain.
* **Control** is linked to the **Physical** domain.
* **Information** is central to all three domains.
### Key Observations
The diagram emphasizes that information is the core element connecting the cyber, physical, and systems aspects of a cyber-physical system. The use of a triangle suggests a balanced and integrated relationship between these components. The color red used for the sides ("Cyber", "Physical", "Systems") may indicate their foundational importance.
### Interpretation
This diagram illustrates a foundational model for understanding Cyber-Physical Systems (CPS). CPS are engineered systems that are built from, and depend upon, the tight integration of computation, networking, and physical processes. The diagram highlights that:
* **Cyber aspects** (computation, data processing) are essential for managing and interpreting information.
* **Physical aspects** (control, actuation) are responsible for interacting with the real world.
* **Systems aspects** (communication, coordination) ensure the seamless integration of cyber and physical components.
* **Information** is the lifeblood of the system, flowing between all components and enabling intelligent operation.
The model suggests that a disruption in any one of these areas can impact the entire system. For example, a failure in communication could prevent control signals from reaching the physical components, leading to system malfunction. The diagram is a high-level representation and doesn't delve into the specifics of how these components are implemented or interact, but it provides a useful framework for analyzing and designing CPS.
</details>
The main goals for an efficient design of CPS are to co-design its cyber and physical parts, and to engineer the system of systems involving the intrinsic heterogeneity. Moreover, an increase in the complexity of its various components and the utilization of advanced technologies pose a major challenge for developing a CPS. For example, in the case of smart cars, it is required to develop cost-effective methods ensuring: a) design and analysis (verification) of its var- ious components at different levels of abstraction, i.e., at different systems and software architecture levels; b) analyzing and understanding the interactions of system of systems, e.g., cars' control system and its various components, such as engine, wheel, steering; c) minimizing the cost of the car by ensuring the safety, reliability, performance and stability of the overall system. Thus, these requirements have to be fulfilled for the efficient design and analysis of a CPS.
The analysis of CPS can generally be characterised as of three types, namely, functional, performance and dependability analysis. For example, the functional analysis involves the analysis of the physical, control and signal processing components of CPS. Each of these characteristics also need to consider a hybrid behavior incorporating both continuous and discrete dynamics, e.g., the physical and cyber elements of the underlying system.
Conventionally, CPS are analyzed using paper-and-pencil methods or computerbased numerical and symbolic techniques. Moreover, most of the time is spent on designing the life-cycle of CPS and their physical (dynamical) behaviour needs to be manipulated. However, there is a lack of theoretical foundations for CPS dynamics and compositional theories for the heterogeneous systems in the tools associated with these analyses. Moreover, these analysis methods suffer from their inherent limitations, like human-error proneness, discretization and numerical errors and the usage of unverified simplification algorithms [23] and thus cannot provide absolute accuracy of the corresponding analysis. Due to the safety critical-nature of CPS, the accuracy of their design and analysis is becoming a dire need. For example, the fatal crash of Uber's self-driving car in March 2018 that killed a pedestrian in Tempe, Arizona, USA was found to be caused by some sensor's anomalies [1]. A more rigourous analysis of CPS could have avoided this incident.
Formal methods [44] have been used as a complementary technique for analyzing CPS and thus can overcome the above-mentioned inaccuracy limitations of the analysis. The two most commonly used formal methods are model checking [14] and theorem proving [35]. Model checking is based on developing a statespace based model of the underlying system and formally verifying the properties of interest, specified in temporal logic. It has been used for analyzing several aspects of a CPS [21]. However, this kind of analysis involves the discretization of the continuous dynamical models and thus compromises the accuracy of the corresponding analysis. Moreover, it also suffers from the state-space explosion problem [14]. Theorem proving [35] is a computer based mathematical method that involves developing a mathematical model of the given system in an appropriate logic and the formal verification of the properties of interest based on mathematical reasoning within the sound core of a theorem prover. The involvement of the formal model and its associated formally specified properties along with the sound nature of theorem proving ensures the accuracy and completeness of the analysis. Based on the decidability or undecidability of the underlying logic, e.g., propositional or higher-order logic, theorem proving can be automatic or interactive, respectively.
Many theorem provers, e.g., HOL4 [92], HOL Light [36], Isabelle [69], KeYmaera [73], Coq [19], PVS [68] have been used for the formal analysis (formal verification) of CPS, e,g., formal functional analysis, formal probabilistic and performance analysis, formal dependability analysis, and hybrid analysis. For instance, the KeYmaera theorem prover has been specifically designed for the formal verification of hybrid systems, thus, incorporating both the continuous and discrete dynamics of the underlying system. KeYmaera is based on deductive reasoning and computer algebraic prover technologies. It uses differential dynamic logic for the model implementation and specification of the underlying system, which is a first-order logic. Similarly, HOL Light provides an extensive support of mathematical libraries that have been used for the functional analysis, i.e., the verification of various continuous aspects of CPS, such as control systems, power electronics, electromagnetic, quantum and optical systems. HOL4 and Isabelle theorem provers provide an extensive support for the formal probabilistic and dependability analysis of systems. Likewise, Isabelle and HOL4 have been extensively used for the verification of software components, providing safety and security analysis of the underlying CPS. In this paper, we report these developments that have been done for the modeling, analysis and verification of CPS in these theorem provers.
## 2 Formal Functional Analysis
## 2.1 Verification of Physical Components
Hasan et al. [38] proposed a framework for analyzing the optical waveguides using HOL4. In particular, the authors formally analyzed the eigenvalues for the planar optical waveguides and utilized their proposed framework for analyzing a planar asymmetric waveguide. Afshar et al. [5] developed a formal support for the complex vector analysis using HOL Light and used it to formally verify the law of reflection for the planar waves. Later, the authors used the formalization of complex vectors to formalize the notions of electromagnetic optics [51], which is further used for performing the formal analysis of the resonant cavity enhanced photonic devices.
Siddique et al. [86] provided a formalization of geometrical optics using HOL Light. The authors formalized fundamental concepts about geometrical optics, i.e., ray, free space, optical system and its stability. Finally, they used their proposed formalization to perform the stability analysis of the Fabry-Perot resonator with fiber rod lens [82]. Next, the authors extended their framework by formalizing the ray optics of the cardinal points and utilized it for formally analyzing a thick lens [87] and the optical instrument used to compensate the ametropia of an eye [89]. Moroever, the authors formalized the notion of optical resonators and used it for formally verifying the 2-D microresonator lattice optical filters [88]. Finally, the authors extended their formal support for geometrical optics in HOL Light by performing the formal analysis of the gaussian [90] and periodic [91] optical systems.
As a part of the optics formal verification project [6], Mahmoud et al. [60] provided a support for the formal analysis of the quantum systems using HOL Light. In particular, the authors formalized the infinite dimension linear spaces and used it for formally verifying a quantum beam splitter. Next, the authors used their formalization of linear algebra to formalize the optical quantum circuits, i.e., the flip gate and used it to formally verify the beam splitter and the phase conjugating mirror [61]. Later, the authors also formalized the notion of coherent light, which is a light produced by the laser sources and formally verified its various properties using HOL Light [62]. Based on these findings, Beillahi et al. [15] proposed a framework for the hierarchical verification of the quantum circuit and used it for the formal analysis of a controlled-phase gate and the Shors factoring quantum circuits. Rand et al. [75] proposed a framework implementing the QWIRE quantum circuit language in Coq, which accepts a high-level abstract model of the quantum circuits and allows the verification of their properties using Coq's features such as dependently-typed circuits and proof-carrying code. Liu et al. [54] formalized the theory of Quantum Hoare Logic (QHL) and used it for formally verifying the correctness of a nontrivial quantum algorithm using Isabelle.
## 2.2 Verification of Software Components
The High-Assurance Cyber Military Systems (HACMS) research program [33] was started by the Defense Advanced Research Projects Agency (DARPA) in the USA with an aim of creating a technology for constructing CPS that are resilient against cyber-attacks, i.e., CPS providing an appropriate security and safety properties. One of the major goals of this program is to create a highassurance software for vehicles, ranging from automobiles to military vehicles, such as quadcopters and helicopters. As a part of this project, Cofer et al. [22] proposed a formal approach for constructing a secure airvehicle software to ensure security against cyber attacks using Isabelle. Moreover, the authors applied their proposed approach for formally analyzing the SMACCMcopter, which is a modified commercial quadcopter, and Boeings Unmanned Little Bird (ULB), which is a full-sized optionally-piloted helicopter. Klein et al. [52] presented the formal verification of seL4 microkernel in HOL4, which is a third-generation microkernel of L4 provenance. The authors formally proved that the implementation of the underlying system follows the high-level specification of the kernel behaviour using Isabelle. Moreover, they also verified two vital properties of the microkernel, i.e., 1) the kernel will not perform an unsafe operation; 2) it will never crash.
## 2.3 Verification of Control and Signal Processing Components
Transform methods, such as Laplace, Fourier and z -transforms are widely used for solving dynamical models and performing the frequency domain analysis of systems. Generally, the dynamics of a system in frequency domain are characterized by the transfer function and frequency response, providing a relationship between its input and output and are important properties of the control and signal processing components of a CPS. In this regards, Taqdees et al. [93] formalized the Laplace transform using multivariate calculus theories of HOL Light. Moreover, the authors used their formalization of the Laplace transform for formally verifying the transfer function of the Linear Transfer Converter (LTC) circuit. Next, the authors extended their framework and provided a support to formally reason about the linear analog circuits, such as Sallen-Key low-pass filters [94] by formalizing the system governing laws such as Kirchhoff's Current Law (KCL) and Kirchhoff's Voltage Law (KVL) using HOL Light. Later, Rashid et al. [81] proposed a new formalization of the Laplace transform based on the notion of sets and used it for analyzing the control system of the Unmanned Free-swimming Submersible (UFSS) vehicle [79] and 4Ο soft error crosstalk model [76]. The Laplace transform [49,96] has also been formalized in Isabelle and Coq theorem provers. Similarly, Rashid et al. [77] formalized the Fourier transform in HOL Light and used it to formally analyze an Automobile Suspension System (ASS), an audio equalizer, a drug therapy model and a MEMs accelerometer [78].
To perform the transfer function based analysis of the discrete-time systems, Siddique et al. [84] formalized z -transform using HOL Light and used it for the formal analysis of Infinite Impulse Response (IIR) Digital Signal Processing (DSP) filter. Later, the authors extended their proposed framework by providing the formal support for the inverse z -transform and used it for formally analyzing a switched-capacitor interleaved DC-DC voltage doubler [85]. Beillahi et al. [17] proposed a formalization of signal-flow graph, which is widely used for evaluating the system performance in the form of transfer function, using HOL Light. The authors used their proposed framework for formally analyzing a die design process [16], 1-boost cell interleaved DC-DC, Pulse Width Modulation (PWM) push-pull DC-DC converters [17], Double-coupler Double-ring (DCDR) photonic processor [83], z-source impedance network and PANDA Vernier resonator [18].
Farooq et al. [32] proposed a formal framework for the kinematic analysis of a two-link planar manipulator, which describes a geometrical relationship between the robotic joints and links, and is widely used to capture the motion of the robots. Moreover, the authors performed the formal kinematic analysis of a biped walking robot using HOL Light. Next, Affeldt et al. [4] carried forward this idea and formalized the foundational support for 3D analysis of the robotic manipulators in Coq. The authors used their proposed framework for the kinematic analysis of the SCARA robot manipulator. Wu et al. [97] used HOL4 to formally reason about the forward kinematics of the 3-DOF planar robot manipulator. Similarly, Li et al. [53] provided the formal verification of the Collision-free Motion Planning Algorithm (CFMPA) of Dual-arm Robot (DAR) using HOL4. Walter et al. [95] formally verified a collision-avoidance algorithm for service robots in Isabelle. The authors mainly formalized the safety zone of the robot based on the algorithm and used it to formally verify that the robot will stop upon facing an obstacle, otherwise, it will continue its movement within the safety zone. Recently, Rashid et al. [80] provided the formal modeling and analysis of the 2-DOF robotic cell injection systems using HOL Light.
## 2.4 Formal Hybrid Analysis
Platzer et al. [70] developed an algorithm for the verification of the safety properties of CPS. The authors used the notion of continuous generalization of induction to compute the differential invariants, which do not require solving the differential equations capturing the dynamics of CPS. Moreover, they used their proposed algorithm for formally verifying the collision avoidance properties in car controls and aircraft roundabout maneuvers [71] using KeYmaera. Similarly, Platzer et al. [72] verified the safety, controllability, liveness, and reactivity properties of the European Train Control System (ETCS) protocol using KeYmaera. KeYmaera has also been widely used for the dynamical analysis of various CPS, such as a distributed car control system [59], freeway traffic control [67], autonomous robotic vehicles [66] and industrial airborne collision avoidance system [50]. Recently, Bohrer et al. [20] presented VeriPhy, a verified pipeline for automatically transforming verified models of CPS to verified controller executables. It proves CPS safety at runtime by verified monitors. All these analysis performed using KeYmaera are based on the differential dynamics logic, which captures both the continuous and discrete dynamics of CPS and their interaction. This logic allows the suitable automation of the verification process as well. Similarly, Foster et al. [34] proposed a framework for the verification of CPS based on Unifying Theories of Programming (UTP) and Isabelle/HOL. In particular, the authors provide the implementation of designs, reactive processes, and the hybrid relational calculus, which are important foundational theories for analyzing CPS.
## 3 Formal Probabilistic and Performance Analysis
Hasan et al. [45] proposed a higher-order logic framework for the probabilistic analysis of the systems using HOL4. The authors first formalized the standard uniform random variable [39]. Next, they used this random variable alongside a non-uniform random number generation method to formalize continuous uniform random variables. Finally, the authors used their proposed formalization for the probabilistic analysis of roundoff error in a digital processor [39]. Next, Hasan et al. [41] used HOL4 for the formal verification of the expectation and variance of the discrete random variable and used their expectation theory to formally reason about the Coupon Collectors problem [41]. Later, the authors extended their framework by providing the formal verification of the expectation properties of the continuous random variables, i.e., Uniform, Triangular and Exponential [37]. Next, the authors formalized the indicator random variables using HOL4 and used it for the expected time complexity analysis of various algorithms, i.e., the birthday paradox, the hat-check and the hiring problems [42]. Elleuch et al. [30] used the probability theory of HOL4 to formally reason about the detection properties of Wireless Sensor Networks (WSNs) and a WSN-based monitoring framework [31]. Moreover, the authors conducted the performance analysis of WSNs [29]. Hasan et al. also used their probability theory in HOL4 for conducting the performance analysis of Automatic-repeat-request (ARQ) protocols, i.e., Stop-and-Wait, Go-Back-N and Selective-Repeat protocols [40]. Finally, Hasan et al. [43] formalized the notion of conditional probability and formally verified its classical properties, i.e., Bayes' theorem and total probability law. The authors utilized their formalization for formally analyzing the binary asymmetric channel, which is widely used in communication systems. Mhamdi et al. [63] formalized the Lebesgue integral using HOL4 and used it for formally verifying the Markov and Chebyshev inequalities, and the Weak Law of Large Numbers (WLLN) theorem. Next, the authors built upon Lebesgue integral to formalize the Radon-Nikodym derivative and used it for formalizing the fundamentals of information theory, i.e., Shannon and relative entropies [64]. Later, Mhamdi et al. [65] used the probabilistic analysis support developed in HOL4 to evaluate the security properties of the confidentiality protocols. A library for the formal probabilistic analysis has also been developed in Isabelle. Holzl et al. [47] formalized measure theory with extended real numbers as measure values, in particular, the authors formalized Lebesgue integral, product measures and Fubinis theorem using Isabelle. Eberl at al. [24] developed an inductive compiler, which takes programs in a probabilistic functional language and computes density functions for the probability spaces using Isabelle. Similarly, Holzl et al. [48] proposed a formalization of Markov chains and used it to formally verify the ZeroConf and the Crowds protocols using Isabelle.
## 4 Formal Dependability Analysis
Hasan et al. [46] formalized some fundamental concepts about the reliability theory in HOL4 and used it for formal reliability analysis of reconfigurable memory arrays in the presence of stuck-at and coupling faults. Moreover, the authors performed the reliability analysis of the combinational circuits, such as full adders, comparators and multiplier. Later, Abbasi et al. [3] extended the reliability analysis framework by formally verifying some statistical properties, i.e., second moment and variance and other reliability concepts, i.e., survival, hazard and fractile functions. The authors utilized their proposed framework for formally analyzing the essential electronic and electrical system components.
Liu et al. [56] proposed a framework to reason about the finite-state discretetime Markov chains using HOL4 and formally verified some of its properties such as joint and steady-state probabilities, and reversibility. The authors utilized their proposed framework to formally analyze a binary communication channel and an automatic mail quality measurement protocol [58]. Next, the authors formalized the discrete-time Markov reward models and used it to formally reason about the memory contention problem of a multi-processor system [57]. Later, the authors proposed a framework to formally reason about the properties of the Hidden Markov Models (HMMs) such as joint probabilities and formally analyzed a DNA sequence [55].
Ahmad et al. [9] developed a higher-order logic based framework for the formal dependability analysis using probability theory of HOL4. The proposed analysis provides the failure characteristics of the systems, i.e., reliability, availability, maintainability, etc. The authors formalized the Reliability Block Diagrams (RBD) [11], which are the graphical representations providing the functional behaviour of a system modules and their interconnections. The proposed formalization of RBD has been used for formally analyzing a simple oil and gas pipeline, a generic Virtual Data Center (VDC) [13], Reliable Multi-Segment Transport (RMST) data transport, Event to Sink Reliable Transport (ESRT) protocols [12] and Logistics Service Supply Chains (LSSCs) [10]. Similarly, Ahmad et al. [7] proposed a framework for the formal fault tree analysis using HOL4. The authors formalized the fault tree gates, i.e., AND, OR, NAND, NOR, XOR and NOT and formally verified their generic expressions for probabilities failures. Moreover, their proposed framework was used to perform the fault tree analysis of a solar array, which is used as a major source of power in the Dong Fang Hong-3 (DFH-3) satellite [7] and a communication gateway software for the next generation Air Traffic Management System (ATMS) [8].
Elderhalli et al. [26] developed a higher-order logic based framework for the formal dynamic dependability analysis using HOL4. The proposed analysis provides the dynamic failure characteristics of the systems, i.e., dynamic reliability and fault trees, etc. The authors formalized the Dynamic Fault Trees (DFTs) [25] and Dynamic Reliability Block Diagrams (DRBD) [27] using HOL4. Moreover, they used their proposed formalization for formally analyzing the Drive-by-wire System (DBW), a Shuffle-exchange Network (SEN) and Cardiac Assist System (CAS) [28].
## 5 Theorem Proving Support for CPS
Table 1 summarizes the formal libraries that are available in various theorem provers for performing the formal analysis of CPS. For example, the formal support for the dependability analysis of systems is only available in HOL4. Similarly, the libraries to formally reason about robotics and software components are available in most of the theorem provers. KeyMaera provides a support for formally analyzing the hybrid systems. Moreover, HOL4 and Isabelle theorem provers have a quite dense library for probabilistic and performance analyses of systems. Similarly, the transform methods are partially available in Isabelle, Coq and HOL4 theorem provers, i.e., only the Laplace transform is formalized in these theorem provers. However, HOL Light contains formal libraries for most of the transform methods, i.e., Laplace, Fourier and z -transforms. Also, the formal library for analyzing the optical systems is only available in HOL Light.
Table 1: Libraries for Formal Analysis in Major Theorem Provers
<details>
<summary>Image 2 Details</summary>
### Visual Description
\n
## Data Table: Analysis/Theorem Provers Capabilities
### Overview
This image presents a data table comparing the capabilities of several theorem provers (HOL4, HOL light, Isabelle/HOL, Coq, PVS, and Keymaera) across different types of analysis. The table uses checkmarks to indicate which theorem provers support each analysis type.
### Components/Axes
* **Rows:** Represent different types of analysis: Transform Methods, Probabilistic Analysis, Performance Analysis, Dependability Analysis, Hybrid Systems, Optical Systems, Quantum Systems, Robotic Systems, and Software Components.
* **Columns:** Represent different theorem provers: HOL4, HOL light, Isabelle/HOL, Coq, PVS, and Keymaera.
* **Cells:** Contain a checkmark (β) if the corresponding theorem prover supports the corresponding analysis type, and are empty otherwise.
### Detailed Analysis or Content Details
Here's a reconstruction of the data table's content:
| Analysis/Theorem Provers | HOL4 | HOL light | Isabelle/HOL | Coq | PVS | Keymaera |
|---|---|---|---|---|---|---|
| Transform Methods | β | β | β | β | | |
| Probabilistic Analysis | β | | β | | | |
| Performance Analysis | β | | β | | | |
| Dependability Analysis | β | | | | | |
| Hybrid Systems | | | | | | β |
| Optical Systems | | β | | | | |
| Quantum Systems | | β | β | β | | |
| Robotic Systems | β | β | β | β | β | β |
| Software Components | β | β | β | β | | β |
**Specific Observations:**
* **HOL4:** Supports Transform Methods, Probabilistic Analysis, Performance Analysis, Dependability Analysis, and Robotic/Software Components.
* **HOL light:** Supports Transform Methods, Optical Systems, Quantum Systems, and Robotic/Software Components.
* **Isabelle/HOL:** Supports Transform Methods, Probabilistic Analysis, Performance Analysis, Quantum Systems, Robotic Systems, and Software Components.
* **Coq:** Supports Transform Methods, Quantum Systems, and Robotic/Software Components.
* **PVS:** Supports Transform Methods and Robotic Systems.
* **Keymaera:** Supports Hybrid Systems and Robotic/Software Components.
### Key Observations
* Robotic Systems is the most widely supported analysis type, supported by all six theorem provers.
* Hybrid Systems is only supported by Keymaera.
* Optical Systems is only supported by HOL light.
* Dependability Analysis is only supported by HOL4.
* Transform Methods is supported by HOL4, HOL light, Isabelle/HOL, and Coq.
### Interpretation
The data suggests a varying degree of specialization among the theorem provers. HOL4 appears to be a versatile tool for a range of analyses, while HOL light excels in Optical and Quantum Systems. Isabelle/HOL offers broad support, particularly in areas like probabilistic and performance analysis. Coq is strong in Transform Methods and Quantum Systems. PVS is more limited in scope, focusing on Transform Methods and Robotic Systems. Keymaera is unique in its support for Hybrid Systems.
The table highlights the trade-offs between breadth and depth of capabilities. A theorem prover like HOL4 might be a good starting point for a variety of analyses, while a more specialized tool like Keymaera might be necessary for specific applications like Hybrid Systems verification. The choice of theorem prover will depend on the specific requirements of the analysis task.
</details>
| Analysis/Theorem Provers | HOL4 | HOL light | Isabelle/HOL | Coq | PVS | Keymaera |
|----------------------------|--------|-------------|----------------|-------|-------|------------|
| Transform Methods | 3 | 3 | 3 | 3 | | |
| Probabilistic Analysis | 3 | | 3 | | | |
| Performance Analysis | 3 | | 3 | | | |
| Dependability Analysis | 3 | | | | | |
| Hybrid Systems | | | | | | 3 |
| Optical Systems | | 3 | | | | |
| Quantum Systems | | 3 | 3 | 3 | | |
| Robotic Systems | 3 | 3 | 3 | | 3 | 3 |
| Software Components | 3 | 3 | 3 | | 3 | 3 |
## 6 Conclusion
CPS are highly complex systems composed of actuators, sensors, and several electronic, communication and controller modules, and exhibit both the continuous and discrete dynamics. Due to the safety critical-nature of CPS, their accurate analysis is of utmost importance. This paper surveys some of the efforts that have been done regarding the formal verification of CPS using theorem proving by highlighting the aspects of CPS that have been verified using different theorem provers. In this regard, only one dedicated theorem prover, KeYmaera, has been developed for analyzing hybrid systems. However, we need to develop dedicated formal libraries in other theorem provers that can support the analysis of hybrid systems, i.e., incorporating the interlinked discrete and continuous-time features of a CPS simultaneously.
## References
1. https://arstechnica.com/tech-policy/2018/05/report-software-bug-ledto-death-in-ubers-self-driving-crash/?amp=1 (2018)
2. https://www.2b1stconsulting.com/cyber-physical-systems-cps/ (2020)
3. Abbasi, N., Hasan, O., Tahar, S.: An Approach for Lifetime Reliability Analysis using Theorem Proving. Journal of Computer and System Sciences 80(2), 323-345 (2014)
4. Affeldt, R., Cohen, C.: Formal Foundations of 3D Geometry to Model Robot Manipulators. In: Certified Programs and Proofs. pp. 30-42. ACM (2017)
5. Afshar, S.K., Aravantinos, V., Hasan, O., Tahar, S.: Formalization of Complex Vectors in Higher-order Logic. In: Intelligent Computer Mathematics. LNCS, vol. 8543, pp. 123-137. Springer (2014)
6. Afshar, S.K., Siddique, U., Mahmoud, M.Y., Aravantinos, V., Seddiki, O., Hasan, O., Tahar, S.: Formal Analysis of Optical Systems. Mathematics in Computer Science 8(1), 39-70 (2014)
7. Ahmad, W., Hasan, O.: Towards Formal Fault Tree Analysis using Theorem Proving. In: Intelligent Computer Mathematics. LNCS, vol. 9150, pp. 39-54. Springer (2015)
8. Ahmad, W., Hasan, O.: Formalization of Fault Trees in Higher-order Logic: A Deep Embedding Approach. In: Dependable Software Engineering: Theories, Tools, and Applications. LNCS, vol. 9984, pp. 264-279. Springer (2016)
9. Ahmad, W., Hasan, O., Tahar, S.: Formal Dependability Modeling and Analysis: A Survey. In: Intelligent Computer Mathematics. LNCS, vol. 9791, pp. 132-147. Springer (2016)
10. Ahmad, W., Hasan, O., Tahar, S., Hamdi, M.: Towards Formal Reliability Analysis of Logistics Service Supply Chains using Theorem Proving. In: Implementation of Logics. pp. 111-121 (2015)
11. Ahmad, W., Hasan, O., Tahar, S., Hamdi, M.S.: Towards the Formal Reliability Analysis of Oil and Gas Pipelines. In: Intelligent Computer Mathematics. LNCS, vol. 8543, pp. 30-44. Springer (2014)
12. Ahmed, W., Hasan, O., Tahar, S.: Formal Reliability Analysis of Wireless Sensor Network Data Transport Protocols using HOL. In: Wireless and Mobile Computing, Networking and Communications. pp. 217-224. IEEE (2015)
13. Ahmed, W., Hasan, O., Tahar, S.: Formalization of Reliability Block Diagrams in Higher-order Logic. Journal of Applied Logic 18, 19-41 (2016)
14. Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT press (2008)
15. Beillahi, S.M., Mahmoud, M.Y., Tahar, S.: Hierarchical verification of quantum circuits. In: NASA Formal Methods Symposium. LNCS, vol. 9690, pp. 344-352. Springer (2016)
16. Beillahi, S.M., Siddique, U., Tahar, S.: Towards the Application of Formal Methods in Process Engineering. Fun With Formal Methods pp. 1-11 (2014)
17. Beillahi, S.M., Siddique, U., Tahar, S.: Formal Analysis of Power Electronic Systems. In: Formal Methods and Software Engineering. LNCS, vol. 9407, pp. 270-286. Springer (2015)
18. Beillahi, S.M., Siddique, U., Tahar, S.: Formal Analysis of Engineering Systems Based on Signal-Flow-Graph Theory. In: Numerical Software Verification. LNCS, vol. 10152, pp. 31-46. Springer (2016)
19. Bertot, Y., CastΒ΄ eran, P.: Interactive Theorem Proving and Program Development: CoqArt: the Calculus of Inductive Constructions. Springer Science & Business Media (2013)
20. Bohrer, B., Tan, Y.K., Mitsch, S., Myreen, M.O., Platzer, A.: VeriPhy: Verified Controller Executables from Verified Cyber-physical System Models. In: Programming Language Design and Implementation. pp. 617-630 (2018)
21. Clarke, E.M., Zuliani, P.: Statistical Model Checking for Cyber-physical Systems. In: Automated Technology for Verification and Analysis. LNCS, vol. 6996, pp. 1-12. Springer (2011)
22. Cofer, D., Gacek, A., Backes, J., Whalen, M.W., Pike, L., Foltzer, A., Podhradsky, M., Klein, G., Kuz, I., Andronick, J., et al.: A Formal Approach to Constructing Secure Air Vehicle Software. Computer 51(11), 14-23 (2018)
23. DurΒ΄ an, A.J., PΒ΄ erez, M., Varona, J.L.: Misfortunes of a Mathematicians' Trio using Computer Algebra Systems: Can We Trust? CoRR abs/1312.3270 (2013)
24. Eberl, M., H¨ olzl, J., Nipkow, T.: A Verified Compiler for Probability Density Functions. In: European Symposium on Programming Languages and Systems. pp. 80104. Springer (2015)
25. Elderhalli, Y., Ahmad, W., Hasan, O., Tahar, S.: Probabilistic Analysis of Dynamic Fault Trees using HOL Theorem Proving. Journal of Applied LogicsIfCoLog Journal of Logics and their Applications 6(3) (2019)
26. Elderhalli, Y., Hasan, O., Ahmad, W., Tahar, S.: Formal Dynamic Fault Trees Analysis using an Integration of Theorem Proving and Model Checking. In: NASA Formal Methods Symposium. LNCS, vol. 10811, pp. 139-156. Springer (2018)
27. Elderhalli, Y., Hasan, O., Tahar, S.: A Formally Verified Algebraic Approach for Dynamic Reliability Block Diagrams. In: Formal Methods and Software Engineering. pp. 253-269. Springer (2019)
28. Elderhalli, Y., Hasan, O., Tahar, S.: A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving. IEEE Access 7, 136176-136192 (2019)
29. Elleuch, M., Hasan, O., Tahar, S., Abid, M.: Towards the Formal Performance Analysis of Wireless Sensor Networks. In: Enabling Technologies: Infrastructure for Collaborative Enterprises. pp. 365-370. IEEE (2013)
30. Elleuch, M., Hasan, O., Tahar, S., Abid, M.: Formal Probabilistic Analysis of Detection Properties in Wireless Sensor Networks. Formal Aspects of Computing 27(1), 79-102 (2015)
31. Elleuch, M., Hasan, O., Tahar, S., Abid, M.: Formal Probabilistic Analysis of a WSN-Based Monitoring Framework for IoT Applications. In: Formal Techniques for Safety-Critical Systems. CCIS, vol. 694, pp. 93-108. Springer (2016)
32. Farooq, B., Hasan, O., Iqbal, S.: Formal Kinematic Analysis of the Two-link Planar Manipulator. In: Formal Methods and Software Engineering. LNCS, vol. 8144, pp. 347-362. Springer (2013)
33. Fisher, K., Launchbury, J., Richards, R.: The HACMS Program: using Formal Methods to Eliminate Exploitable Bugs. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences 375(2104), 20150401 (2017)
34. Foster, S., Woodcock, J.: Towards Verification of Cyber-Physical Systems with UTP and Isabelle/HOL. In: Concurrency, Security, and Puzzles, LNCS, vol. 10160, pp. 39-64. Springer (2017)
35. Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press (2009)
36. Harrison, J.: HOL Light: A Tutorial Introduction. In: Formal Methods in Computer-Aided Design. LNCS, vol. 1166, pp. 265-269. Springer (1996)
37. Hasan, O., Abbasi, N., Akbarpour, B., Tahar, S., Akbarpour, R.: Formal Reasoning about Expectation Properties for Continuous Random Variables. In: Formal Methods. LNCS, vol. 5850, pp. 435-450. Springer (2009)
38. Hasan, O., Afshar, S.K., Tahar, S.: Formal Analysis of Optical Waveguides in HOL. In: Theorem Proving in Higher Order Logics. LNCS, vol. 5674, pp. 228-243. Springer (2009)
39. Hasan, O., Tahar, S.: Formalization of the Standard Uniform Random Variable. Theoretical Computer Science 382(1), 71-83 (2007)
40. Hasan, O., Tahar, S.: Performance Analysis of ARQ Protocols using a Theorem Prover. In: Performance Analysis of Systems and Software. pp. 85-94. IEEE (2008)
41. Hasan, O., Tahar, S.: Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables. Journal of Automated Reasoning 41(3-4), 295-323 (2008)
42. Hasan, O., Tahar, S.: Formally Analyzing Expected Time Complexity of Algorithms Using Theorem Proving. Journal of Computer Science and Technology 25(6), 1305-1320 (2010)
43. Hasan, O., Tahar, S.: Reasoning about Conditional Probabilities in a Higher-orderlogic Theorem Prover. Journal of Applied Logic 9(1), 23-40 (2011)
44. Hasan, O., Tahar, S.: Formal Verification Methods. Encyclopedia of Information Science and Technology, IGI Global Publication pp. 7162-7170 (2015)
45. Hasan, O., Tahar, S.: Formalized Probability Theory and Applications using Theorem Proving. IGI Global (2015)
46. Hasan, O., Tahar, S., Abbasi, N.: Formal Reliability Analysis using Theorem Proving. IEEE Transactions on Computers 59(5), 579-592 (2010)
47. H¨ olzl, J., Heller, A.: Three Chapters of Measure Theory in Isabelle/HOL. In: Interactive Theorem Proving. pp. 135-151. Springer (2011)
48. H¨ olzl, J., Nipkow, T.: Interactive Verification of Markov Chains: Two Distributed Protocol Case Studies. arXiv preprint arXiv:1212.3870 (2012)
49. Immler, F.: Laplace Transform Archive of Formal Proofs. https://www.isaafp.org/entries/Laplace\_Transform.html (2018)
50. Jeannin, J.B., Ghorbal, K., Kouskoulas, Y., Gardner, R., Schmidt, A., Zawadzki, E., Platzer, A.: Formal Verification of ACAS X, An Industrial Airborne Collision Avoidance System. In: Embedded Software. pp. 127-136. IEEE (2015)
51. Khan-Afshar, S., Hasan, O., Tahar, S.: Formal Analysis of Electromagnetic Optics. In: Novel Optical Systems Design and Optimization XVII. vol. 9193, p. 91930A. International Society for Optics and Photonics (2014)
52. Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al.: SeL4: Formal Verification of an OS Kernel. In: Operating Systems Principles. pp. 207-220. ACM (2009)
53. Li, L., Shi, Z., Guan, Y., Zhao, C., Zhang, J., Wei, H.: Formal Verification of a Collision-free Algorithm of Dual-arm Robot in HOL4. In: Robotics and Automation. pp. 1380-1385. IEEE (2014)
54. Liu, J., Zhan, B., Wang, S., Ying, S., Liu, T., Li, Y., Ying, M., Zhan, N.: Formal Verification of Quantum Algorithms using Quantum Hoare Logic. In: Computer Aided Verification. pp. 187-207. Springer (2019)
55. Liu, L., Aravantinos, V., Hasan, O., Tahar, S.: On the Formal Analysis of HMM using Theorem Proving. In: Formal Methods and Software Engineering. LNCS, vol. 8829, pp. 316-331. Springer (2014)
56. Liu, L., Hasan, O., Tahar, S.: Formalization of Finite-state Discrete-time Markov Chains in HOL. In: Automated Technology for Verification and Analysis. LNCS, vol. 6996, pp. 90-104. Springer (2011)
57. Liu, L., Hasan, O., Tahar, S.: Formal Analysis of Memory Contention in a Multiprocessor System. In: Formal Methods: Foundations and Applications. LNCS, vol. 8195, pp. 195-210. Springer (2013)
58. Liu, L., Hasan, O., Tahar, S.: Formal Reasoning about Finite-state Discrete-time Markov Chains in HOL. Journal of Computer Science and Technology 28(2), 217231 (2013)
59. Loos, S.M., Platzer, A., Nistor, L.: Adaptive Cruise Control: Hybrid, Distributed, and now Formally Verified. In: Formal Methods. LNCS, vol. 6664, pp. 42-56. Springer (20011)
60. Mahmoud, M.Y., Aravantinos, V., Tahar, S.: Formalization of Infinite Dimension Linear Spaces with Application to Quantum Theory. In: NASA Formal Methods Symposium. LNCS, vol. 7871, pp. 413-427. Springer (2013)
61. Mahmoud, M.Y., Aravantinos, V., Tahar, S.: Formal verification of Optical Quantum Flip Gate. In: Interactive Theorem Proving. LNCS, vol. 8558, pp. 358-373. Springer (2014)
62. Mahmoud, M.Y., Tahar, S.: On the Quantum Formalization of Coherent Light in HOL. In: NASA Formal Methods Symposium. LNCS, vol. 8430, pp. 128-142. Springer (2014)
63. Mhamdi, T., Hasan, O., Tahar, S.: On the Formalization of the Lebesgue Integration Theory in HOL. In: Interactive Theorem Proving. LNCS, vol. 6172, pp. 387-402. Springer (2010)
64. Mhamdi, T., Hasan, O., Tahar, S.: Formalization of Entropy Measures in HOL. In: Interactive Theorem Proving. LNCS, vol. 6898, pp. 233-248. Springer (2011)
65. Mhamdi, T., Hasan, O., Tahar, S.: Evaluation of Anonymity and Confidentiality Protocols using Theorem Proving. Formal Methods in System Design 47(3), 265286 (2015)
66. Mitsch, S., Ghorbal, K., Platzer, A.: On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles. In: Robotics: Science and Systems (2013)
67. Mitsch, S., Loos, S.M., Platzer, A.: Towards Formal Verification of Freeway Traffic Control. In: Cyber-Physical Systems. pp. 171-180. IEEE Computer Society (2012)
68. Owre, S., Rushby, J.M., Shankar, N.: PVS: A Prototype Verification System. In: Automated Deduction. LNCS, vol. 607, pp. 748-752. Springer (1992)
69. Paulson, L.C.: Isabelle: A Generic Theorem Prover, vol. 828. Springer Science & Business Media (1994)
70. Platzer, A., Clarke, E.M.: Computing Differential Invariants of Hybrid Systems as Fixedpoints. Formal Methods in System Design 35(1), 98-120 (2009)
71. Platzer, A., Clarke, E.M.: Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study. In: Formal Methods. LNCS, vol. 5850, pp. 547-562. Springer (2009)
72. Platzer, A., Quesel, J.D.: European Train Control System: A Case Study in Formal Verification. In: Formal Methods and Software Engineering. LNCS, vol. 5885, pp. 246-265. Springer (2009)
73. Platzer, A., Quesel, J.D.: KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description). In: Automated Reasoning. LNCS, vol. 5195, pp. 171178. Springer (2008)
74. Rajkumar, R., Lee, I., Sha, L., Stankovic, J.: Cyber-physical Systems: The Next Computing Revolution. In: Design Automation Conference. pp. 731-736. IEEE (2010)
75. Rand, R., Paykin, J., Zdancewic, S.: QWIRE practice: Formal Verification of Quantum Circuits in Coq. arXiv preprint arXiv:1803.00699 (2018)
76. Rashid, A., Hasan, O.: Formalization of Lerchs Theorem using HOL Light. Journal of Applied LogicsIFCoLog Journal of Logics and their Applications 5(8), 1623-1652 (2018)
77. Rashid, A., Hasan, O.: On the Formalization of Fourier Transform in Higher-order Logic. In: Interactive Theorem Proving. LNCS, vol. 9807, pp. 483-490. Springer (2016)
78. Rashid, A., Hasan, O.: Formal Analysis of Continuous-time Systems using Fourier Transform. arXiv preprint arXiv:1707.09941 (2017)
79. Rashid, A., Hasan, O.: Formal Analysis of Linear Control Systems using Theorem Proving. In: Formal Methods and Software Engineering. LNCS, vol. 10610, pp. 345-361. Springer (2017)
80. Rashid, A., Hasan, O.: Formal Analysis of Robotic Cell Injection Systems using Theorem Proving. In: Design, Modeling, and Evaluation of Cyber Physical Systems. LNCS, vol. 11267, pp. 127-141. Springer (2017)
81. Rashid, A., Hasan, O.: Formalization of Transform Methods using HOL Light. In: Intelligent Computer Mathematics. LNAI, vol. 10383, pp. 319-332. Springer (2017)
82. Siddique, U., Aravantinos, V., Tahar, S.: Formal Stability Analysis of Optical Resonators. In: NASA Formal Methods Symposium. LNCS, vol. 7871, pp. 368-382. Springer (2013)
83. Siddique, U., Beillahi, S.M., Tahar, S.: On the Formal Analysis of Photonic Signal Processing Systems. In: Formal Methods for Industrial Critical Systems. LNCS, vol. 9128, pp. 162-177. Springer (2015)
84. Siddique, U., Mahmoud, M.Y., Tahar, S.: On the Formalization of Z-Transform in HOL. In: Interactive Theorem Proving. LNCS, vol. 8558, pp. 483-498. Springer (2014)
85. Siddique, U., Mahmoud, M.Y., Tahar, S.: Formal Analysis of Discrete-time Systems using Z-transform. Journal of Applied LogicsIFCoLog Journal of Logics and their Applications 5(4) (2018)
86. Siddique, U., Tahar, S.: A Framework for Formal Reasoning about Geometrical Optics. In: Intelligent Computer Mathematics, LNCS, vol. 8543, pp. 453-456. Springer (2014)
87. Siddique, U., Tahar, S.: Towards Ray Optics Formalization of Optical Imaging Systems. In: Information Reuse and Integration. pp. 378-385. IEEE (2014)
88. Siddique, U., Tahar, S.: Towards the Formal Analysis of Microresonators based Photonic Systems. In: Design, Automation & Test in Europe. pp. 1-6. IEEE/ACM (2014)
89. Siddique, U., Tahar, S.: On the Formalization of Cardinal Points of Optical Systems. In: Formalisms for Reuse and Systems Integration. AISC, vol. 346, pp. 79102. Springer (2015)
90. Siddique, U., Tahar, S.: On the Formal Analysis of Gaussian Optical Systems in HOL. Formal Aspects of Computing 28(5), 881-907 (2016)
91. Siddique, U., Tahar, S.: Formal Verification of Stability and Chaos in Periodic Optical Systems. Journal of Computer and System Sciences 88, 271-289 (2017)
92. Slind, K., Norrish, M.: A Brief Overview of HOL4. In: Theorem Proving in Higherorder Logics. LNCS, vol. 5170, pp. 28-32. Springer (2008)
93. Taqdees, S.H., Hasan, O.: Formalization of Laplace Transform Using the Multivariable Calculus Theory of HOL-Light. In: Logic for Programming, Artificial Intelligence, and Reasoning. LNCS, vol. 8312, pp. 744-758. Springer (2013)
94. Taqdees, S.H., Hasan, O.: Formally Verifying Transfer Functions of Linear Analog Circuits. IEEE Design & Test 34(5), 30-37 (2017)
95. Walter, D., T¨ aubig, H., L¨ uth, C.: Experiences in Applying Formal Verification in Robotics. In: Computer Safety, Reliability, and Security. LNCS, vol. 6351, pp. 347-360. Springer (2010)
96. Wang, Y., Chen, G.: Formalization of Laplace Transform in Coq. In: Dependable Systems and Their Applications. pp. 13-21. IEEE (2017)
97. Wu, A., Shi, Z., Yang, X., Guan, Y., Li, Y., Song, X.: Formalization and Analysis of Jacobian Matrix in Screw Theory and its Application in Kinematic Singularity. In: Intelligent Robots and Systems. pp. 2835-2842. IEEE (2017)