Ensuring the safety of complex industrial control systems (ICS) cannot be fully achieved during the design and development phases. Many uncertainties and unknowns only become apparent during real-world operation, especially in the context of Industry 4.0, where ICS integrate increasing characteristics of cyber-physical systems (CPS), such as openness and connectivity. Runtime verification (RV) is extensively employed to guarantee the runtime safety of systems. However, current RV methods face substantial challenges in ICS, particularly due to extensive device heterogeneity, intricate real-time constraints, and the need for coordinating multiple controllers. In this article, we propose a novel framework that incorporates stream-based RV to ensure the runtime safety of ICS. By leveraging a communication bridge based on the open platform communications unified architecture (OPC UA) standard, our framework achieves platform compatibility. This framework, coupled with its nonintrusive verification feature, is well-suited for scenarios involving heterogeneous devices and collaborative controllers. Additionally, stream-based formal specification captures complex time-sensitive constraints, such as real-time synchronizations involving various signals, including triggering, duration, and timeout. To further enhance safety, the framework offers online correction strategies for addressing runtime violations, aiming to preserve or restore system safety. Experimental results from general case studies demonstrate that our approach surpasses existing methods in managing device heterogeneity, complex real-time constraints, and multicontroller cooperation scenarios.

Great achievements have improved the efficiency and effectiveness of formal verification fairly, such that it is now applicable to industrial-scale software. However, verifying a full software system is still considered too complex. In practice, industrial control software models to be verified may result in state space explosion. We propose a problem frame-based approach that takes the full software system as input and tries to decompose the full software model into some smaller modules. Our approach decomposes the whole safety requirements to sub safety requirements, and the verification problem of the whole model is projected to sub verification problem according to the decomposed safety requirements. The sub verification problems check the projected sub models against the the sub safety requirements. We carry out an extensive evaluation based on the trackside subsystems in rail transit. Verifying the decomposed model can lead to a significant performance gain, due to the fact that abstract models reduce too much state space.

The decision-making process in autonomous driving systems encounters large uncertainties with environmental changes and needs to face the complex spatio-temporal evolution of multiple objectives.Formal analysis and verification are crucial to establishing reliable and safe standards.In this paper, we propose an extension of the clock constraint language CCSL to construct spatio-temporal constraint and autonomous driving safety specifications, leveraging various autonomous driving scenarios.Additionally, we introduce probabilistic spatio-temporal events and devise extensions for driving specifications that incorporate stochasticity.This specification is converted to the UPPAAL-SMC model for facilitating formal modeling and verification.Specific schemes and verification are given in conjunction with a typical autonomous driving scenario.

Automatic flight control systems (AFCS) are safety-critical systems tightly integrating computation, networking and physical processes. However, the uncertainty resulting from evolving dynamics in cyberspace and the physical world can affect the reliability of decision-making in the controller, threatening the system’s safety. How to accurately capture the uncertainty, effectively control the aircraft and improve safety has become an unavoidable challenge for the software industry. To this end, we define an uncertainty-aware modeling language (UAML), which supports modeling the AFCS’s dynamic behavior and environmental uncertainty using formal specifications. We use a machine learning-based method to predict the risk levels in operating environments as the representation of uncertainty from the physical world. The prediction result is transferred to UAML as the parameters. On this basis, we present a framework for quantitative safety evaluation using statistical model checking based on UPPAAL-SMC to help AFCS make reliable decisions at runtime. We illustrate our approach by modeling and analyzing a realistic example, and the experimental result demonstrates the effectiveness of our approach.

Cyber-physical System (CPS) represents a system that tightly integrates computation, communication, and physical processes. As an effective modeling language, AADL is often applied for real-time and embedded systems. However, AADL has limitations in modeling stochastic events because the interaction between the system and an uncertain external environment is often complex and unpredictable. In this paper, we propose a stochastic hybrid modeling language based on AADL, called SHML. SHML supports both continuous behavior analysis and probabilistic modeling of CPSs. To achieve the verification objective, we present a set of mapping rules to transform the SHML design into networks of stochastic hybrid automata (NSHA). By using statistical model-checking techniques, the obtained NSHA model and performance queries are jointly applied to evaluate the quantitative performance of SHML designs. Experiments on traffic collision avoidance systems are conducted, and the results demonstrate the usability and effectiveness of our approach.

