Formal veri cation and simulation are powerful tools for the veri cation 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 highlevel 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 language, and are veri ed automatically against Simulink models.
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 veri er [
Our framework provides: 1) automatic extraction of Simulink model information and association of
requirements with target model signals and components; 2) translation of fret temporal logic formulas into synchronous
data ow cocospec [
Similarly to [
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) 1https://github.com/NASA-SW-VnV/fret 2https://github.com/hbourbouh/lm_challenges Step 0 : FRETISH to pmLTL A fretish requirement contains up to six elds: scope, condition, component*, shall*, timing, and response*. Mandatory elds are indicated by an asterisk. component speci es the component that the requirement 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 speci es the period when the requirement holds. The optional condition eld is a Boolean expression that further constrains when the response shall occur. timing, e.g., always, after/for N time units, speci es 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 elds. Since scope and condition elds are omitted, the requirement holds
universally. 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 [
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 corresponds 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 framework provides a mechanism to automatically extract the required architectural data from a Simulink model.
Once model data is imported, the architectural mapping procedure starts, which includes mapping every component 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 constructs the desired mapping. From our experience however, this is usually not the case. Di erent engineers work on requirements and on models, and these two parts are hardly ever properly synchronized. For this reason, 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 identi es 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 speci cation language for Lustre: -- Once node O(X: bool ) returns (Y: bool ); let
Y = X or ( false -> pre Y); tel --Y since X node S(X ,Y: bool ) returns (Z: bool ); let Z = X or (Y and ( false -> pre Z)); tel -- Historically node H(X: bool ) returns (Y: bool ); let
Y = X -> (X and ( pre Y)); tel --Y since inclusive X node SI (X ,Y: bool ) returns (Z: bool ); let
Z = Y and (X or ( false -> pre Z)); tel autopilot
1 sensorLimits
3 supported
4 apfail
5 standby
A B
A ==> B
In1
guarantee (sensorLimits and autopilot) => (pullup)
FSM001
The semantics of the unary pre and the binary initialization -> operators are de ned as follows, in the synchronous data ow language Lustre. At time t = 0, pre p is unde ned 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 r [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.
2
pullup
cocosim attaches cocospec monitors to Simulink
subsystems. This process relies heavily on cocosim's Inputs T=0 T=1 T=2 T=3
Lustre-to-Simulink compiler. The rst compilation step standby F F F F
is performed by LustreC [
At this step, veri cation can be performed either at the Simulink level using e.g., the Simulink Design Veri er
or, at the Lustre level, using e.g., Kind2 [
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 rst 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 [
This additional information helped us to tailor the proper requirement by disambiguating and re ning 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
Table 2 summarizes preliminary results from applying
our approach to the LMCPS challenge, which is
described in detail in [
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 veri cation particularly helpful in order to obtain meaningful results. Due to its architectural mapping, our framework allows us to deploy cocospec speci cations at di erent levels of the model behavior. For instance, for the FSM component, we generated three di erent contracts that we deployed at three di erent hierarchical levels of the model. This is important for complex models where veri cation does not scale when applied at the top level. We applied modular veri cation to 20 out of the 64 requirements. 4
ments written in a restricted natural language can be equivalently transformed into monitors and be analyzed against Simulink models by Simulink-based and Lustrebased veri cation tools. Our framework ensures that requirements and analysis activities are fully aligned: Simulink monitors are derived directly from requirements (and not handcrafted), and analysis results are traced back to requirements. The features of our framework are generic and can be used to integrate other requirement elicitation and analysis tools. In the future, we plan to provide additional ways of providing feedback from analysis tools to requirement engineers, to support them in correcting requirements. We also plan to extend our framework with additional types of analysis that can be performed at the level of requirements, e.g., realizability checking.
Triplex Signal Monitor (TSM) Finite State Machine (FSM) Tustin Integrator (TUI) Control Loop Regulators (REG) Nonlinear Guidance (NLG) Feedforward Neural Network (NN) Control E ector Blender (EB) 6DoF Autopilot (AP) System Safety Monitor (SWIM) Euler Transformation (EUL) Total 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.