Formal Verification of a Dependable State Machine-Based Hardware Architecture for Safety-Critical Cyber-Physical Systems: Analysis, Design, and Implementation

With the increasing interest in embedding digital devices in safety-critical cyber-physical systems (CPSs), such as industrial automation, aerospace, and automotive industries, attention has been directed toward proposing verifiable and reliable architectures. Prominent levels of formal verification and fault-tolerance are a requirement in dependable CPS systems to ensure system design meet the specifications and verify safety properties. In this paper, a novel formal verifiable and fault-tolerant hardware architecture uses the concepts of state machine, verification, and fault-tolerance as a foundation is developed. It is divided into four models: analysis model includes the functional requirements defined by the user, design model, the finite state machine is utilized to model the systems behavior which is tested by the NuSMV checker tool, implementation model simulates test cases on waveforms to validate the design against the requirements and verification model verifies functional and critical properties using mathematical formal linear time and computation tree logic to prove compliance with requirements and detect errors. The system uses temporal logic to formulate the required properties for a railway interlocking system (RIS) as a case study and symbolic model verifier (SMV) to demonstrate the correct execution. From the simulation results, the effectiveness of the architecture is proved for verifying critical properties and detecting design faults through majority voting circuits. The proposed architecture has been synthesized in the Altera FPGA programmable chip with logic elements 33%, 52% area overhead, and frequency as 100 MHz. The system does meet its reliability requirements with the lowest reliability 91.333687 x \({10}^{-2}\) and failure rate 0.2 failure per hour at time 60 min. Finally, we think that adopting this architecture will enhance the trustworthiness and certification of CPS systems.