=Paper=
{{Paper
|id=Vol-2584/PT-paper9
|storemode=property
|title=Bridging the Gap Between Requirements and Simulink Model Analysis
|pdfUrl=https://ceur-ws.org/Vol-2584/PT-paper9.pdf
|volume=Vol-2584
|authors=Anastasia Mavridou,Hamza Bourbouh,Pierre-Loic Garoche,Dimitra Giannakopoulou,Thomas Pressburger,Johann Schumann
|dblpUrl=https://dblp.org/rec/conf/refsq/MavridouBGGPS20
}}
==Bridging the Gap Between Requirements and Simulink Model Analysis==
https://ceur-ws.org/Vol-2584/PT-paper9.pdf
Bridging the Gap Between Requirements and Simulink
Model Analysis
Anastasia Mavridou Hamza Bourbouh
KBR / NASA Ames KBR / NASA Ames
anastasia.mavridou@nasa.gov hamza.bourbouh@nasa.gov
Pierre Loic Garoche Dimitra Giannakopoulou
Onera / KBR / NASA Ames NASA Ames
pierre-loic.garoche@onera.fr dimitra.giannakopoulou@nasa.gov
Thomas Pressburger Johann Schumann
NASA Ames KBR / NASA Ames
tom.pressburger@nasa.gov johann.m.schumann@nasa.gov
Abstract
Formal verification and simulation are powerful tools for the verification
of requirements against complex systems. Requirements are developed
in early stages of the software lifecycle and are typically expressed in
natural language. There is a gap between such requirements and their
software implementation. We present a framework that bridges this
gap by supporting a tight integration and feedback loop between high-
level requirements and their analysis against software artifacts. Our
framework implements an analysis portal within the fret requirements
elicitation tool, thus forming an end-to-end, open-source environment
where requirements are written in an intuitive, structured natural lan-
guage, and are verified automatically against Simulink models.
1 Introduction
The industry imposes a strict development process according to which requirements for safety-critical code are
written in the early phases of the software lifecycle, and are refined into models and/or code, while keeping
track of traceability information. Verification and validation (V&V) activities must ensure that the development
process properly preserves these requirements (for example, see the DO-178C [17] document). Requirements are
typically written in natural language, which is prone to be ambiguous and, as such, not amenable to formal
analysis. Frameworks like stimulus [14] or fret (Formal Requirements Elicitation Tool) [11, 12] address this
problem by enabling the capture of requirements in restricted natural languages with formal semantics. fret
additionally supports automated formalization of requirements in temporal logics.
To support V&V activities, it is necessary to associate high-level requirements with software artifacts in terms
of architectural information such as components and signals. For formulas generated by fret for example, the
atomic propositions or free variables of a formula must be connected to variable values or method invocations
Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International
(CC BY 4.0).
In: M. Sabetzadeh, A. Vogelsang, S. Abualhaija, M. Borg, F. Dalpiaz, M. Daneva, N. Fernández, X. Franch, D. Fucci, V.
Gervasi, E. Groen, R. Guizzardi, A. Herrmann, J. Horkoff, L. Mich, A. Perini, A. Susi (eds.): Joint Proceedings of REFSQ-2020
Workshops, Doctoral Symposium, Live Studies Track, and Poster Track, Pisa, Italy, 24-03-2020, published at http://ceur-ws.org
in the target Simulink model. To this end, we have developed an end-to-end, open-source requirements analysis
framework that supports a tight integration and feedback loop between high level requirements and the V&V of
models or code against these requirements. Our framework is available and open source; it currently connects
fret1 with the cocosim model verifier [3, 4, 7], with plans to extend it to support a variety of analysis tools.
Our framework provides: 1) automatic extraction of Simulink model information and association of require-
ments with target model signals and components; 2) translation of fret temporal logic formulas into synchronous
dataflow cocospec [5] specifications as well as Simulink monitors, to be used by verification tools; and 3) inter-
pretation of counterexamples produced by verification back at model and requirement levels.
Similarly to [2, 16], our framework checks formal properties against Simulink models, but unlike [16], it does
not involve translation by hand, and unlike [2], property propositions do not need to match model variables.
Moreover, in our framework, analysis results can be traced back to requirements.
2 Our framework step-by-step
Figure 1 shows the workflow of our requirement analysis frame-
work. The contributions of this paper are represented by con-
tinuous arrows. In Step 0, requirements written in fretish are
translated by fret into pure Past Time Metric Linear Tempo-
ral Logic (pmLTL) formulas. In Step 1, data is used from the
model under analysis to produce an architectural mapping be-
tween requirement propositions and Simulink signals. In Step
2, the pmLTL formulas and the architectural mapping are used
to generate monitors in cocospec, which is an extension of
the synchronous dataflow language Lustre [13] for the specifi-
cation of assume-guarantee contracts. In Step 3, the generated
cocospec monitors and model traceability data are imported
into cocosim [7] along with the Simulink model under anal-
ysis. cocosim automatically generates and attaches monitors
to the Simulink model. From the complete model (initial mod-
el and attached monitors), cocosim also generates equivalent
Lustre code. As a result, the complete model can be analyzed
by both Simulink-based (e.g., Simulink Design Verifier (SLDV))
and Lustre-based (e.g., Kind2 [6], Zustre [10]) verification tools
in Step 4. Counterexamples generated during the analysis can
be traced back to cocosim or fret for simulation in Step 5.
The next sections illustrate each workflow step in detail, us- Figure 1: Requirement analysis framework
ing a requirement from the Lockheed Martin Cyber Physical
Systems (LMCPS) challenge [8]. The LMCPS challenge is representative of flight-critical systems and is publicly
available.2 Requirement [FSM-001] (Figure 2) partly describes the required behavior of an advanced autopilot
system with an independent sensor platform.
NL: “Exceeding sensor limits shall latch an autopilot pullup when the pilot is not in control (not standby) and the system
is supported without failures (not apfail)”
FRETish: FSM shall always satisfy (sensorLimits & autopilot) ⇒ pullup
pmLTL: H((sensorLimits & autopilot) =⇒ pullup)
Figure 2: FSM-001 in Natural Language (NL), fretish, and pmLTL forms (the Boolean variable autopilot is an
abbreviation of (!standby & !apfail & supported))
1 https://github.com/NASA-SW-VnV/fret
2 https://github.com/hbourbouh/lm_challenges
Step 0 : FRETISH to pmLTL
A fretish requirement contains up to six fields: scope, condition, component*, shall*, timing, and
response*. Mandatory fields are indicated by an asterisk. component specifies the component that the re-
quirement refers to. shall is used to express that the component’s behavior must conform to the requirement.
response is a Boolean condition that the component’s behavior must satisfy. scope specifies the period when
the requirement holds. The optional condition field is a Boolean expression that further constrains when the
response shall occur. timing, e.g., always, after/for N time units, specifies when the response shall happen,
subject to condition and scope.
The manually written fretish version of requirement [FSM-001], shown in Figure 2, uses the component,
shall, timing, and response fields. Since scope and condition fields are omitted, the requirement holds uni-
versally. The autopilot proposition was used by the requirements engineer to simplify the requirement; it equals
(! standby & ! apfail & supported). For each requirement, fret generates a pmLTL formalization, e.g.,
see Figure 2 for the pmLTL of [FSM-001]. H refers to the Historically pmLTL operator [1].
Step 1 : Architectural Mapping
To generate monitors and automatically attach them at
the appropriate hierarchical level of the model, we need
architectural data from the model. For instance, for
[FSM-001], we need information about the hierarchical
level, i.e., the path, of the model component that cor-
responds to the FSM component mentioned in fretish.
Additionally, we need information about the signals of
the component, e.g., name, type (e.g., input, output),
datatype (e.g., boolean, double, bus) that correspond
to the propositions mentioned in [FSM-001].Our frame-
work provides a mechanism to automatically extract the
required architectural data from a Simulink model.
Once model data is imported, the architectural map-
ping procedure starts, which includes mapping every com-
ponent and proposition mentioned in a requirement to a
model component and a signal, respectively. There are Figure 3: sensorLimits mapping
two ways to do the architectural mapping: in the ideal
case where the same names are used both in the requirements and in the model, our tool automatically con-
structs the desired mapping. From our experience however, this is usually not the case. Different engineers
work on requirements and on models, and these two parts are hardly ever properly synchronized. For this rea-
son, we provide an easy-to-use user interface, through which the user can pick the path of the corresponding
model component or port from a drop-down menu and map it to a requirement component or proposition (see
Figure 3 for the mapping of the sensorLimits proposition of FSM, to the limits signal of the fsm 12B model
component). Then, our tool automatically identifies all the other required information (data types, dimensions,
etc) to generate correct-by-construction monitors and corresponding traceability data. Alternatively, a user may
provide the required information manually.
Step 2 : COCOSPEC Monitors and Traceability Data
To translate pmLTL into cocospec, we created a library of pmLTL operators in cocospec, a specification
language for Lustre:
-- Once -- Historically
node O ( X : bool ) returns ( Y : bool ) ; node H ( X : bool ) returns ( Y : bool ) ;
let let
Y = X or ( false -> pre Y ) ; Y = X -> ( X and ( pre Y ) ) ;
tel tel
--Y since X --Y since inclusive X
node S (X , Y : bool ) returns ( Z : bool ) ; node SI (X , Y : bool ) returns ( Z : bool ) ;
let let
Z = X or ( Y and ( false -> pre Z ) ) ; Z = Y and ( X or ( false -> pre Z ) ) ;
tel tel
The semantics of the unary pre and the binary initialization -> operators are defined as follows, in the
synchronous dataflow language Lustre. At time t = 0, pre p is undefined for an expression p, while for each
later time step t > 0, pre p returns the value of p at t − 1. At time t = 0, p -> q returns the value of p at t = 0,
while for t > 0 it returns the value of q at t. Here is the monitor fir [FSM001] in the cocospec language:
contract FSMSpec ( apfail : bool ; sensorLimits : bool ; standby : bool ; supported : bool ; ) returns (
pullup : bool ; ) ;
let
var autopilot : bool = supported and not apfail and not standby ;
guarantee " FSM001 " H (( sensorLimits and autopilot ) = > ( pullup ) ) ;
tel
The generated traceability data, which include the mapping of fretish propositions to the absolute paths of
the Simulink signals, are provided in JSON format.
1
sensorLimits
autopilot
3
supported
A
4
A ==> B In1 guarantee
apfail B
5 FSM001
(sensorLimits and autopilot) => (pullup)
standby
2
pullup
Figure 4: Generated Simulink monitor for requirement [FSM001]
Step 3 : Simulink Monitor Generation
cocosim attaches cocospec monitors to Simulink sub-
systems. This process relies heavily on cocosim’s Inputs T=0 T=1 T=2 T=3
Lustre-to-Simulink compiler. The first compilation step standby F F F F
is performed by LustreC [9], an open-source Lustre com- apfail F F F F
piler, which produces information necessary to extract supported T T T T
the model structure. The second step transforms the sensorLimits T F T F
produced structure into Simulink blocks through the Outputs
Simulink API. Each cocospec construct (e.g., assume, pullup F T F F
guarantee) is compiled and translated: their equivalent
Simulink blocks are provided by a dedicated cocosim Table 1: Counterexample for [FSM-001v2]
block library [7]. Mathematical operators are translated
into equivalent Simulink blocks. The pre operator is implemented as a Simulink Unit delay block. Figure 4
shows the generated Simulink monitor for [FSM-001]. Once the monitor is generated, cocosim automatically
attaches it to the Simulink model based on the traceability data from Step 2. Once generated and attached at
the model, the monitors can be used as runtime V&V components.
Step 4: Verification of the complete model
At this step, verification can be performed either at the Simulink level using e.g., the Simulink Design Verifier
or, at the Lustre level, using e.g., Kind2 [6]. Since requirements are initially given to us in natural language,
their semantics is often ambiguous. For instance, our interpretation in fretish of the requirement [FSM001],
where all conditions must be satisfied at the same time for pullup to be activated, was shown to be invalid when
checked against the model. After revisiting the requirement, we thought that potentially there is a time step
difference between limits = true and the activation of pullup. Thus we wrote the following second version,
which, however, was also shown to be invalid.
FSM-001v2: if autopilot & pre autopilot & pre limits FSM shall immediately satisfy pullup
Step 5: Counterexample simulation
Simulation of counterexamples is helpful for identifying weaker properties and producing meaningful reasoning
scenarios. For instance, let us consider requirement [FSM-001v2], for which Kind2 returned the counterexample
shown in Table 1. It is clear that, even though pullup was activated the first time sensorlLimits hold, it was
not activated at the second occurrence of sensorLimits. To better understand the behavior of the model, we
performed a simulation based on this counterexample. Figure 5 illustrates a scenario when sensorLimits occurs
multiple times during the autopilot operation, during which condition autopilot must be true. Based on this
simulation, we found that pullup is latched only when sensorLimits holds in the previous step and has not
been true for at least three steps before that [15].
This additional information helped us to tailor the proper requirement by disambiguating and refining the
original natural language requirement. This shows on one hand, the ambiguous nature of natural language and,
on the other hand, the elicitation capabilities of our framework.
3 Preliminary results
Table 2 summarizes preliminary results from applying
our approach to the LMCPS challenge, which is de-
scribed in detail in [15].Our framework is generic and
can use the strengths of several analysis tools. For ex-
ample, our case study uses Kind2 and SLDV. However,
since the MathWorks license prevents the publication
of empirical results comparing with SLDV, we only
provide the Kind2 results in Table 2.
In general, the LMCPS models are highly numeric Figure 5: Simulation of [FSM-001v2]
and non-linear, which makes analysis very challenging
when using SMT-based model checkers such as Kind2 and SLDV. In the case of Kind2, to handle non-linearities,
we used abstractions of non-linear functions such as trigonometric functions and as a result, Kind2 was able
to return an answer (decided) in cases that were undecided before adding the abstractions. We found modular
verification particularly helpful in order to obtain meaningful results. Due to its architectural mapping, our
framework allows us to deploy cocospec specifications at different levels of the model behavior. For instance,
for the FSM component, we generated three different contracts that we deployed at three different hierarchical
levels of the model. This is important for complex models where verification does not scale when applied at the
top level. We applied modular verification to 20 out of the 64 requirements.
4 Conclusion
We described an end-to-end framework in which require-
ments written in a restricted natural language can be Name NR D/UN
equivalently transformed into monitors and be analyzed Triplex Signal Monitor (TSM) 6 6/0
against Simulink models by Simulink-based and Lustre- Finite State Machine (FSM) 13 13/0
based verification tools. Our framework ensures that Tustin Integrator (TUI) 3 3/0
requirements and analysis activities are fully aligned: Control Loop Regulators (REG) 10 6/4
Simulink monitors are derived directly from require- Nonlinear Guidance (NLG) 7 0/7
ments (and not handcrafted), and analysis results are Feedforward Neural Network (NN) 4 0/4
traced back to requirements. The features of our frame- Control Effector Blender (EB) 3 0/3
work are generic and can be used to integrate other re- 6DoF Autopilot (AP) 8 8/0
quirement elicitation and analysis tools. In the future, System Safety Monitor (SWIM) 3 3/0
we plan to provide additional ways of providing feed- Euler Transformation (EUL) 7 7/0
back from analysis tools to requirement engineers, to
Total 64 46/18
support them in correcting requirements. We also plan
to extend our framework with additional types of anal- Table 2: LMCPS results with Kind2, NR : #analyzed
ysis that can be performed at the level of requirements, requirements, D: Decided, UN: Undecided
e.g., realizability checking.
Acknowledgements. We thank Mohammad Hejase, Cesare Tinelli, and Daniel Larraz for fruitful discussions
and feedback. This work was funded by the NASA ARMD System-Wide Safety Project.
References
[1] Baier, C., Katoen, J.P.: Principles of model checking. MIT press (2008)
[2] Balasubramanian, D., Pap, G., Nine, H., Karsai, G., Lowry, M., Păsăreanu, C., Pressburger, T.: Rapid
property specification and checking for model-based formalisms. In: 2011 22nd IEEE International Sympo-
sium on Rapid System Prototyping. pp. 121–127 (May 2011). https://doi.org/10.1109/RSP.2011.5929985
[3] Bourbouh, H., Garoche, P.L., Garion, C., Gurfinkel, A., Kahsai, T., Thirioux, X.: Automated analysis of
Stateflow models. EPiC Series in Computing 46, 144–161 (2017)
[4] Bourbouh, H., Garoche, P.L., Loquen, T., Noulard, É., Pagetti, C.: CoCoSim, a code generation framework
for control/command applications: An overview of CoCoSim for multi-periodic discrete Simulink models.
In: 10th European Congress on Embedded Real Time Software and Systems (ERTS 2020) (2020)
[5] Champion, A., Gurfinkel, A., Kahsai, T., Tinelli, C.: CoCoSpec: A mode-aware contract language for
reactive systems. In: Software Engineering and Formal Methods - 14th International Conference, SEFM
2016, Held as Part of STAF 2016, Vienna, Austria, July 4-8, 2016, Proceedings. pp. 347–366 (2016).
https://doi.org/10.1007/978-3-319-41591-8 24
[6] Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The Kind 2 model checker. In: Computer Aided Veri-
fication - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings,
Part II. pp. 510–517 (2016). https://doi.org/10.1007/978-3-319-41540-6 29
[7] CoCo-team: CoCoSim – automated analysis framework for Simulink. https://github.com/NASA-SW-VnV/
CoCoSim
[8] Elliott, C.: An example set of cyber-physical V&V challenges for S5, Lockheed Martin Skunk Works. In:
Laboratory, A.F.R. (ed.) Safe & Secure Systems and Software Symposium (S5), 12-14 July 2016, Dayton,
Ohio (2016), http://mys5.org/Proceedings/2016/Day_2/2016-S5-Day2_0945_Elliott.pdf
[9] Garoche, P., Kahsai, T., Thirioux, X.: LustreC, https://github.com/coco-team/lustrec
[10] Garoche, P., Kahsai, T., Thirioux, X.: Zustre, https://github.com/coco-team/zustre
[11] Giannakopoulou, D., Mavridou, A., Pressburger, T., Rhein, J., Schumann, J., Shi, N.: Formal requirements
elicitation with FRET. In: 26th Intl Working Conference on Requirements Engineering: Foundation for
Software Quality (REFSQ-2020, Tool) (2020), http://ceur-ws.org
[12] Giannakopoulou, D., Pressburger, T., Mavridou, A., Schumann, J.: Generation of formal requirements from
structured natural language. In: 26th Intl Working Conference on Requirements Engineering: Foundation
for Software Quality (REFSQ-2020) (2020)
[13] Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language
LUSTRE. Proceedings of the IEEE 79(9), 1305–1320 (1991)
[14] Jeannet, B., Gaucher, F.: Debugging Embedded Systems Requirements with STIMULUS: an Automotive
Case-Study. In: 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016).
TOULOUSE, France (Jan 2016), https://hal.archives-ouvertes.fr/hal-01292286
[15] Mavridou, A., Bourbouh, H., Garoche, P.L., Hejase, M.: Evaluation of the FRET and CoCoSim tools on the
ten Lockheed Martin cyber-physical challenge problems. Tech. Rep. TM-2019-220374, National Aeronautics
and Space Administration (February 2020)
[16] Nejati, S., Gaaloul, K., Menghi, C., Briand, L.C., Foster, S., Wolfe, D.: Evaluating model testing and
model checking for finding requirements violations in Simulink models. In: Proceedings of the 2019 27th
ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of
Software Engineering. p. 1015–1025. ESEC/FSE 2019, Association for Computing Machinery, New York,
NY, USA (2019). https://doi.org/10.1145/3338906.3340444
[17] RTCA, S.C.: DO-178C, Software Considerations in Airborne Systems and Equipment Cfertification (2011)