Safety is critical for the new technology of the communication-based train control (CBTC) system, the train-to-train CBTC (T2T-CBTC) system, which establishes direct communication between trains. In this paper, we define a parametric spatio-temporal hybrid modeling language (StHML(p)), focusing on the extension of spatio-temporal elements and probability parameters, to model the T2T-CBTC system. The parameters are risk states which come from the uncertain environment. To this end, we present a safety-risk prediction method based on a deep recurrent neural network for the T2T-CBTC system, which takes into account highly imbalanced data of the system, to predict the risk states through environment data. To verify StHML(p) model, we propose a mapping algorithm to transform StHML(p) into NSHA (Networks of Stochastic Hybrid Automaton) and employe the statistical model checker UPPAAL-SMC for verifying quantitative properties. Finally, we implement our approach in an T2T-CBTC system.

Analysis of spatial behaviors of safety-critical systems attracts more and more attention in the filed of cyber physical systems and image processing. The major problem is expressiveness and verifiability for modeling and analysis of spatial behaviors. In order to verify the satisfiability problem of spatial properties, in this paper, we propose a novel topometric model through inducing a topological space with metric distance. For the spatial logic, we specify spatial properties with S4u in continuous regions, which are encoded S4u formula to RCC-8 relations, and discrete spatial regions, whose evolution is achieved through extending S4u with spatial near and until, named S4ue. We present a spatial model checking algorithm to verify if an S4u spatial term or formula satisfies the topometric model. We exemplify the applicability of the approach on obstacle avoidance-based path planning of robots.

Combining spatial and temporal primitives together is quite useful to specify dynamic behaviors of cyber-physical systems. The ability to represent spatio-temporal properties by means of formulas in spatio-temporal logics has recently found important applications in various fields, such as runtime verification, parameter synthesis, contract-Based design. In this paper, we present a spatio-temporal specification language, STSL, by combining Signal Temporal Logic (STL) with a spatial logic S4u, to characterize spatio-temporal dynamic behaviors of cyberphysical systems. This language is highly expressive: it allows the description of quantitative signals, by expressing spatiotemporal traces over real valued signals in dense time, and Boolean signals, by constraining values of spatial objects across threshold predicates. STSL combines the power of temporal modalities and spatial operators, and enjoys important properties such as safety and liveness. We provide the falsification problem through extending Lemire's algorithm and a parameter synthesis procedure by calling the simulated annealing algorithm. We demonstrate the proposed approaches on adaptive cruise control system and path planning of quadrotors.

Describing spatio-temporal behaviors of cyber-physical systems attracts more and more attention in the filed of intelligent transportation systems and biological systems. The major problem is expressiveness and verifiability for modeling and analysis of spatio-temporal behaviors. In order to verify spatial and spatio-temporal behaviors, in this paper, we propose a methodology to model the evolution of spatial scene snapshots and verify the spatio-temporal models. Firstly, we define a novel Topograph through inducing Bigraph in topological space to characterize cyber-physical systems and verify the model against patterns specified with S4uformulas. Secondly, for spatio-temporal verification, we extend Topograph in dense time, named Temporal Topograph, to describe the evolution of spatial objects, which are verified against spatio-temporal specification language. We evaluate the applicability of the approach on CBTC-based intelligent transportation systems.

Specifying spatio-temporal aspects is one of the important areas in cyber-physical systems.Spatio-temporal logic with changes of truth value in discrete time and dense time has been researched, but a combination of spatial and temporal components with changes of spatial entities in dense time hasn't been well-done.The major problem is dense time and real-valued variables of the spatio-temporal properties of cyber-physical systems.In this paper, we propose a spatio-temporal specification language, named STSL, which integrates Signal Temporal Logic (STL) with a spatial logic S4u to deal with the changes of realvalues spatial entities in dense time.The combined language is divided into two formalisms, ST SLP C and ST SLOC , which is applied to interpret the Boolean semantics and quantitative semantics, respectively.The syntax of the two formalism and the corresponding semantics are provided.Besides, we present a Hilbert-style axiomatization for the proposed STSL and provide the soundness and completeness result by the spatio-temporal extension of maximal consistent set and canonical model.