SMT-based Probabilistic Analysis of Timing Constraints in Cyber-Physical Systems

TL;DR

This paper presents an SMT-based method for probabilistic analysis of timing constraints in cyber-physical systems, integrating EAST-ADL, SIMULINK/STATEFLOW, and PrCCSL for safety-critical embedded system design.

Contribution

It introduces an automatic transformation from SIMULINK/STATEFLOW models to SMT formulas for probabilistic timing analysis in EAST-ADL systems, extending prior work with a practical approach.

Findings

Successfully applied to a cooperative automotive system case study.

Enables formal probabilistic analysis of timing constraints.

Reduces analysis to SMT validity checking.

Abstract

Modeling and analysis of timing constraints is crucial in cyber-physical systems (CPS). EAST-ADL is an architectural language dedicated to safety-critical embedded system design. SIMULINK/STATEFLOW (S/S) is a widely used industrial tool for modeling and analysis of embedded systems. In most cases, a bounded number of violations of timing constraints in systems would not lead to system failures when the results of the violations are negligible, called Weakly-Hard (WH). We have previously defined a probabilistic extension of Clock Constraint Specification Language (CCSL), called PrCCSL, for formal specification of EAST-ADL timing constraints in the context of WH. In this paper, we propose an SMT-based approach for probabilistic analysis of EAST-ADL timing constraints in CPS modeled in S/S: an automatic transformation from S/S models to the input language of SMT solver is provided; timing constraints specified in PrCCSL are encoded into SMT formulas and the probabilistic analysis of timing constraints is reduced to the validity checking of the resulting SMT encodings. Our approach is demonstrated a cooperative automotive system case study.

Figures

Tables

Table 1. TABLE I: Verification Results of Timing Constraints in Z3

Timing Constraint	Results	Time (Min)	Mem (Mb)	CPU (%)
End-to-End	valid	70.3	1710.75	23.81
Periodic	valid	12.7	2639.25	24.86
Sporadic	valid	202.4	1869.02	24.89
Execution	valid	12.7	2516.13	24.89
Synchronization	valid	63.6	2299.83	20.36
Comparison	valid	65.7	2005.06	23.63
Exclusion	valid	112.4	2569.08	20.47

Full text

I Introduction

Cyber-Physical Systems (CPS) are real-time embedded systems where the software controllers interact with physical environments. The continuous time behaviors of CPS often rely on complex dynamics as well as on stochastic behaviors. Modeling and analysis of timing constraints is essential to ensure the correctness of CPS. East-adl111EAST-ADL. https://www.maenad.eu/public/EAST-ADL-Specification_M2.1.9.1.pdf is an architectural description language for safety-critical embedded systems design. The latest release of East-adl has adopted the time model, which composes the basic timing constraints, i.e., repetition rates, end-to-end delays, and synchronization constraints. East-adl relies on external tools, e.g., Simulink/Stateflow222Simulink and Stateflow. https://www.mathworks.com/products.html (S/S), for system behaviors description. Simulink (Sl) is a block-diagram based formalism used to model continuous dynamics while Stateflow (Sf) is used to specify control logic and state-based model behaviors of systems. Despite its strength in system modeling and simulation, S/S lacks of formal semantics to support rigorous verification of specifications. To tackle this shortcoming, efforts have been devoted into formal analysis of S/S models by using formal methods, e.g., model-checking, satisfiability modulo theory (Smt) solving. However, the conventional formal analysis of real-time systems addresses worst case designs, typically used for hard deadlines in safety-critical systems. The “Less-than-worst-case” models are far less investigated. In fact, in most cases, a bounded number of violations of timing constraints in systems would not lead to system failures when the results of the violations are negligible, called Weakly-Hard (WH) [1]. In this paper, we propose an Smt-based approach to support formal probabilistic analysis of East-adl timing constraints in CPS modeled in S/S in the context of WH.

Clock Constraint Specification Language (Ccsl) is a formal language for specification of both logical and dense timing constraints. We have previously defined a probabilistic extension of Ccsl, called PrCcsl [2], which states that the relations (e.g., coincidence, causality and precedence) between events (e.g., input/output triggering, state changes) must hold with probability greater than or equal to a given probability threshold. Previous work is extended by including the supports of probabilistic analysis of timing constraints using Smt-based model checking:

1. S/S models, which describe the behaviors of systems, are transformed into the input language of Smt solver;

2. East-adltiming constraints with stochastic properties are specified in PrCcsl and encoded into Smt formulas;

3. The probabilistic analysis of timing constraints is reduced into validity checking of the resulting Smt encodings.

Our approach is demonstrated on a cooperative automotive system case study.

II Methodology & Experiment

The overview of our approach is shown in Fig. 1. In our approach, S/S models are stored in ‘.mdl’ files, which contain textual descriptions of the compositions of the models. Z3 Smt solver333Z3 SMT Solver. https://github.com/Z3Prover/z3 is employed as our verification engine.

To translate the stochastic functions (e.g., random number generation) in Sl, we adapt Z3py  (the Z3 API in Python) as encoding interface, in which the add-on modules for description of probability distributions can be leveraged. Given a system model in S/S and an East-adl timing constraint $\phi$ (specified in PrCcsl), the goal of our approach is to verify whether the probability of the constraint is greater than or equal to a probability threshold $p$, i.e., $Pr(\phi)\geq p$. To achieved this, we perform the following steps:

1. Extract necessary information (see Fig. 1) of S/S from .mdl file and translate S/S into Z3py encodings based on the extracted information;

2. Encode PrCcsl specifications of East-adl timing constraints (ETC) in Z3py and check the validity of the encodings using Z3.

Translation of S/S into Z3py: Fig. 2 shows an excerpt of S/S model in .mdl file, in which each object (e.g., block, data or state) has a unique identifier named $id$. The data/variables in discrete-time S/S model are updated at $sample\ time$ steps, which are translated into vectors (i.e., bounded lists) of appropriate sorts (e.g., integer, real and boolean). The index of the vectors represent the number of time steps have proceeded during simulation. For instance, an integer signal $a$ is mapped to an integer list, with $a[i]$ (i$$\in$$\mathbb{N}) representing the value of signal $a$ at $i^{th}$ step during simulation. In Sl, lines are used for data transmission. During simulation, the data of ports connected by the same line are identical, which is interpreted as the equivalence of the data in Z3py. The blocks of linear math/logic functions in Sl are mapped to the same arithmetic/logical operations in Z3py straightforwardly.

States in Sf can be either active or inactive during simulation, declared as integer vectors whose elements are either 1 (active) or 0 (inactive) in Z3py. The information of $state$ in .mdl file can be divided into three classes (see Fig. 2): Hierarchy includes decomposition, history junction and the relation between superstates and their substates (indicated by treeNode). Transition represents the passage of the system from one state to another when the condition (i.e., a boolean expression) on the transition is true. State action refers to the operations (e.g., assignments) executed when the state is active, entered or exited. After the information of hierarchy, transitions and actions (HTA) is extracted from the .mdl file, the translation of Sf becomes the interpretation of HTA of each state in Z3py, as presented in Algorithm 1.

Experiment: Our approach is demonstrated on a cooperative automotive system (CAS) [3], which includes distributed and coordinated sensing, control, and actuation over two vehicles running in the same lane. We consider seven types of timing constraints of CAS system, i.e., End-to-End, Periodic, Sporadic, Execution, Synchronization, Comparison and Exclusion constraints. The timing constraints are specified in PrCcsl, whose semantics is specified in the form of Smt formulas [2] that can be expressed in Z3py naturally. In our experiment, the simulation bound and the probability threshold are set to 3000 steps and 95% respectively. The experiment results are listed in Table I and all timing constraints are established as valid.

III Conclusion and Future Work

We present an Smt-based approach to perform probabilistic analysis of East-adl timing constraints in CPS described in Simulink/Stateflow. The practicality of our approach is demonstrated on a CAS case study. As ongoing work, the application of our approach in larger-scale case studies will be investigated and an automatic translator from Simulink/Stateflow (.mdl file) to Z3py will be developed.