Modeling, Analysis And Verification For Cyber-Physical Systems Based On Clock And Signal Constraints

Cyber Physical Systems (CPS) are complex systems that vise computations, com-munications and controls deeply embedded in and interacting with physical processes to enable the close interactions between the cyber and physical worlds. Comparing to other general purpose systems, the close interactions between cyber worlds and physical world-s bring CPS the intrinsic heterogeneity, concurrency and time-sensitivity, and demand higher confidence in predictability and safety. All the above features raise the following challenges of modeling, verification and analysis for CPS:the integration of heterogenous Models of Computations (MoCs), the fusion of heterogenous time models and behavior semantics, and the predictability and safety requirements. To address those challenges, we propose a framework for modeling, verification and scheduliability analysis of CPS. The main contributions of this dissertation can be summarized as follows.· A declarative language for CPS modeling, Signal Constraint Modeling language (SCM-L). is defined based on the theory of Model of Computation (MoC). With SCML, an environment-based modeling method is given to address the challenges of CPS model-ing. The time model of SCML is heterogenous, including logical time which supports untimed causal based behaviors, and super dense time which provides an accurate and faithful description basis of hybrid of continuous timed dynamics and discrete timed dynamics. Based on the heterogenous time model, SCML provides various kinds of signals and signal constraints. Signals could be continuous timed, value continuous evolving but not continuous timed, discrete timed or logical ones. Different kinds of signals facilitate descriptions of heterogeneous behaviors. Signal constraints specify relations among signals, capturing the conversion and communications between signal-s as well as the diverse coordination rules from different MoC considerations. SCML is equipped with operational semantics to implement the integration of heterogenous MoCs and the fusion of heterogenous time models and behavior semantics. The environment-based modeling method uses SysML and UML-MARTE for co-modeling and SCML as their companion constraint language. Thanks to the formal operational semantics of SCML, the formed SCML specification provides an explicit semantic model for the behaviors of the SysML and UML-MARTE model. In this way, it also provides formal support for follow-up formal verification and schedulability analysis.· An approach to do schedulability analysis for SCML specifications is proposed. With the balance of details and efficiency in mind, we decide to extract necessary infor-mation from a SCML specification to form an extended dock constraint specification (eCCSL specification), and then use model checking techniques and tools to perform the schedulability analysis on the eCCSL specification. The approach includes the fol-lowing works:After analyzing the predictability and safety requirements, we identify properties to check, including conditions for admissible schedules, quality properties for scheduling like schedulability category and scheduling-time-insensitive property and quantitative standards of scheduling, such as scheduling success rate, scheduling missing rate and average response time. And we also identify their manifestations in the context of SCML specifications. To express the necessary information, wt; extend Clock Constraint Specification Language (CCSL) with clock terminations and physi-cal time references. For the model checking implementation, we provide a state-based operational semantics for the eCCSL. which benefits not only the checking but also the interpretation and other analysis of CCSL. We propose a method to extract necessary information from a SCML specification and express them in eCCSL. providing rules for the extraction from SCML signals and signal constraints to eCCSL clocks and clock constraints. We propose a method do perform schedulability analysis on the ex-tracted eCCSL specifications. They are transformed to NuSMV FSMs and UPPAAL timed automata, concerned properties are expressed in CTL and TCTL formulas, and corresponding model checkers are called to check transformed models against the properties. We relate the schedulability of a eCCSL specification to the problem of emptiness of recognizable language of a corresponding automata. Transition-based Generalized Buchi automata (tGBA) with acceptance criteria are proposed to deal with the problem of identifying admissible schedules. Based on them, an algorithm is given to select admissible schedules and to reduce the state space of a tGBA. Only the states that can lead to admissible schedules are remained. We provide an algorithm to detect bad choices that lead to scheduling failures. When there are other options it will warn users not to choose the bad ones.· An approach to formally verify SCML specifications is proposed. The approach in-cludes the following works:After analyzing the predictability and safety requirements we identify properties to check, including general properties like safetyness and live ness, business logic related properties, and some quantitative properties like response time for requests. And we also identify their manifestations in the context of SCML specifications. We construct the eCCSL specification for the SCML specification to verify, using similar methods as in the schedulability analysis. We propose a method to verify eCCSL specifications. The eCCSL specifications are transformed to Promela and UPPAAL timed automata, concerned properties are expressed in LTL and TCTL formulas, then corresponding model checkers are called to check transformed models against the properties. To prove the correctness of this approach, we define check-point labeled transition system and check-point bisimulation relation. Based on them. the correctness of the checking route is proved.The feasibility and effectiveness of our framework is evaluated by an industry scale case study, an intelligence traffic control system (which is a typical CPS application) applied in a common benchmark case, the railroad crossing problem.