=Paper=
{{Paper
|id=Vol-2308/aviose2019paper02
|storemode=property
|title=Test Sequence Generation From Formally Verified SysML Models
|pdfUrl=https://ceur-ws.org/Vol-2308/aviose2019paper02.pdf
|volume=Vol-2308
|authors=Pierre de Saqui-Sannes,Ludovic Apvrille
|dblpUrl=https://dblp.org/rec/conf/se/Saqui-SannesA19
}}
==Test Sequence Generation From Formally Verified SysML Models==
https://ceur-ws.org/Vol-2308/aviose2019paper02.pdf
Test Sequence Generation From Formally Verified SysML Models
Pierre de Saqui-Sannes Ludovic Apvrille
ISAE-Supaero LTCI, Telecom ParisTech, Université Paris Saclay
10 Avenue Emile blouin 46 rue Barrault
31400 Toulouse, France 75013 Paris, France
Email: Pierre.De-saqui-sannes@isae-supaero.fr Email: ludovic.apvrille@telecom-paristech.fr
Abstract—Test generation has been acknowledged as a cost- obtain a set a test sequences. Associated algorithms have been
prone activity reducing productivity and time to market. The implemented in the free and open-source tool named TTool
expected benefits of Model Based Systems Engineering include [10].
automated generation of test sequences from models. The paper
proposes verification solutions for the System Modeling Lan- The paper is organized as follows. Section II introduces
guage (SysML). In particular, the paper shows how to link SysML and more precisely the block instance and state ma-
test generation to formal verification. The proposed algorithms chine diagrams. Section III presents a verification by abstrac-
are implemented by the free software TTool. Two case studies tion approach for SysML models. Section IV uses the output
support discussion on conformance and interoperability testing, of the verification process to generate test sequences. Section
respectively.
V applies the proposed approach to a client/server protocol
I. INTRODUCTION and discusses interoperability testing. Section VI uses a UAV
in charge of taking pictures to address conformance testing.
The widespread of Model Based System Engineering ap-
Section VII surveys related work. Section VIII concludes the
proaches [1] has encouraged several communities to de-
paper and outlines future work.
velop their own modelling language. For instance, the Ob-
ject Management Group (OMG) [2] and the International
II. S YS ML
Council for Systems Engineering (INCOSE) [3] have jointly
developed and standardized the Systems Modeling Language The SysML standard [3] defines nine type of diagrams that
(SysML) [4]. The benefits and potential of using SysML may be used inside one model to cover the requirement cap-
have been acknowledged in several application domains, in ture, analysis and design phases in the trajectory of systems.
particular avionics [5], [6], [27]. SysML is now supported by For the test generation approach discussed in the paper, only
proprietary [7], [8] and open-source tools like Papyrus1 or the design phase is of interest.
TTool2 that help automating an important variety of activities During the design phase, one defines the architecture of the
(e.g. [9]) throughout the design trajectory of complex systems. system and the behaviors of the blocks the architecture is
One of these activities is test sequence generation, an activity made up of. The SysML standard defines two architectural
that is cost-prone and time consuming, and therefore worth design diagrams: the Block Definition Diagram (BDD) and
being automated to reduce time to market of complex systems. the Internal Block Diagrams (IBD) of the SysML standard. In
Automated test generation from SysML models has already the paper, we use the version of SysML supported by TTool
been discussed in [10], [11], [12]. The paper proposes another where the BDD and IBD are merged into one diagram: the
SysML-approach based on earlier work with the Formal De- Block Instance Diagram (BID). Each block instance has a
scription Technique Estelle [13]. behavior expressed in the form of a SysML state machine
In brief, the reachability graph of the SysML model is com- diagram.
puted directly from the block instance diagram that defines the
architecture of the system and from the state machine diagrams A. Block Instance Diagram
that define the behaviors of the block instances. The transitions A Block Instance Diagram is a tripartite graph with one
of the graph are labelled using the messages exchanged by type of nodes, each one defining a block instance, and two
pairs of block instances. This transforms the reachability types of relations. First, the ”composition” relation of SysML
graph of the SysML model into a Labeled Transition System. (black diamond) enables to say that one block instance is
Theories developed for LTS [16] therefore apply, in particular made up of one or several block instances. Second, the
minimization that outputs a quotient automaton computed ”connect” relation connects two ports used for exchanging
with respect to an equivalence relation such as Milner’s signals. For simplicity, the below definitions address the
observational equivalence [17]. Taking a quotient automaton ”connect” relation, not the ”composition” one.
as input, all the paths of maximal size leading to a termination
state are computed using the Dijkstra technique (22) to finally Definition: block instance. A block instance is a 4-uple
1 Papyrus: https://www.eclipse.org/papyrus/ (id, al, ml, pl, isl, osl) where:
2 TTool: https://ttool.telecom-paristech.fr/ • id is a String that names the block instance.
AvioSE 2019: 1st Workshop on Avionics Systems and Software Engineering @ SE19, Stuttgart, Germany 67
• al is an attribute list. The attribute types include Integer, Thus, it heavily depends on the experience of the user of
Boolean, Timer, and user-defined Records. An attribute the simulator, or on the random generator of that simulator.
may be defined with an initial value. Conversely, formal verification relies on mathematics rather
• ml is a method list. than chance.
• pl is a port list.
A. Working Hypothesis
• isl is an input signal list.
• osl is an output signal list. The verification approach discussed in this section requires
exploring the state space of the SysML and more precisely
Definition: Block Instance Diagram. A Block Instance generating (a sub part of) the graph of states that may be
Diagram is a 3-uple (Blk, connect, assoc) where: reached from the initial state of the system. Full generation
of the reachability graph of the SysML model explores all the
• Blk is a set of block instances.
execution paths the system may go through starting from its
• connect is a function Port → Port that connects pairs of
initial state. The graph enables checking the system against
ports.
reachability properties (using the model-checker we have
• assoc is a function (BlkxSignal) → (BlockxSignal) that
integrated into TTool). Also, when a property to investigate
associates one signal of block B1 to one signal of block
is the reachability of a given state, then the graph generation
B2, making it possible to compose the state machines
stops as soon as the property is satisfied (on-the-fly model-
belonging to B1 and B2. Here, the term compose denotes
checking).
a composition in the usual sense of finite state machine
As usually, reachability analysis faces the state space explosion
composition, not the composition relation supported de-
problem. Starting from now, the following hypothesis applies:
picted by a black diamond in SysML.
the reachability graph of the SysML model may be entirely
Finally, a Block Instance Diagram depicts the architecture of built within an acceptable amount of time and memory.
a system as a graph of interconnected blocks.
B. Labeled Reachability Graph
B. State Machine Diagram
In this section, we assume the SysML model is composed
Each block instance contains one extended state finite state of one block instance diagram and one state machine diagram
machine that supports states, transitions, attribute settings, in- per block instance. Other diagrams of the SysML model are
puts and outputs operations on signals, and time manipulation. ignored since they do not play any role in the reachability
Definition: State Machine. An extended finite state machine graph construction process.
depicted by a SysML state machine diagram is bi-partite graph
(s0, S, T ) where Definition: Labeled Reachability Graph. The Labeled
• S is a set of states (s0 is the initial state). Reachability Graph (LRG) of a SysML model is a 5-uple LRG
• T is a set of transitions. = (S, Σ, Θ, ∆, s0 ) where:
• S denotes the countable number of global states of the
Definition: State Transition. A transition in a state machine SysML model
is a 5-uple (sstart , a f ter, condition, Actions, send ) where: • Σ is a countable set of observable events included in the
• sstart is the initial state of the transition. list of signals exchanged on ports. Thus we have Σ ⊆
• a f ter(tmin,tmax) enables firing the transition after at ”!”Ao (p) ∪ ”?”Ai (p) ∪ ”!”So (p) ”?”Si (p)) where:
least between tmin and tmax units of time have elapsed. – ”!” and ”?” respectively denote an emission and a
• condition is a Boolean expression that conditions the reception.
execution of the transition. A condition may use attributes – Ao (p) is an output signal connected to an asyn-
of its corresponding block. chronous channel.
• Actions is a ordered set of action. These actions can be – Ai (p) is an input signal connected to an asyn-
executed only once the transition has been enabled i.e. the chronous channel.
a f ter clause has elapsed and the condition equals true. – So and S1 are output and input signals connected via
• send is the final state of the transition. a synchronous channel.
A state machine cannot contain parallel states, historic state, – p denotes a list of attributes of the block to which
fork and join states. These behaviors can easily be replaced the signal sending/receiving corresponds.
by counterparts. e.g. using sub-blocks and synchronous signals • Θ is a countable set of internal events, e.g. the assignation
for each parallel activity. of an attribute. Thus we have Θ ⊆ i(a =< expr >) ∨ i()
where a is an attribute.
III. FORMAL VERIFICATION • ∆ ⊆ Sx(Σ ∪ Θ)xS denotes the set of labeled transitions in
Adding a state machine to each block instance makes the the reachability graph. A label contains the name of the
model an executable one. Interactive simulation enables early signal exchanged by one pair of block instances or the
checking of the state machines against design errors. It does identification of the internal action, i.e. i(...). An empty
not necessarily explore the entire state space of the model. i() transition is sometimes denoted τ.
AvioSE 2019: 1st Workshop on Avionics Systems and Software Engineering @ SE19, Stuttgart, Germany 68
s0 denotes the initial state of the SysML model, i.e. the
• Transitions Systems, these signals of interest play the role
global state obtained when all the block instances enter of observable events. Other signals become de facto invisible
their initial states. events. Transitions involving one signal exchange are labeled
Generating the LRG consists in considering all possible by the name of the signal. Other transitions are labeled by
transitions from all not-yet-handled states —this not-yet- τ. The objective of minimizing the Labeled Reachability
handled set contains s0 when starting the graph generation—. Graph is to get rid of the transitions labeled by τ and to
For each not yet handled transition t fire-able from a given keep the ones labeled by a signal name. Depending on the
state s1 ∈ not − yet − handled, we first create δ ∈ ∆ with equivalence relation, the quotient automaton resulting from the
δ = (s1 , σ , s2 ). We then have to compute whether ∃s ∈ S minimization process may still contain τ transitions.
with s ≡ s2. If this is the case, δ = (s1 , σ , s2 ). Otherwise, s2 TTool implements a 3-step algorithm:
is added to S and to the not-yet-handled set. This leads us 1) Replace each ignored actions with a τ action.
to define the notion of state and of state equivalence for a 2) Remove all τ transitions i.e. merging states s1 and s2
SysML model. when there is a τ transition between the two.
3) Minimize the graph.
Definition:
S
State. The state of a SysML model is defined The quotient automaton computation algorithm can be
as Sb , Sa where: sketched as follows. If the first two stages are quite straight-
• Sb is the state of block b. The state of a block b is defined forward from an algorithmic point of view, the minimization
by the value of its attributes al, by one state of its state itself relies on the identification of coarse blocks, i.e. blocks
machine (it can be considered as a pointer to the current that are bisimulation-equivalent states. In order to identify
state of the state machine of b), and by the value of its these blocks, we rely on the partitioning of the graphs —using
clock. Indeed, if we assume a global clock applied to all splitters— iterating on the different symbols in the graph, as
blocks, we need to use a local clock to remember how explained in [21].
much of after clauses has elapsed. IV. TEST SEQUENCE GENERATION
• Sa represents the state of the signal queue a. There is one
signal queue for each asynchronous communication. The The paper proposes a test sequence generation where the
state of a signal queue is characterized by its ordered test sequences are generated from the quotient automaton
list of n messages m1 (p11 , p12 , ...), m2 (p21 , p22 , ...), ...). output by the verification process. Since test sequences are
built directly from SysML actions and communication labels,
the labelling of test sequences directly refers to elements of
Definition: State equivalence. Two states s1 and s2 are
the SysML model.
said to be equivalent s1 ≡ s2 if and only if all their state
values are equal. A. Refusal Graphs and Test Sequence Generation
A refusal graph [20] is a deterministic Labeled Transition
In terms of tool implementation, the above approach is System that emphasizes on the actions that are accepted from
implemented by the model-checker integrated to TTool. The a state (and thus on the ones that are refused).
comparison between states is based on hashing techniques
taking into account all elements above listed: state machine Definition: Refusal Graph. A Refusal Graph is a 5-uple
pointer, attributes values, local clock, message queues. Finally, RG = (G, Σ, ∆, g0 , Re f ) where Re f : G → P(P(Σ)) is a
contrary to many contributions, we are able to generate LRG mapping which defines for each state, the sets of actions that
directly from SysML model, without the need to use a pivot may be refused after the sequence leading to this state. To
language. This facilitates the back-tracing to models, and avoid redundancy, refusal sets must be minimal w.r.t. their
avoids formally proving model transformations. This probably inclusion set. Also, to avoid describing imaginary systems,
has a performance cost when generating the reachability only refused parts of the output set are considered.
graphs or more generally studying safety properties.
The algorithm used to generate a Refusal Graph from a
C. LRG Minimization Quotient Automaton can be sketched as follows. It follows
The labeled reachability graph of the SysML model may all possible paths in the input Quotient Automaton, but stops
have hundred, thousands and even more states and transitions. each time an already met state is encountered (cycle). A
Definitely, interpreting such a graph is impossible for Human. transition with a given label l is created in the RG each time
Also, the purpose of verification is not to check the entire the outgoing transitions of the QA contains this label at least
behavior of the system in one operation. The question of once from the current state of QA.
which subset of the system can be defined and checked is then
asked. The answer proposed by verification by abstraction is Using refusal graphs enables using an operational procedure
as follows: verification will zoom on a subset of the signals for implementing the concept of canonical tester [23]. The
exchanged by pairs of blocks involved in the evolution of latter and the original model have the same traces. Further,
the system. To refer to the theories developed for Labeled its synchronization with the Implementation Under Test must
AvioSE 2019: 1st Workshop on Avionics Systems and Software Engineering @ SE19, Stuttgart, Germany 69
not lead to a deadlock situation.
Finally, generating Test Sequences TS from a Refusal Graph
basically consists in identifying all possible paths of maximal
size i.e. it consists in finding, from termination states, the
longest path from the origin state. To do this, we rely on the
Dijkstra algorithm that can compute the path length from one
state to another in a LTS. Therefore, test sequences correspond Fig. 1. Global Testing Architecture (left) and Local Testing Architecture
to all longest paths from the initial state to a termination state. (right)
ClientServerSystem
Definition: Test Case. A Test Case is a Labeled Transition
System TC = (S, Σ, ∆, s0 , v) where v : S → {pass, f ail}. <>
ProcessRequest
<>
Client Server
The algorithm deriving a refusal graph from one quotient
automaton is described below.
1: QA: Quotient Automaton. RG: Refusal Graph.
2: We go though the graph, starting at state #1. Each time <>
Network
we meet an already handled state, we stop handling this
path.
Fig. 2. Use-Case Diagram for the Client/Server Protocol
3: metStates = {}
4: toHandleStates = { QA.getState(0)} {We have a list of
associations Assoc{} between states in QA and RF}
added service. Similarly, the interoperatibility testing architec-
5: State currentState = new State(0);
ture defines a 3-layer architecture where the tester is located on
6: RG.add(currentState)
top of one or several protocol entities (IUT1 and IUT2). The
7: Assoc.add(QA.getState(0), currentState) {Main loop}
Implementation Under Test UTA1 and UT2 are themselves
8: while toHandleStates is non empty do
being on top of one pre-existing communication service.
9: currentQA = toHandleStates.get(0)
Assuming the networked system is made up of two protocol
10: currentRefusal = Assoc.get(currentQA);
entities, Figure 1 (left part) defines a global testing architecture
11: toHandleStates.remove(0)
where the global tester is connected to both protocol entities.
12: metStates.add(currentQA) {For each out transition of
Figure 1 (right part) depicts a local testing architecture where
currentQA, we create a transition in currentRefusal if
the tester is connected to one protocol entity (IUT1).
the transition does not yet exist with the same label}
13: Loop on tr = currentQA out transitions B. Client/Server Protocol
14: if not (tr.label exists in out transitions of currentRefusal)
then This section abstractly defines a client/server protocol where
15: QA.add(newState) the server may acknowledge or refuse the requests issued by
16: Assoc(destination state of tr, newState) the client.
17: currentRefusal.addOutTransition(to newState, label The use-case diagram in Figure 2 delimits the boundary of
of tr) the communication system and links it to the client and server
18: if not (metStates contains destination state of tr) then applications, as well as to underlying, preexisting network.
19: toHandleStates.add(destination state of tr) Figure 3 depicts a successful completion of an inquiry
20: end if procedure. The service primitive suffixes abbreviate request,
21: end if indication, response, and confirm. Two Protocol Data Units are
22: Endloop used: xREQ and xOK. For space reasons, the paper does not
23: end while show the sequence diagrams developed for the inconclusive
termination of the request. In brief, the sequence diagrams of
The following case studies demonstrate the usability of
Figures 3 and 4 are merely modified to replace ”ok” by ”nok”
our verification approach on a relevant system. The interest
and ”OK” by ”NOK”.
of generating graphs and test sequences from SysML model
Figure 5 depicts the communication architecture that use
is shown by the clear relation between graph labels and the
the client/server protocol.
SysML model.
In terms of protocol machines, Figure 6 depicts the protocol
V. A C ASE S TUDY OF I NTEROPERABILITY T ESTING machine associated with the Requester. Figure 7 depicts the
protocol machine associated with the Responder.
A. Testing architecture Figure 8 depicts the reachability graph generated from the
Layered design of communication protocol commonly uses SysML model by TTool. Making the reachability graph a
a 3-layer pattern where two protocol entities rely on one pre- Labeled Transition Systems, which enables reuse of verifi-
exisiting communication service to render in turn a value- cation techniques originally developed for LTS, in particular
AvioSE 2019: 1st Workshop on Avionics Systems and Software Engineering @ SE19, Stuttgart, Germany 70
IDLE
x_req()
XREQ()
Fig. 3. Service Scenario (successful request)
WAITING
XOK() XNOK()
x_cnf_ok() x_cnf_nok()
Fig. 4. Protocol Scenario (successful request)
Fig. 6. Protocol Machine for the Requester
block block
Client Server
IDLE
~ out x_req() ~ in x_ind()
~ in x_cnf_ok() ~ out x_rsp_ok()
~ in x_cnf_nok() ~ out x_rsp_nok()
XREQ()
block block
Requester x_ind()
Responder
WAITING
~ in x_req() ~ out x_ind()
~ out x_cnf_ok() ~ in x_rsp_ok()
~ out x_cnf_nok() ~ in x_rsp_nok()
~ out XREQ() ~ in XREQ()
~ in XOK() ~ out XOK()
x_rsp_ok() x_rsp_nok()
~ in XNOK() ~ out XNOK()
XOK() XNOK()
Fig. 5. Communication architecture
Fig. 7. Protocol Machine for the Responder
minimization with respect to an equivalence relation. The
transitions of the reachability graph are labeled by those events
the designer wants to focus verification on. These events are
typically exchanges of signals between pairs of blocks.
As far as communication architecture validation is concerned,
the events to be preserved by the minimization process are
the service primitives exchanged at the boundary between the
protocol entities (Requester and Responder on Figure 5) and
their respective users (Client and Server on Figure 5). We
selected service primitives as observable events to decorate
the reachability graph in Figure 8. The minimization process
with respect to observational equivalence outputs the quotient
automaton depicted by Figure 9.
From the quotient automaton in Figure 9, we obtained the test
sequences depicted by Figure 10. If the system stops in an Fig. 8. Reachability Graph
intermediate state (e.g., a state different from 4 and 8), then
AvioSE 2019: 1st Workshop on Avionics Systems and Software Engineering @ SE19, Stuttgart, Germany 71
Fig. 11. Conformance Testing Architecture
block
CompactFlashDriver block
- savingTimeMin = 9 : int; CameraDriver
- savingTimeMax = 11 : int;
- full = false : bool;
block ~ out pictureWasTake...
Fig. 9. Quotient Automaton Preserving the Service Primitives block ~ in takePicture()
TransmissionDevices
PictureProcessingManager
- p : Point;
- p1 : Point; - p : Point;
- p2 : Point; - pTemp : Point;
~ in takePictureOrder(Point p) block
~ out flight()
~ out takePictureOrder(... ~ in flight() Autopilot
~ in currentPosition(Point p)
~ out gotoPosition(Point p) - currentPosition : Poi...
~ in pictureWasTaken() - targetPosition : Point;
block
~ out savePicture() - currentSpeed : Spe...
GNSSDeviceDriver ~ out takePicture() - diffX : int;
~ in pictureWasSaved() - diffY : int;
- p : Point;
~ in transmitPicture() - neg : int;
~ out picture()
~ in setNewPosition(Poin...
~ in gotoPosition(Poi...
~ out positionToPPM(Poi...
~ out setSpeed(Spe...
~ in getCurrentPositi...
block
LocationManager
- speed : Speed;
- p : Point; This block contains
- turbulenceX : int; the initial position
- turbulenceY : int;
- turbulence = false : bool;
- alwaysTurbulence = false : bool;
Fig. 12. Architecture of the UAV
Fig. 10. Test Sequences derived from the Quotient Automaton
modeled.
Pictures can be taken only when the drone is flying. A
the test fails. Otherwise, it succeeds. remote system located in a ground station can send picture
order to the drone. A picture order contains the GPS position
VI. A C ASE S TUDY OF C ONFORMANCE T ESTING : A UAV of the picture to be taken. To know its current position, a
A. Testing Architecture drone has an integrated GPS. When a picture GPS point
Conformance testing is the process of verifying the cor- is reached, with regards to a given threshold, the picture is
rectness of an artifact in the development cycle of a system taken, and then stored on a CompactFlash removable storage
against its model. For a black box testing approach one system. The system needs 2 seconds to take a picture, and
may use a testing architecture where the tester accesses the between 4 and 5 seconds to store it in on the memory card.
Implementation Under Test (IUT) via one or several Points Pictures may be remotely downloaded from the ground station
of Control and Observations (PCOs). Assuming the design is using a download order. Pictures can also be read from the
a layered one, Figure 11 depicts such type of conformance CompactFlash once the drone has come back from its mission.
testing architecture with two PCOs that respectively test the
C. UAV Modeling and Test Sequence Generation
interfaces of the IUT with its upper and lower layers.
Figure 12 depicts the architecture of the UAV in the form
B. Informal Specification of the UAV of a block instance diagram.
The UAV can autonomously take off, fly in a stabilized The reachability graph of the UAV depicted by Figure 12
way, and land at its destination or whenever a critical situation has 674 states and 927 transitions. The reachability graph
is encountered. It takes pictures at given locations. Only is labeled to preserve a limited set of signal exchanges:
the software related to taking pictures is modeled in this requesting for the flight to start, taking pictures, and
case study: the taking off, flying and landing actions are not saving them. The minimization process outputs the quotient
AvioSE 2019: 1st Workshop on Avionics Systems and Software Engineering @ SE19, Stuttgart, Germany 72
Fig. 13. Quotient Automaton from the UAV model
automaton depicted by Figure 13. Complying with the
approach proposed by the paper, the quotient automaton
serves as starting point for generating test sequences.
Figure 14 depicts the test sequences generated by TTool:
one of them concerns the regular execution of the UAV , the
other one evaluates that that the UAV works as expected when
the memory for storing pictures is full. These test sequences
remain abstract test sequences that need to be transformed into
concrete test sequences that may be processed by an actual
tester. This transformation is not yet implemented by TTool.
Fig. 14. Test Sequences for the UAV Model
VII. RELATED WORK
A. Model-Based Testing for Basic Models
How to derive test sequences from fundamental models
such as Extended Finite State Machine or Labeled Transition
System has extensively been discussed in the literature, years
before the MBSE acronym was coined. In particular, the use state machine diagrams to model transactions. An Event-
increasing development of networked systems has stimulated Model is derived from the SysML one to generate vulnerability
research work on protocol testing In [17]. Most of the models and robustness test cases.
listed in [17] are discrete event Model of Computation. The ad- In [19], Gonzales et al. propose a SysML-based modeling
vent of Cyber Physical Systems has stimulated research work methodology for model testing of CPSs, and a SyML-Simulink
on hybrid models assembling discrete events and continuous co-simulation framework.
paradigms. In [24], Hilken and Peleska combine model-based test gener-
ation and requirement tracing. It becomes possible to identify
B. Model-Based Testing from SysML models test cases suitable for verifying a given requirement in an
In [10], Gauthier et al use discrete SysML/OCL modeling automated way.
artifact and add a Modelica support to address continuity. In [25], Yin et al. propose to derive test cases from activity
The SysML model is annotated with Modelica and OCL. The diagram, not from state machine diagrams (unlike other au-
approach relies on simulation techniques. thors). A SysML model edited with Enterprise Architect is
In [12], Lasalle et al. present MBT, a test sequence generation transformed into an intermediate representation form that is
tool developed for SysML in the framework of VETESSS, a in turn used to generate test cases automatically.
project connected with automotive industry. MBT generates In [25], Abbors et al. present MATERA, a plug-in of No-
functional tests from UML or SysML diagrams edited with Magic’s MagicDraw. MATERA enables requirement modeling
the open-source and Eclipse-based tool Topcased. The SysML in SysML and traces them to the UML model of the System
model of the System Under Test is the input of a tool that Under Test. MATERA transforms models into input for the
generates abstract test suites and transfers them to another tool Conformiq Qtronic tool, used for automated test generation.
in charge of creating concrete tests in the form of test scripts. The test scripts generated by Qtronic are executed in the
In [22], Ouerdi et al. share an experience in vulnerability test NetHawks’s East execution environment. The results of statis-
generation from SysML models of smart cards. The authors tics analysis of the test run are displayed.
AvioSE 2019: 1st Workshop on Avionics Systems and Software Engineering @ SE19, Stuttgart, Germany 73
VIII. CONCLUSIONS [11] J.M. Faria, S. Mahomad, N. Silva, Practical Results from the Application
of Model Checking and Test Generation from UML/SysML Models of
Test generation has been acknowledged as one of the On-Board Space Applications, DASIA 2009 Data Systems in Aerospace,
most cost-prone activity in the design trajectory of complex by L. Ouwehan, May 2009.
systems. The expected benefits of using a model-based [12] Lasalle, J., Peureux, F., Fondement F., Development of an Automated
MBT Toolchain from UML/SysML models, Innovations in Systems and
approach includes the possibility to reduce that cost by Software Engineering, December 2011, Vol. 7, No. 4, pp 247256.
automating a test generation from a model of the system. [13] Saqui-Sannes P. de, Courtiat J-P., Casadessus R., 1995, Verification
by abstraction as a preamble for interoperability test suite generation.
Protocol Specification, Testing and Verification XIV, Vancouver, BC,
The paper proposes a novel approach for generating test Canada.
sequences expressed in SysML and more precisely in the [14] Brinksma E., Tretmans J. (2001) Testing Transition Systems: An Anno-
dialect of SysML supported by the free and open-source tool tated Bibliography. In: Cassez F., Jard C., Rozoy B., Ryan M.D. (eds)
named TTool. The block instance diagram describing the Modeling and Verification of Parallel Processes. MOVEP 2000. Lecture
Notes in Computer Science, vol 2067. Springer, Berlin, Heidelberg.
architecture of the system and the state machine diagrams [15] Hennessy M., Milner R. (1980) On observing nondeterminism and con-
describing the behaviors of the block instances serve as input currency. In: de Bakker J., van Leeuwen J. (eds) Automata, Languages
to a process that links test generation to formal verification. and Programming. ICALP 1980. Lecture Notes in Computer Science,
vol 85. Springer, Berlin, Heidelberg.
Indeed, assuming the reachability graph of the SysML model
[16] R., Konur S., Yildirim U., Uddin A., Campean F., Gheorghe M., Towards
can be computed, TTool generates the latter as a Labeled an Integrated Approach to Verification and Model-Based Testing in
Transition System whose transitions are labeled by events System Engineering, 2017 IEEE International Conference on Internet
appropriately selected by the user of TTool. The labeled of Things (iThings) and IEEE Green Computing and Communications
(GreenCom) and IEEE Cyber, Physical and Social Computing (CP-
reachability graph is minimized using Milner’s observational SCom) and IEEE Smart Data (SmartData).
equivalence. The resulting quotient automaton serves as [17] Dssouli, R, Khoumsi, A., Elqortobi M., Bentabar. J., Chapter Three
starting point to build up a refusal graph, which serves in - Testing the Control-Flow, Data-Flow, and Time Aspects of Com-
munication Systems: A Survey. Advances in Computers 106: 95-155
turn as starting point for generating test sequences. (2017). Peleska, J., Huang W., Industrial-Strength Model-Based Testing
of Safety-Critical Systems, 2016, International Symposium on Formal
Taking a UAV as case study, the paper illustrates the test Methods, Limassol, Cyprus.
generation approach in the case of conformance testing. Other [18] TTCN standard, ESTI n. ES 201 873-1, http://www.ttcn-3.org/
[19] Carlos A. Gonzlez, Mojtaba Varmazyar, Shiva Nejati, Lionel C. Briand
types of testing, such as interoperability testing [13] also and Yago Isasi, Enabling Model Testing of Cyber-Physical Systems.
deserve investigations. Whatever the type of testing, the test In Proceedings of ACM/IEEE 21th International Conference on Model
sequences must be presented in a standardized form, e.g. using Driven Engineering Languages and Systems (MODELS 2018). ACM,
New York, NY,USA, 11 pages.
the TTCN notation [18].
[20] Drira, K., The refusal Graph: a Tradeoff between Verification and Test,
R EFERENCES 6th International Workshop on Protocol Test Systems (IWPTS’93), 0.
Rafiq (ed.), Pau (France), September 1993, pp.301-316.
[1] Madni, A., Sievers, M., Model-based systems engineering: Motivation, [21] Eliyah Kilada, Project Report Class: ECE/CS 5745/6745, “A C++
current status, and research opportunities, Systems Engineering, May Implementation of an Efficient Algorithm for Labeled Transition Sys-
2018. tem Minimization Based on Bisimulation Equivalence”, Project Re-
[2] Object Management Group, https://www.omg.org/. port Class: ECE/CS 5745/6745, Fall 2008. http://www.ece.utah.edu/ ki-
[3] International Council for Systems Engineering, https://www.incose.org/. lada/ClassProjects/BisimulationMinimization.pdf
[4] Systems Modeling Language, version 1.5, [22] Ouerdi, N., Azizi, M., J.L. Lanet, Azizi, J.L., Ziane, M., EMV Card:
https://www.omg.org/spec/SysML/, May 2017. Generation of Test Cases based on SysML Models, International Con-
[5] T. Le Sergent, F.-X. Dormoy, A. Le Guennec. Benefits of Model Based ference on Electronic Engineering and Computer Science, 2013, IERI
System Engineering for Avionics Systems. 8th European Congress on Procedia 4 ( 2013 ) 133 138.
Embedded Real Time Software and Systems (ERTS 2016), Toulouse,
[23] Richards, D., Stuart, A., Hause, M., Testing Solutions through SysML
France, January 2016,.
/ UML, Incose, Singapore, July 2019, Vol. 19, No. 1, pp. 760-774.
[6] F. Mehnni, J.-Y. Choley, N. Nguyen, C. Frazza, Flight Control System
Modeling with SysML to Support Validation, Qualification and Certifi- [24] Hilken C., Peleska J. Model-Based Testing Against Complex SysML
cation, IFAC-PapersOnLine 49-3 (2016), pp. 453–458. Models. In: Drechsler R., Khne U. (eds) Formal Modeling and Verifi-
[7] Cameo Systems Modeler, https://www.nomagic.com/products/cameo- cation of Cyber-Physical Systems. Springer Vieweg, Wiesbaden, June
systems-modeler. 2015.
[8] Rhapsody, https://www.ibm.com/fr-fr/marketplace/architect-for-systems- [25] Yin, Y., Xu, Y., Chen, Y., An Automated Test Case Generation Ap-
engineers. proach based on Activity Diagrams of SysML, International Journal on
[9] Saqui-Sannes, P. de, Vingerhoeds, R., Apvrille, L, EarlyChecking of Performability Engineering, Vol. 13, No. 6, October 2017, pp. 922-936.
SysML Models applied to protocols, 12th International Conference [26] Abbors, F., Bcklund, A., Truscan, D., MATERA - An Integrated
on Modeling, Optimisation and Simulation (Mosim 2018), June 2018, Framework for Model-Based-Testing, Proceedings of the 17th IEEE
Toulouse, France. International Conference and Workshops on Engineering of Computer
[10] Gauthier, J.-M., Bouquet, F., Hammad, A., and Peureux, F. 2015, A Based Systems 2010, pp. 321-328.
SysML Formal Framework to Combine Discrete and Continuous Simu- [27] Peleska, J., Model-based Avionic Systems Testing for the Airbus Family,
lation for Testing, 17th International Conference on Formal Engineering 23r IEEE European Test Symposium, Amsterdam, The Netherlands,
Methods. (ICFEM15), LNCS 9407, p. 134-152. 2018.
AvioSE 2019: 1st Workshop on Avionics Systems and Software Engineering @ SE19, Stuttgart, Germany 74