-AutoFOCUS3 (AF3) [1] supports formal verification of its models using the nuXmv [2] model checker. This requires a model transformation from AF3 to nuXmv models. In this paper we present this behavior transformation. It is a two way transformation between a high-level and a low-level model involving intricate cases typical of behavior transformations whose solutions can therefore be beneficial to the community.
Model driven Engineering (MDE) allows us to model the system: its requirements, behavior, target platform, and generate code out of this model which can be deployed on the system. The behavior model of the system can be used for early verification, thus detecting bugs at an early stage of development, thereby saving time and money.
One way to perform verification is using formal methods, which are useful when we need high assurance, but are hard to use. They are however difficult to integrate with MDE tools because it requires a behavior transformation from a high-level MDE model to a low-level model of the formal analysis tool.
AutoFOCUS3 (AF3) [
In this paper we present the details of this model transformation. We believe this is useful to the community because it points out pitfalls that one typically encounters while developing a bi-directional transformation from a high-level to a low-level model and shows how to circumvent them. Most importantly, we designed the transformation to be modular, extensible and to maximize reuse: the reuse aspect is particularly put to practice with the reverse transformation.
This work deals with 1) transformation between a high level model and a low level model, 2) two way transformation: from AF3 to nuXmv and vice versa, 3) transformation of a high level model which can model both events and messages. Note finally that we have applied this solution to an industrial use case.
This transformation is a complete rebuild of the one
informally presented in [
The paper is structured as follows: Section II presents AF3 and nuXmv, Section III describes our transformation, Section IV describes a use case, Section V considers the related work, and Section VI concludes this paper.
In this section we give an overview of AF3 [
AutoFOCUS3 [
Fig. 1. Component architecture in AutoFOCUS3
This paper concerns the software architecture, whose following characteristics are essential for formal verification: Component-based: Software architecture in AF3 is a hierarchy of components communicating with each other through typed channels (Fig. 1) which are connected to ports. Ports, which can be input or output, form the interface of the component. Each port carries values of a defined type (no objects: only booleans, integers, doubles, enumerations, or combinations thereof). Channels in AF3 are statically fixed.
Atomic components, if implemented, contain a behavior specification modeled by a state machine or code expressed in a very simple language.1
nents is formally defined according to the FOCUS model
of computation [
nuXmv [
In nuXmv, a system is modeled as a finite state machine (FSM) described in terms of variables and constraints. Variables, which can be state variables or input variables, can have different values in different states. Constraints are used to describe 1) transition relations: how a state machine evolves during execution, 2) initial state, 3) invariants. It also supports hierarchical descriptions.
Three types of specifications are supported: LTL, CTL, and INVAR (invariants). The definition of the FSM, specifications, and declarations (input variables, state variables, constants, and define) are encapsulated in a module declaration.
A module can be then instantiated inside another module. Every nuXmv program must contain a main module. The main module does not have any parameters and is the entry point of the nuXmv model.
The transformation from AF3 to nuXmv models is not trivial as it transforms a model at a high level of abstraction to one at a lower level of abstraction. We now describe some AF3-specific notions which make the transformation challenging.
NoVal: AF3 allows to model situations where a channel is not carrying a value. This is required when modeling events, e.g., a user pressing the brake in a car. We could also see it as a null value. This situation is modeled using a special constant called NoVal which belongs to every port type and symbolizes the absence of an event in the current tick. This is problematic because a boolean type port in AF3 can then have three values: true; f alse; and N oV al, whereas in the model checker a boolean value can be only true or f alse. This is analogously true for ports of other types.
Causality: AF3 allows to specify the causality of a component as strong or weak. In a strongly causal components output 1Note that behavior can also be expressed using tables, but this feature is deprecated at the moment. ports are updated in the next clock tick, whereas in a weakly causal component output ports are updated in the same tick.
The strongly causal components can be seen as Moore machines: the output of the current tick is only dependent on the state and not on the input, input can only influence the output of the next tick (we can also see it as input only changing the state, which in turn affects the output). Weakly causal components can be interpreted as Mealy machines: output is dependent on both the state and the input.
As nuXmv does not have the notion of strong and weak causality this needs to be additionally handled.
User defined functions: AF3 also supports the use of functions defined by the user in a Data Dictionary. These functions are stateless and use the same simple language which can be used to define a component’s behavior. These are not part of the transformed component’s tree, but are contained in a separate subtree. Note that we do not describe this transformation in the paper.
We decompose the transformation in small step transformations. These transformations are then executed sequentially: the output of the first transformation is the input of the next. We denote the sequential composition by ”;”: applying T1; T2 on I means that first T1 is applied on I, and then T2 is applied on its output.
This decomposition allows the small step transformations
(or blocks) to be reused in different contexts, e.g., for the
reverse transformation (which was not possible in [
As a running example, we consider a component C, with
input port ip which is a boolean array of size 2, and a boolean
output port op which is true if both values are equal in the
input array. The behavior of the component is specified using
a code specification:
i f ( i p [ 0 ] = = i p [
It is a strongly causal component, which means that the output values are updated on the next tick.
At the top level, transformation of an AF3 model to a nuXmv model T is a chain of 2 transformations 1) normalization of the model, 2) transformation to nuXmv: T = TNorm; TnuXmv (1)
Fig 2 shows this chain in a pictorial form. From now on we describe chains using only the ”;” operator.
This transformation takes an AF3 model and transforms it into a normalized AF3 model, which is easier to transform to a nuXmv model. It is a chain of 5 transformations: TNormalize = TNames; TCodeSpec; TNoV al (2) ; TP roductT ypes; TCausality Note that (1) and (2) will be reused in Section III-C.
1) Name transformation: TName changes the names of the
artifacts by appending their internal id, and removing white
spaces and special characters. The references to these elements
are also transformed. The example is then transformed to:
i f ( i p 4 0 [ 0 ] = = i p 4 0 [
A code specification in AF3 is stateless, so it is transformed to an automaton with a single state, where each if (and else) block is converted to a transition. TCodeSpec is again a chain of 2 transformations:
TCodeSpec = TNormalizeCodeSpec; TT oAutomaton TNormalizeCodeSpec outputs a code specification which is behaviorally equivalent to the input and in a normalized form from which we can do a canonical transformation to a state automaton, and TT oAutomaton performs this canonical transformation.
Applying TNormalizeCodeSpec on the above code
specification results in the following code specification:
i f ( i p 4 0 [ 0 ] = = i p 4 0 [
Note the addition of the empty else block modeled to obtain a canonical transformation to an automaton.
Fig. 3 shows the result of applying TT oAutomaton to the above code specification. Note that the transition for the else block (lower half in the figure) has no action. The semantics of this automaton and the initial code specification are equivalent.
The output of this transformation satisfies the property: All the components are specified using a state automaton. In case the input already satisfies this property the transformation behaves as the identity transformation.
3) NoVal resolution: As described in Section II-C, AF3 ports can have one more value: NoVal, than the corresponding type in the model checker.
To take this discrepancy into account, for each port p we add a boolean port p P RESEN T whose value denotes whether the port is carrying a value or not. This also requires that we change the behavior of the state automaton. This transformation is also a chain of 2 transformations:
TNoV al = TUpdateT ransitions; TResolveNoV al TUpdateT ransitions: If a port is not explicitly assigned a value in a transition it should carry NoVal. This transformation makes this step explicit, i.e., we transform the transitions to explicitly assign NoVal to ports which are not assigned a value.
TResolveNoV al: This transformation adds the PRESENT port and updates the transitions such that for every port p which is assigned a value, p P RESEN T is assigned true, otherwise p P RESEN T is assigned false (in this case p is assigned a default value of the type). The guards of the transitions are also transformed accordingly. This is done to ensure that after this transformation no NoVal can flow through the model.
The absence of a value is interpreted using the value of the
TArray is again a chain of two transformations: 1) TT oStructT ype: transforms array types to structure types by creating a structure member for each element of the array. This transformation also changes the type of the array variables to the corresponding structure type. It is to be noted that after this transformation the model could be inconsistent, as the expressions involving the ports would still be array expressions but the port type has changed to the Structure type. 2) TT oStructExpression: transforms array expressions to structure expressions. It converts an array access to a structure access, and also transforms the array constants to structure constants.
Fig. 5 shows the result of applying TArray on the automaton in Fig. 4.
The output of this transformation satisfies the following property: The model does not contain arrays.
TF latten flattens the structures, i.e., 1) creates a variable definition for each member of a structure variable definition, 2) converts the expressions involving structure variable to semantically equivalent flattened expressions. It is defined as a chain of three transformations: 1) TF lattenExpression: flattens the structure expressions, e.g., an expression x == y, will be converted to a conjunction of a list of equality expressions of the form x:f ieldi == y:f ieldi. 2) TT oNonStructExpressions: replaces the flattened expression with member access to the corresponding variable created for the structure member. The model is inconsistent after this transformation. 3) TflattenV ariableDefinitions: flattens a variable definition, i.e., creates a variable for each member of a structure variable.
The output of this transformation satisfies the property: The model does not contain structures.
Note that the decomposition in modular transformations
enables the handling of nested arrays and structures in an easy
manner, a feature which was not supported in [
II-C, AF3 supports two kinds of causalities: strong and weak. We convert the strongly causal components to weakly causal components and add a delay, which can be seen as transforming a Moore machine to a Mealy machine. This allows us to reuse the transformation of a weakly causal atomic component to the model checker.
The approach is as follows: 1) add a state variable for every output port, 2) assign each of these state variables the value which was assigned to the corresponding output port, and 3) assign the values of these state variables to output ports.
Fig. 7 shows the result of applying TCausality on the automaton in Fig. 6.
Once this chain of transformations is executed our AF3 model is considered normalized. It has the following properties: 1) All variable, component, transition, function, etc. names are unique. 2) All atomic components are specified as state automata. 3) All ports carry a value. 4) The model contains only simple types, i.e., no arrays or structures. 5) All components are weakly causal.
The normalized component can be transformed to a nuXmv module in an easier way. Note that it is still not a canonical transformation.
The second top level transformation TnuXmv transforms a normalized AF3 model to a nuXmv model. The first step generates a nuXmv model, and the second one is a model-totext transformation which is straightforward and therefore not discussed in this paper.
NuXmv
Module
Module parameter Define (a named expression)
State variable Not transformed explicitly
Define (a named expression) 1) transition (T RAN S) constraint
for state variable 2) case statement for output ports
TABLE I
MAPPING OF AF3 AND NUXMV ELEMENTS
This transformation seems counterintuitive, but it was designed this way as the intuitive transformation is erroneous in the case of non-deterministic automata. As an example, consider a component with a boolean output port o and behavior expressed as the state automaton given in Fig. 8. There is a non-determinism between T 1 and T 2. Intuitively, this automaton would be transformed to: DEFINE o : = c a s e ( s = s 1 ) & TRUE : TRUE ; ( s = s 1 ) & TRUE : FALSE ; e s a c ; T1
T2 TRANS ( s = s 1 & TRUE ) TRANS ( s = s 1 & TRUE ) > n e x t ( s ) = s 2 ; > n e x t ( s ) = s 3 ;
Here, although the next state of the automaton might be
s3 (i.e., T 2 is executed), o will be always assigned T RU E
(corresponding to the case T 1) as it is the first satisfying
case. This kind of description leads to outputs being updated
incorrectly in case of non-determinism, which precisely was
a bug in [
Modeling the chosen transition explicitly instead of inferring it from the change in state enables us to solve this issue. Instead of modeling the automaton as evolution of states, we model it as a sequence of transitions. Our transformation specifies the automaton in Fig. 8 as: DEFINE o : = c a s e ( t = T1 ) : TRUE ; ( t = T2 ) : FALSE ; e s a c ;
Here, outputs are updated correctly depending on which transition is taken. Note that the transition is initialized with dummy val; it is necessary as there is no initial transition of a state automaton.
We now briefly describe the technicalities of this transformation. Let us consider a state automaton with states S , transitions T , where each transition consists of a guard and a set of actions fT 2 T = (Tguard; Tactions)g, each action is of the form v := e. Sin T , and Sout T denote the set of incoming and outgoing transitions for the state S 2 S . t is a nuXmv variable representing the transition chosen for execution. Now we describe the module specification.
We generate the following sets of transition constraints: fT RAN S t 2 Sin ! next(t) 2 Sout jS 2 Sg fT RAN S t = T ! execute(Tactions)j T : T g execute(tactions)
fnext(v) := e j (v := e) 2 Tactionsg
fI N V AR t = T ! Tguard j T : T g
An output port op transformed to a define op0 is assigned a value given by a case expression with cases
ft = T ! Tactions[op0]:valueg where Tactions[op0]:value represents the value assigned to op0 in the transition actions for the transition T .
We also initialize the automaton with INIT constraint, with initial values of the state variables.
The user needs to observe a trace returned by the model checker in AF3. A counterexample trace is a sequence of trace steps at the nuXmv level: each trace step assigns a value to every variable of the analysed nuXmv module. For usability, we need however to express this trace back in a sequence at the AF3 level: we should assign values to AF3 ports. Consequently, we should transform nuXmv variables back to AF3 variables. Intuitively, we should reuse the forward transformation to ensure that both transformations are always coherent. Both transformations go however in opposite directions, so it is not possible to use the same transformation trivially.
We actually need on one hand to transform AF3 ports into nuXmv variables (to reuse the transformation), and on the other hand to transform nuXmv valuations into AF3 ones (to lift the results back at the user level). To do so, we introduce a symbolic operator [e] denoting the evaluation of an expression e in (a given step of) the trace. The concrete evaluation of this operator is trivial for nuXmv variables, e.g., evaluating [ip40] is as simple as reading its value in the trace. Our objective is however to find out the concrete evaluation of this operator for AF3 ports, e.g., [ip]. We therefore need to express the evaluation of an AF3 port in terms of the (trivial) evaluation of a nuXmv variable. This can be achieved simply by applying the following subsequence of the original transformation to this epxression:
TCE = TName; TNoV al; TP roductT ypes
Note that not all transformations are necessary here, e.g., the transformation TCodeSpec (Section III-A2) is irrelevant for the counterexample interpretations as this transformation deals only with representation of the component’s behavior. We therefore do not use it in our counterexample transformation. However, the transformation TNoV al (Section III-A3) changes the behavior of the component and affects how the port values are interpreted, and therefore is a part of the composition chain.
We support LTL formulas in the form of verification patterns, and also LTL contracts in the form of assume-guarantee expressions. Here as well we reuse a part of the chain T (eqn. 1, 2) for transforming specifications.
TSpec = TNames; TNoV al; TP roductT ypes; TnuXmv
Always (op 6= N oV al && op) G(op 24 P RESEN T & op 24)
As a case study we successfully ran various formal
verification checks: state reachability, non-determinism, port bound
violation checks, on a model of a pick and place unit (PPU)2
[
4) Crane: Used for picking and placing work pieces between above 3 stations.
Work pieces can be metallic or black plastic. The PPU picks up the work piece from the stack and processes it. The crane picks up a work piece from the stack. If the work piece is black plastic it is transported to the ramp, if it is metallic then it is transported to the stamp: where it is stamped, and then the stamped piece is transported to the ramp by the crane.
The PPU model in AF3 is a big model which uses a wide range of features provided by AF3: both strong and weak causalities, product types, user defined functions, code specifications, state automatons. We checked state reachability, non-determinism and ports’ bound violation on this model. We found that in particular stamp automaton was nondeterministic.
The closest related work to our approach is the older
implementation of formal verification support for AutoFOCUS3
[
mbeddr [
Simulink Design Verifier4, Scade Suite5, Dezine6 are professional tools which support formal analyses requiring a behavioral transformation but their details are not public for comparison.
The work [
4https://www.mathworks.com/ 5http://www.esterel-technologies.com/ 6http://www.verum.com/ not supports reverse transformation (note in addition that this is a master thesis written in German).
A transformation from a DSL to Event-B [
The GEMOC7 initiative aims at the conceptual globalization of modeling languages. They target the automated processing of heterogeneous modeling languages, and provide framework for coordinated execution. Even though dealing with execution semantics at different levels of abstraction, the approach used to solve the problem is not based on model transformation and therefore not relevant for our work.
We have implemented the transformation of AutoFOCUS3 models to nuXmv models. We have used this transformation to apply formal verification on model of a pick and place unit.
This complex transformation provides new insights on what is required by a model transformation such that it can be reused with ease. In fact, systematizing model transformation reuse is one of our future work which would be useful for the community. Secondly, we plan work on reasoning about the model transformations: find a set of properties we can verify, and find (or define if needed) a language suitable to express such properties.
Acknowledgments. This work builds on top of the work
done by Daniel Ratiu who implemented the original
transformation of [