Modular transformation from AF3 to nuXmv Sudeep Kanav, Vincent Aravantinos fortiss GmbH Guerickestr. 25 80805 Munich, Germany Email: {last name}@fortiss.org Abstract—AutoFOCUS3 (AF3) [1] supports formal verification The paper is structured as follows: Section II presents AF3 of its models using the nuXmv [2] model checker. This requires and nuXmv, Section III describes our transformation, Section a model transformation from AF3 to nuXmv models. In this IV describes a use case, Section V considers the related work, paper we present this behavior transformation. It is a two way transformation between a high-level and a low-level model and Section VI concludes this paper. involving intricate cases typical of behavior transformations whose solutions can therefore be beneficial to the community. II. BACKGROUND In this section we give an overview of AF3 [1] and provide a brief introduction to the concepts needed to understand the I. I NTRODUCTION paper. We then give an introduction to nuXmv [2], and lastly we list down the challenges which make this solution useful Model driven Engineering (MDE) allows us to model the and non trivial. system: its requirements, behavior, target platform, and gen- erate code out of this model which can be deployed on the A. AutoFOCUS3 introduction system. The behavior model of the system can be used for AutoFOCUS3 [1] is a model-based development tool for early verification, thus detecting bugs at an early stage of embedded systems, which provides support for most develop- development, thereby saving time and money. ment phases: requirements engineering, software architecture, One way to perform verification is using formal methods, hardware architecture, as well as mapping between the artifacts which are useful when we need high assurance, but are hard of these various phases. C and Java code can be generated to use. They are however difficult to integrate with MDE tools from the developed model after the architecture and behavior because it requires a behavior transformation from a high-level are fully defined. MDE model to a low-level model of the formal analysis tool. AutoFOCUS3 (AF3) [1], is an MDE tool which supports formal verification of its models. We use the nuXmv [2] (successor of NuSMV [3]) model checker for formal analyses. We transform AF3 models to nuXmv models, run model checking on them, interpret the result, and simulate the model checker trace, if available. In this paper we present the details of this model transfor- mation. We believe this is useful to the community because it points out pitfalls that one typically encounters while de- veloping 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, ex- tensible 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 Fig. 1. Component architecture in AutoFOCUS3 finally that we have applied this solution to an industrial use case. This paper concerns the software architecture, whose fol- This transformation is a complete rebuild of the one in- lowing characteristics are essential for formal verification: formally presented in [4] covering a larger fragment, fixing • Component-based: Software architecture in AF3 is a important limitations of the previous transformation and de- hierarchy of components communicating with each other signed in a modular manner. through typed channels (Fig. 1) which are connected to ports. Ports, which can be input or output, form the ports are updated in the next clock tick, whereas in a weakly interface of the component. Each port carries values of a causal component output ports are updated in the same tick. defined type (no objects: only booleans, integers, doubles, The strongly causal components can be seen as Moore enumerations, or combinations thereof). Channels in AF3 machines: the output of the current tick is only dependent are statically fixed. on the state and not on the input, input can only influence Atomic components, if implemented, contain a behavior the output of the next tick (we can also see it as input only specification modeled by a state machine or code ex- changing the state, which in turn affects the output). Weakly pressed in a very simple language.1 causal components can be interpreted as Mealy machines: • Formal execution semantics: The semantics of compo- output is dependent on both the state and the input. nents is formally defined according to the FOCUS model As nuXmv does not have the notion of strong and weak of computation [5], i.e., a global clock is assumed and all causality this needs to be additionally handled. components are (in a nutshell) synchronously executed. User defined functions: AF3 also supports the use of func- One can then simulate their component architecture in tions defined by the user in a Data Dictionary. These functions AF3 according to these semantics. are stateless and use the same simple language which can be used to define a component’s behavior. These are not B. nuXmv part of the transformed component’s tree, but are contained nuXmv [2] is a symbolic model checker. We now describe in a separate subtree. Note that we do not describe this the features which we use for the formal verification of an transformation in the paper. AF3 component. In nuXmv, a system is modeled as a finite state machine III. T RANSFORMATION DESCRIPTION (FSM) described in terms of variables and constraints. Vari- We decompose the transformation in small step transforma- ables, which can be state variables or input variables, can tions. These transformations are then executed sequentially: have different values in different states. Constraints are used the output of the first transformation is the input of the next. to describe 1) transition relations: how a state machine evolves We denote the sequential composition by ”;”: applying T1 ; T2 during execution, 2) initial state, 3) invariants. It also supports on I means that first T1 is applied on I, and then T2 is applied hierarchical descriptions. on its output. Three types of specifications are supported: LTL, CTL, and This decomposition allows the small step transformations INVAR (invariants). The definition of the FSM, specifications, (or blocks) to be reused in different contexts, e.g., for the and declarations (input variables, state variables, constants, and reverse transformation (which was not possible in [4]). The define) are encapsulated in a module declaration. transformations are implemented in Java. A module can be then instantiated inside another module. As a running example, we consider a component C, with Every nuXmv program must contain a main module. The main input port ip which is a boolean array of size 2, and a boolean module does not have any parameters and is the entry point output port op which is true if both values are equal in the of the nuXmv model. input array. The behavior of the component is specified using C. A non-trivial transformation a code specification: The transformation from AF3 to nuXmv models is not i f ( ip [0]== ip [ 1 ] ) trivial as it transforms a model at a high level of abstraction { op : = t r u e ; } to one at a lower level of abstraction. We now describe some AF3-specific notions which make the transformation It is a strongly causal component, which means that the challenging. output values are updated on the next tick. NoVal: AF3 allows to model situations where a channel is At the top level, transformation of an AF3 model to a not carrying a value. This is required when modeling events, nuXmv model T is a chain of 2 transformations 1) normal- e.g., a user pressing the brake in a car. We could also see ization of the model, 2) transformation to nuXmv: it as a null value. This situation is modeled using a special T = TN orm ; TnuXmv (1) 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 compo- Fig. 2. Transformation from AF3 to nuXmv model nent as strong or weak. In a strongly causal components output 1 Note that behavior can also be expressed using tables, but this feature is Fig 2 shows this chain in a pictorial form. From now on we deprecated at the moment. describe chains using only the ”;” operator. A. Transformation normalizing the project The output of this transformation satisfies the property: All This transformation takes an AF3 model and transforms it the components are specified using a state automaton. In case into a normalized AF3 model, which is easier to transform to the input already satisfies this property the transformation a nuXmv model. It is a chain of 5 transformations: behaves as the identity transformation. 3) NoVal resolution: As described in Section II-C, AF3 TN ormalize = TN ames ; TCodeSpec ; TN oV al ports can have one more value: NoVal, than the corresponding (2) ; TP roductT ypes ; TCausality type in the model checker. Note that (1) and (2) will be reused in Section III-C. To take this discrepancy into account, for each port p 1) Name transformation: TN ame changes the names of the we add a boolean port p P RESEN T whose value denotes artifacts by appending their internal id, and removing white whether the port is carrying a value or not. This also requires spaces and special characters. The references to these elements that we change the behavior of the state automaton. This are also transformed. The example is then transformed to: transformation is also a chain of 2 transformations: i f ( ip 40 [0]== ip 40 [ 1 ] ) TN oV al = TU pdateT ransitions ; TResolveN oV al { op 24 : = t r u e ; } TU pdateT ransitions : If a port is not explicitly assigned a value 2) Code specification to state automaton: TCodeSpec turns in a transition it should carry NoVal. This transformation a behavior of an atomic component, in case it is specified as makes this step explicit, i.e., we transform the transitions to a code specification, into a state automaton. explicitly assign NoVal to ports which are not assigned a value. A code specification in AF3 is stateless, so it is transformed TResolveN oV al : This transformation adds the PRESENT port to an automaton with a single state, where each if (and else) and updates the transitions such that for every port p which is block is converted to a transition. TCodeSpec is again a chain assigned a value, p P RESEN T is assigned true, otherwise of 2 transformations: 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 TCodeSpec = TN ormalizeCodeSpec ; TT oAutomaton also transformed accordingly. This is done to ensure that after TN ormalizeCodeSpec outputs a code specification which is this transformation no NoVal can flow through the model. behaviorally equivalent to the input and in a normalized The absence of a value is interpreted using the value of the form from which we can do a canonical transformation to PRESENT port. a state automaton, and TT oAutomaton performs this canonical transformation. Applying TN ormalizeCodeSpec on the above code specifica- tion results in the following code specification: i f ( ip 40 [0]== ip 40 [ 1 ] ) { op 24 : = t r u e ; return ;} else{ return ;} Note the addition of the empty else block modeled to obtain a canonical transformation to an automaton. Fig. 4. Result of applying TN oV al Fig. 3 shows the result of applying TT oAutomaton to the Fig. 4 shows the result of applying TN oV al on the state above code specification. Note that the transition for the else automaton in Fig. 3. block (lower half in the figure) has no action. The semantics of The output of this transformation satisfies the property: this automaton and the initial code specification are equivalent. Every channel carries a value. 4) Product types to simple types: This transformation con- verts arrays and structures to simple types and correspondingly transforms the variable definitions and expressions. This transformation is a chain of two transformations : 1) TArray : transforms arrays to structures, 2) TF latten : flattening of structures and their expressions. TP roductT ypes = TArray ; TF latten 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 Fig. 3. Result of applying TT oAutomaton array. This transformation also changes the type of the array variables to the corresponding structure type. It is to The output of this transformation satisfies the property: The be noted that after this transformation the model could be model does not contain structures. inconsistent, as the expressions involving the ports would Note that the decomposition in modular transformations still be array expressions but the port type has changed enables the handling of nested arrays and structures in an easy to the Structure type. manner, a feature which was not supported in [4]. 2) TT oStructExpression : transforms array expressions to 5) Causality transformation: As described in subsection structure expressions. It converts an array access to a II-C, AF3 supports two kinds of causalities: strong and weak. structure access, and also transforms the array constants We convert the strongly causal components to weakly causal to structure constants. components and add a delay, which can be seen as transform- ing 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. 5. Result of applying TArray 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 Fig. 7. Result of applying TCausality a chain of three transformations: 1) TF lattenExpression : flattens the structure expressions, Fig. 7 shows the result of applying TCausality on the e.g., an expression x == y, will be converted to a automaton in Fig. 6. conjunction of a list of equality expressions of the form After the execution of this transformation all the components x.f ieldi == y.f ieldi . are weakly causal. 2) TT oN onStructExpressions : replaces the flattened expres- sion with member access to the corresponding variable created for the structure member. The model is inconsis- Once this chain of transformations is executed our AF3 tent after this transformation. model is considered normalized. It has the following prop- 3) Tf lattenV ariableDef initions : flattens a variable definition, erties: 1) All variable, component, transition, function, etc. names i.e., creates a variable for each member of a structure are unique. variable. 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. B. Transformation to NuXmv The second top level transformation TnuXmv transforms Fig. 6. Result of applying TF latten a normalized AF3 model to a nuXmv model. The first step generates a nuXmv model, and the second one is a model-to- Fig. 6 shows the result of applying TF latten on the automa- text transformation which is straightforward and therefore not ton in Fig. 5. discussed in this paper. AutoFOCUS3 NuXmv Component Module −> n e x t ( t ) i n {T1 , T2 } ; InputPort Module parameter OutputPort Define (a named expression) INVAR ( t = T1 ) −> t r u e −− g u a r d o f T1 Transition State variable INVAR ( t = T2 ) −> t r u e −− g u a r d o f T2 State Not transformed explicitly Guard Define (a named expression) Here, outputs are updated correctly depending on which Action 1) transition (T RAN S) constraint for state variable transition is taken. Note that the transition is initialized with 2) case statement for output ports dummy val; it is necessary as there is no initial transition of TABLE I M APPING OF AF3 AND NU X MV ELEMENTS a state automaton. We now briefly describe the technicalities of this trans- formation. Let us consider a state automaton with states S, transitions T , where each transition consists of a guard and Table I shows the mapping of AF3 elements to the nuXmv a set of actions {T ∈ T = (Tguard , Tactions )}, each action elements. Note that the transitions are transformed to state is of the form v := e. Sin ⊆ T , and Sout ⊆ T denote the variables, and not the states. set of incoming and outgoing transitions for the state S ∈ 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: {T RAN S t ∈ Sin → next(t) ∈ Sout |S ∈ S} {T RAN S t = T → execute(Tactions )| T : T } Fig. 8. Example state automaton where This transformation seems counterintuitive, but it was de- execute(tactions ) ≡ {next(v) := e | (v := e) ∈ Tactions } signed this way as the intuitive transformation is erroneous We generate the following set of invariants: in the case of non-deterministic automata. As an example, consider a component with a boolean output port o and {IN V AR t = T → Tguard | T : T } behavior expressed as the state automaton given in Fig. 8. An output port op transformed to a define op0 is assigned a There is a non-determinism between T 1 and T 2. Intuitively, value given by a case expression with cases this automaton would be transformed to: {t = T → Tactions [op0 ].value} DEFINE o : = c a s e ( s = s 1 ) & TRUE : TRUE ; −− T1 where Tactions [op0 ].value represents the value assigned to op0 ( s = s 1 ) & TRUE : FALSE ; −− T2 in the transition actions for the transition T . esac ; We also initialize the automaton with INIT constraint, with initial values of the state variables. TRANS ( s = s 1 & TRUE) −> n e x t ( s ) = s 2 ; TRANS ( s = s 1 & TRUE) −> n e x t ( s ) = s 3 ; C. Counterexample transformation The user needs to observe a trace returned by the model Here, although the next state of the automaton might be checker in AF3. A counterexample trace is a sequence of s3 (i.e., T 2 is executed), o will be always assigned T RU E trace steps at the nuXmv level: each trace step assigns a (corresponding to the case T 1) as it is the first satisfying value to every variable of the analysed nuXmv module. For case. This kind of description leads to outputs being updated usability, we need however to express this trace back in a incorrectly in case of non-determinism, which precisely was sequence at the AF3 level: we should assign values to AF3 a bug in [4]. ports. Consequently, we should transform nuXmv variables Modeling the chosen transition explicitly instead of infer- back to AF3 variables. Intuitively, we should reuse the for- ring it from the change in state enables us to solve this issue. ward transformation to ensure that both transformations are Instead of modeling the automaton as evolution of states, always coherent. Both transformations go however in opposite we model it as a sequence of transitions. Our transformation directions, so it is not possible to use the same transformation specifies the automaton in Fig. 8 as: trivially. DEFINE o : = c a s e We actually need on one hand to transform AF3 ports into ( t = T1 ) : TRUE ; −− T1 nuXmv variables (to reuse the transformation), and on the ( t = T2 ) : FALSE ; −− T2 other hand to transform nuXmv valuations into AF3 ones (to esac ; lift the results back at the user level). To do so, we introduce a symbolic operator [e] denoting the evaluation of an expression TRANS t i n { dummy val } 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 = TN ame ; TN oV al ; TP roductT ypes Table II shows how this expression for the input port ip of our running example is transformed by TCE . Fig. 9. Components of the PPU [6] Transformation Result -Input- [ip] TN ame [ip 40] 3) Stamp: Used to stamp work pieces. TN oV al [ip 40 P RESEN T ] ? [ip 40] : N oV al; 4) Crane: Used for picking and placing work pieces between TP roductT ypes [ip 40 P RESEN T ] ? [[ip 40 elem0], [ip 40 elem1]] above 3 stations. : N oV al; Work pieces can be metallic or black plastic. The PPU picks TABLE II up the work piece from the stack and processes it. The crane I NTERMEDIATE RESULTS OF THE COUNTEREXAMPLE TRANSFORMATION 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 Note that not all transformations are necessary here, e.g., it is transported to the stamp: where it is stamped, and then the transformation TCodeSpec (Section III-A2) is irrelevant for the stamped piece is transported to the ramp by the crane. the counterexample interpretations as this transformation deals The PPU model in AF3 is a big model which uses a only with representation of the component’s behavior. We wide range of features provided by AF3: both strong and therefore do not use it in our counterexample transformation. weak causalities, product types, user defined functions, code However, the transformation TN oV al (Section III-A3) changes specifications, state automatons. We checked state reacha- the behavior of the component and affects how the port values bility, non-determinism and ports’ bound violation on this are interpreted, and therefore is a part of the composition model. We found that in particular stamp automaton was non- chain. deterministic. D. Specifications V. R ELATED W ORK We support LTL formulas in the form of verification pat- The closest related work to our approach is the older im- terns, and also LTL contracts in the form of assume-guarantee plementation of formal verification support for AutoFOCUS3 expressions. Here as well we reuse a part of the chain T (eqn. [4]. Our solution is modular, of a better quality (fixed known 1, 2) for transforming specifications. bugs), supporting more features: product types, user defined functions, support for different causalities, and better support TSpec = TN ames ; TN oV al ; TP roductT ypes ; TnuXmv for counterexample simulation. As an example, a specification mbeddr [7] also supports formal verification using CBMC3 on the generated C code, however, it is not a high-level to Always (op 6= N oV al && op) low-level transformation, as the input to CBMC is C code. is transformed to Simulink Design Verifier4 , Scade Suite5 , Dezine6 are pro- fessional tools which support formal analyses requiring a G(op 24 P RESEN T & op 24) behavioral transformation but their details are not public for IV. U SE C ASE comparison. The work [8] describes a two step transformation from As a case study we successfully ran various formal verifi- Scade to SMT for the purpose of verification. The first cation checks: state reachability, non-determinism, port bound step transforms a Scade model to an intermediary language violation checks, on a model of a pick and place unit (PPU)2 (called LAMA) program, and second step transforms a LAMA [6] presented in Fig. 9. A PPU picks a work piece from one program to SMT. This transformation is not modular and does place and places it at another place, as shown in Fig. 9: 1) Stack: Input storage of work pieces. 3 http://www.cprover.org/cbmc/ 2) Ramp: Output storage for work pieces. 4 https://www.mathworks.com/ 5 http://www.esterel-technologies.com/ 2 www.ppu-demonstrator.org 6 http://www.verum.com/ not supports reverse transformation (note in addition that this [9] J.-R. Abrial, Modeling in Event-B: system and software engineering. is a master thesis written in German). Cambridge University Press, 2010. [10] U. Tikhonova, M. Manders, M. Brand, S. Andova, and T. Verhoeff, A transformation from a DSL to Event-B [9] is described “Applying model transformation and Event-B for specifying an in [10]. This transformation targets a DSL, whereas AF3 is industrial DSL,” pp. 41–50. [Online]. Available: http://ceur-ws.org/ more general and has a wider area of application. Secondly, Vol-1069/07-paper.pdf this transformation does not support reverse transformation, instead the DSL program is simulated in a simulator for 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. VI. C ONCLUSION 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 transfor- mation of [4]. R EFERENCES [1] V. Aravantinos, S. Voss, S. Teufl, F. Hölzl, and B. Schätz, “AutoFOCUS 3: Tooling concepts for seamless, model-based development of embedded systems,” in ACES-MB&WUCOR@ MoDELS, 2015, pp. 19–26. [Online]. Available: http://ceur-ws.org/Vol-1508/paper4.pdf [2] R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, and S. Tonetta, “The nuXmv Symbolic Model Checker,” in CAV, 2014, pp. 334–342. [Online]. Available: http://dx.doi.org/10.1007/978-3-319-08867-9 22 [3] A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri, “NUSMV: A new symbolic model verifier,” in CAV, 1999, pp. 495–499. [Online]. Available: http://dx.doi.org/10.1007/3-540-48683-6 44 [4] A. Campetelli, F. Hölzl, and P. Neubeck, “User-friendly model checking integration in model-based development,” in CAINE, 2011. [5] M. Broy and K. Stølen, Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement. Springer New York, 2001. [Online]. Available: https://books.google.de/books? id=A13SBNBSUIsC [6] B. Vogel-Heuser, C. Legat, J. Folmer, and S. Feldmann, “Researching evolution in industrial plant automation: Scenarios and documentation of the pick and place unit,” Technische Universität München, Tech. Rep., 2014. [7] M. Voelter, D. Ratiu, B. Schätz, and B. Kolb, “mbeddr: an extensible c-based programming language and IDE for embedded systems,” in SPLASH, 2012, pp. 121–140. [Online]. Available: http://doi.acm.org/10.1145/2384716.2384767 [8] H. Basold, “Transformation von scade-modellen zur smt-basierten verifikation,” CoRR, vol. abs/1403.2752, 2014. [Online]. Available: http://arxiv.org/abs/1403.2752 7 http://gemoc.org