SCADE is both a language and a model-based software development environment that can develop systems in safety-critical elds. It is paramount for these systems to satisfy their safety requirements. Although SCADE can verify some properties by its Design Veri er (DV), it cannot verify the unbounded temporal or liveness properties due to its limitation. With the diversi cation of system application scenarios, these temporal properties also need to be veri ed to ensure the reliability of the system. In this paper, we concentrate on solving this problem by introducing Scade2Nu, a tool that can transform SCADE state machines into NuSMV input languages. Scade2Nu helps the designer to apply Linear-time Temporal Logic (LTL) and Computational Tree Logic (CTL) formulas as the requirements speci cations of SCADE models. With the aid of the NuSMV model checker as well as its veri cation results, designers can explore more di erent kinds of properties to further reduce bugs at the requirements phase in the development cycle.
Embedded software in elds like aerospace, rail transportation, industrial and nuclear energy often requires safety in analysis and high-security standards. SCADE (Safety Critical Application Development Environment) can design critical systems such as emergency braking systems, power and fuel management, automatic train operation and many other industrial applications. It has broad application in safety-critical elds also because of its compliance with safety standards such as DO-178B/C, IEC 61508 and EN 50128. Most of these standards de ne the guidelines that the veri cation of requirements for systems can minimize the risk of error introduction in the design phase and ensure the e ectiveness of the left software development process.
Design Veri er[ADS+04] (DV) is the formal veri cation component for SCADE, and it expresses safety requirements with SCADE language and performs SAT-based model checking on SCADE models. However, as the number of SCADE users grows, the stricter, more diverse temporal properties arising from the safety-critical requirements will be for veri cation purposes. In formal veri cation, the popular alternative methods for specifying most of these properties are temporal logics, such as Linear Time Logic (LTL) or Computation Tree Logic (CTL). However, DV cannot adequately express general temporal speci cations. In order to analyze the liveness property in industrial practise, Daskaya et al.[DHM11] have transformed the SCADE state-based model into UPPAAL. Therefore, the capability of verifying various temporal properties of SCADE models is an expected demand by SCADE users. If it would support temporal logics, unbounded temporal speci cations could be expressed and checked as well so that more defects can be detected and eliminated earlier in the design phase in the development cycle. Therefore, we present Scade2Nu, a tool that can use temporal logics like LTL and CTL speci cations to verify whether the safety-critical requirements of control systems designed by SCADE have been met.
In SCADE, engineers often use its state machine to design critical control systems. In the high-level, the structure of the SCADE state machine (SSM) is similar to that of the StateChart[Dor08][Har87], which means it has the characteristic of hierarchical state machine[AY01]. Taking it into consideration, Scade2Nu translates the SCADE state machine models into the input language of NuSMV1. The reasons why we choose NuSMV are ¬ the strict correctness of its model language, the ability to express hierarchical models and ® the e ective model checking algorithms. The translator framework we applied in Scade2Nu is based on the STP-approach presented by Clarke et al.[CH00]. They de ned a modular translation rule through a temporal language ETL, which correctly describes the transformation from StateChart to SMV. Since the actions in SCADE models are more concrete so we re ne the monitor-like mechanism in STP-approach as SCADE variables-monitor mechanism in the implementation of Scade2Nu so that it can accommodate for the SCADE situation.
In the following, we present an overview of Scade2Nu in Section 2. Section 3 will show the usage of Scade2Nu via a case study. Finally, the conclusion and future works will be presented in Section 4. 2
Scade2Nu brings the bene ts of temporal veri cation technology to the SCADE requirements veri cation. The veri cation framework and architecture of Scade2Nu are illustrated in Fig.1. This process starts with a SCADE model and its safety requirements, then translates SCADE models into NuSMV programs. Scade2Nu has the following components that make it do the translation:
1A symbolic model checker, see http://nusmv.fbk.eu/ Export
SCADE Model
Feedback
Safety Requirement
Specification Formulas
ANTLR2. This parser generates the parse tree and provides the base interface for tree visiting.
Symbol Table Container. This component accepts the parse tree, extracts its information and stores them into a symbol table. The symbol table is a data structure of the hierarchical SCADE State Machine (SSM). We de ne it with a tuple hI; O; SM; Op; F uni where I and O are the set of input variables and output variables respectively. SM is a set fSM1; :::; SMng where each SMi represents the structure of a sub-state machine. The basic operation blocks that SSM used are stored in Op, while F un has all function nodes that the SSM used. The operations library that Scade2Nu supports includes basic operations, such as mathematical operations, comparison operations, logical operations, choice operations, and temporal operations like previous. And we concentrate on functions in data- ow forms. A function node has its input variables, output variables, and equations so that it can operate computations.
Scade2Nu implements many listeners and visitors using the ANTLR runtime API so that it can get all information about the SCADE state machine and pack it in an SSM symbol table. However, before we put an SSM into translation engine, we had better use abstraction techniques so that veri cation of NuSMV models can run faster. Though we know that NuSMV model checker is a symbolic model checker that can handle systems with large space size, we should also provide an option which bounds the ranges of some or all variables in Scade2Nu for engineers. The bene t of this simMOpDlUeLEabSsMt1raction is helping to further reduce the state MsOpDaULcEe Sseizte_V.i(v1,…,vi, MODULE _ 1 set_vi_s1, reset_vi_s1, function_1,…,function_ Translation Engine. In this step, Scade2Nu puts the SSM instance into the translation engine andINgIeTnerates four parts of the target model based on translatMiOoDnULEruSlMe2s : ¬ statIenvpaumrti/aaOcbulhteipsnute modules SM…i, monitor mvoid=udleesfault value; Set_Var, ® Function modules, and ¯ the main module. Translation rules that Scade2Nu implementsASaSrIenGeNbxat(sveid) := on STP-approach. The detials of the rules and the mechanismcan can be found in our online resource3. Thescease next(set_vi translation rules are classi ed into two aspects. The engine applies Stehte/Rreuselets about the h…ierarchical structure ofnext(reset_ state machines and re nes the rules of a monitor-MlOikDUeLEmSeMc3hanism. PaMroanmiettoerrs …
Hierarchical Structure. Each sub-state machine in the SCADE models corresponds to one state machinneexnte(xrte(sseett__vvii_ module SMi in the NuSMV program. These modules are built in a hierarchical structure through two parametersTRUE esac; active and default that introduced in STP-approach. The engine follows the translation rules to generate the hierarchical state machine modules. …
SCADE Variable Monitor Mechanism. In STP-approach, the monitor-like mechanism means for every event or condition variable var there is a monitor module Set_Var which is a solo module to manipulate the variable var via monitor parameters. But the problem is that its full abstraction of conditions and events will ignore the concrete actions in SCADE states. In SCADE state machine, one state s may do speci c operations on their output variables. Therefore, we re ne the two forms of monitor parameters setm and resetm in STP-approach to set(var;s) and reset(var;s).
MODULE SM1 MODULE SM2 MODULE SM3 …
Input/Output variables Set/Reset
Monitor Parameters
MODULE _ 1 … … MODULE _ MODULE _
MODULE Set_Vi(v1,…,vi,…, vn, set_vi_s1, reset_vi_s1,…, set_vi_sm, reset_vi_sm, function_1,…,function_k) INIT
vi = default value; ASSIGN next(vi) := case next(set_vi_s1) : set_action(s1); next(reset_vi_s1) : reset_action(s1);
… next(set_vi_sm) : set_action(sm); next(reset_vi_sm) : reset_action(sm);
TRUE : vi; esac;
Assume that v1; :::; vi; :::; vn are the variables of an SSM, s1; :::; sm denote the states that have behaviors about vi. Fig.2 shows what the monitor module for variable vi looks like after translation. It declares the related monitor parameters (re)set(var;s). And the (re)set action is the assignment expression for vi that need to be performed in respective states. They are data- ow operations in states, and the engine translates these operations 2ANother Tool for Language Recognition, see https://www.antlr.org/ 3Online appendix. into corresponding expressions straightforwardly. Some of them apply other function nodes that user-de ned. So, Scade2Nu can declare parameters f unction1; :::; f unctionk if actions need.
In the left of Fig.2 shows the SCADE variable monitor mechanism after we re ne the monitor parameters. The variables may change the transition condition expressions so that they can make state machines do state transitions. Each sub-state machine module SMi reads these variables and operates the assignment of monitor parameters based on STP-approach. So it rewrites the values of monitor parameters so that these parameters can decide the values of output variables through the assignment in the monitor modules. This is how the monitor parameters manipulate the state machines indirectly.
Function modules are generated from F un. Each function has its own variables and equations. Since function nodes are in data- ow forms, the translation of each equation is straightforward. In the nal NuSMV model, there is only one main module that handles the top-level state machine. It instantiates its sub-state machines, monitor modules, and function modules, and generates the declarations of variables and monitor parameters. 3
In this section, we illustrate the procedure to verify the safety-critical requirements of a cruise control system using Scade2Nu. The cruise control is a industrial system created by Esterel Technologies, which can control the speed of a car automatically. The driver sets the pace and the system will take over the throttle of the vehicle to maintain the same speed. Fig.3 shows its state machine designed by SCADE Suit. Esterel Technologies provides this case in its SCADE suit and also develops many requirements about this case. Here we list three safety-critical requirements that we have to verify:
_Off Accel
ThrottleCmd
On 1 Off 1 last 'CruiseSpeed
CurSpeed On
Set QuickAccel QuickDecel CurSpeed _RegulOn
1 Regulator
1 CruiseSpeedMgt
_Regulation ThrottleCmd
CurSpeed
SpeedMin CruiseSpeed
CurSpeed SpeedMax _On 1 1 Accel > 0 or not between 1
1 Accel <= 0 and between
<SM3> _StandBy Accel
ThrottleCmd 1 between
<SM1> <SM2> Brake > 0 1
1 Resume
_Interrupt Accel
ThrottleCmd
Requirement 1: If Cruise control is always o , the throttle command is always controlled by the accelerator pedal sensor.
Requirement 2: When the car is under the cruise control, if driver brakes, the system will always be interrupted or o .
Requirement 3: All paths in the system satisfy that if the driver disables the cruise control, the next state of the system will be O for all paths.
Verifying these requirements with Scade2Nu. SCADE suit supports users to convert a graphical model into a textual SCADE language program. We also need to create a new le named VarBound which sets the bound of variables for the simple abstraction. Scade2Nu project accepts these two les and achieves the target .msomdvelm.oWdeel<cbpoymrepascnelyin>ctkitnhge tNheuStMranVslamtoiodnelbultetodonianglirinanme_t4Ch.reuistNeoCeooxnltbtro,al1r_w.1/eCIrunwisretiCthoeinstrdoclo1awsen, twhee gCeTtLtheorCLrTTuhiLusDefeCocro0m6n2tu1r:l0ao6s:l20.t2sh0m1a8vt 1 4Scade2Nu homepage and more cases, see https://sites.google.com/view/scade2nu Feedback
True False False correspond to system requirements. Then we can verify them through NuSMV. Fig.4 shows the graphic view of Scade2Nu and Table 1 presents the formulas written with temporal speci cations in NuSMV. Evaluation and limitations. Scade2Nu provides a counterexample visualizer (the middle bottom of Fig.4) that shows traces in a more friendly manner than the simple text produced by NuSMV because of the combination with NuSeen[AGR17]. Therefore, it can debug the SCADE model by analyzing the detail results. In this case, NuSMV reports that requirement 1 is valid. Requirement 2 and 3 are false and demonstrated by the generated counterexamples. For instance, we nd the unusual transition that from state _Interrupt to _Regulation in SM2 when the driver brakes. In another word, the circumstance that cruise control system will not always interrupt when the driver brakes may happen. So we have to modify it in SCADE model: the guard of transition from state _Interrupt to _Regulation need to be Resume and not (Brake > 0). The veri cation time of Scade2Nu depends on the right bounds of variables. We rstly did not set variable bounds and it took many hours to get the results. After we adding the bound option, the time reduces to few seconds and we get the same results. Therefore one of the limitations of Scade2Nu now is that users need to set variable bounds manually. In this paper, we have presented Scade2Nu, and it provides a new framework for the requirements veri cation of SCADE models. For simple safety requirements, Scade2Nu users only need to write down the temporal speci cations instead of building a monitor SCADE model in Design Verifer. For complex temporal properties that DV cannot express, Scade2Nu has the capability of expression and veri cation. Additionally, the results of the veri cation are more detailed because counterexamples are one of the strengths of model checkers.
However, Scade2Nu now only concentrates on the state-based control systems, so we plan to extend it to support systems that are data- ow oriented. Scade2Nu also needs to be tested by more industrial cases. Therefore, for the purpose of verifying more complex SCADE models, we also plan to support more temporal operations, arrays, as well as high-order operations of SCADE language in future work. 4.0.1
Acknowledgements This work is partially supported by National Natural Science Foundation of China (No. 61602178), Shanghai Science and Technology Committee Rising-Star Program (No.18QB1402000), China HGJ Project under Grant (No. 2017ZX01038 102-002) and National Defense Basic Scienti c Research Program of China (No. JCKY2016204B503).