-Test generation has been acknowledged as a costprone activity reducing productivity and time to market. The expected benefits of Model Based Systems Engineering include automated generation of test sequences from models. The paper proposes verification solutions for the System Modeling Language (SysML). In particular, the paper shows how to link test generation to formal verification. The proposed algorithms are implemented by the free software TTool. Two case studies support discussion on conformance and interoperability testing, respectively.
The widespread of Model Based System Engineering
approaches [
In brief, the reachability graph of the SysML model is
computed directly from the block instance diagram that defines the
architecture of the system and from the state machine diagrams
that define the behaviors of the block instances. The transitions
of the graph are labelled using the messages exchanged by
pairs of block instances. This transforms the reachability
graph of the SysML model into a Labeled Transition System.
Theories developed for LTS [
2TTool: https://ttool.telecom-paristech.fr/
obtain a set a test sequences. Associated algorithms have been
implemented in the free and open-source tool named TTool
[
The paper is organized as follows. Section II introduces SysML and more precisely the block instance and state machine diagrams. Section III presents a verification by abstraction approach for SysML models. Section IV uses the output of the verification process to generate test sequences. Section V applies the proposed approach to a client/server protocol and discusses interoperability testing. Section VI uses a UAV in charge of taking pictures to address conformance testing. Section VII surveys related work. Section VIII concludes the paper and outlines future work.
The SysML standard [
During the design phase, one defines the architecture of the system and the behaviors of the blocks the architecture is made up of. The SysML standard defines two architectural design diagrams: the Block Definition Diagram (BDD) and the Internal Block Diagrams (IBD) of the SysML standard. In the paper, we use the version of SysML supported by TTool where the BDD and IBD are merged into one diagram: the Block Instance Diagram (BID). Each block instance has a behavior expressed in the form of a SysML state machine diagram.
A Block Instance Diagram is a tripartite graph with one type of nodes, each one defining a block instance, and two types of relations. First, the ”composition” relation of SysML (black diamond) enables to say that one block instance is made up of one or several block instances. Second, the ”connect” relation connects two ports used for exchanging signals. For simplicity, the below definitions address the ”connect” relation, not the ”composition” one.
Definition: block instance. A block instance is a 4-uple (id; al; ml; pl; isl; osl) where: id is a String that names the block instance. al is an attribute list. The attribute types include Integer, Boolean, Timer, and user-defined Records. An attribute may be defined with an initial value. ml is a method list. pl is a port list. isl is an input signal list.
osl is an output signal list.
Definition: Block Instance Diagram. A Block Instance Diagram is a 3-uple (Blk; connect; assoc) where:
Blk is a set of block instances. connect is a function Port ! Port that connects pairs of ports. assoc is a function (BlkxSignal) ! (BlockxSignal) that associates one signal of block B1 to one signal of block B2, making it possible to compose the state machines belonging to B1 and B2. Here, the term compose denotes a composition in the usual sense of finite state machine composition, not the composition relation supported depicted by a black diamond in SysML.
Finally, a Block Instance Diagram depicts the architecture of a system as a graph of interconnected blocks.
Each block instance contains one extended state finite state machine that supports states, transitions, attribute settings, inputs and outputs operations on signals, and time manipulation. Definition: State Machine. An extended finite state machine depicted by a SysML state machine diagram is bi-partite graph (s0; S; T ) where
S is a set of states (s0 is the initial state).
T is a set of transitions.
Definition: State Transition. A transition in a state machine is a 5-uple (sstart ; a f ter; condition; Actions; send ) where: sstart is the initial state of the transition. a f ter(tmin; tmax) enables firing the transition after at least between tmin and tmax units of time have elapsed. condition is a Boolean expression that conditions the execution of the transition. A condition may use attributes of its corresponding block.
Actions is a ordered set of action. These actions can be executed only once the transition has been enabled i.e. the a f ter clause has elapsed and the condition equals true. send is the final state of the transition.
A state machine cannot contain parallel states, historic state, fork and join states. These behaviors can easily be replaced by counterparts. e.g. using sub-blocks and synchronous signals for each parallel activity.
Adding a state machine to each block instance makes the model an executable one. Interactive simulation enables early checking of the state machines against design errors. It does not necessarily explore the entire state space of the model. Thus, it heavily depends on the experience of the user of the simulator, or on the random generator of that simulator. Conversely, formal verification relies on mathematics rather than chance.
The verification approach discussed in this section requires exploring the state space of the SysML and more precisely generating (a sub part of) the graph of states that may be reached from the initial state of the system. Full generation of the reachability graph of the SysML model explores all the execution paths the system may go through starting from its initial state. The graph enables checking the system against reachability properties (using the model-checker we have integrated into TTool). Also, when a property to investigate is the reachability of a given state, then the graph generation stops as soon as the property is satisfied (on-the-fly modelchecking).
As usually, reachability analysis faces the state space explosion problem. Starting from now, the following hypothesis applies: the reachability graph of the SysML model may be entirely built within an acceptable amount of time and memory.
In this section, we assume the SysML model is composed of one block instance diagram and one state machine diagram per block instance. Other diagrams of the SysML model are ignored since they do not play any role in the reachability graph construction process.
Definition: Labeled Reachability Graph. The Labeled Reachability Graph (LRG) of a SysML model is a 5-uple LRG = (S; S; Q; D; s0) where:
S denotes the countable number of global states of the SysML model S is a countable set of observable events included in the list of signals exchanged on ports. Thus we have S ”!”Ao(p) [ ”?”Ai(p) [ ”!”So(p) ”?”Si(p)) where: – ”!” and ”?” respectively denote an emission and a reception. – Ao(p) is an output signal connected to an asynchronous channel. – Ai(p) is an input signal connected to an asynchronous channel. – So and S1 are output and input signals connected via a synchronous channel. – p denotes a list of attributes of the block to which the signal sending/receiving corresponds.
Q is a countable set of internal events, e.g. the assignation of an attribute. Thus we have Q i(a =< expr >) _ i() where a is an attribute.
D Sx(S [ Q)xS denotes the set of labeled transitions in the reachability graph. A label contains the name of the signal exchanged by one pair of block instances or the identification of the internal action, i.e. i(:::). An empty i() transition is sometimes denoted t. s0 denotes the initial state of the SysML model, i.e. the global state obtained when all the block instances enter their initial states.
Generating the LRG consists in considering all possible transitions from all not-yet-handled states —this not-yethandled set contains s0 when starting the graph generation—. For each not yet handled transition t fire-able from a given state s1 2 not yet handled, we first create d 2 D with d = (s1; s ; s2). We then have to compute whether 9s 2 S with s s2. If this is the case, d = (s1; s ; s2). Otherwise, s2 is added to S and to the not-yet-handled set. This leads us to define the notion of state and of state equivalence for a SysML model.
Definition: State. The state of a SysML model is defined as S Sb; Sa where:
Sb is the state of block b. The state of a block b is defined by the value of its attributes al, by one state of its state machine (it can be considered as a pointer to the current state of the state machine of b), and by the value of its clock. Indeed, if we assume a global clock applied to all blocks, we need to use a local clock to remember how much of after clauses has elapsed.
Sa represents the state of the signal queue a. There is one signal queue for each asynchronous communication. The state of a signal queue is characterized by its ordered list of n messages m1(p11 ; p12 ; :::); m2(p21 ; p22 ; :::); :::).
Definition: State equivalence. Two states s1 and s2 are said to be equivalent s1 s2 if and only if all their state values are equal.
In terms of tool implementation, the above approach is implemented by the model-checker integrated to TTool. The comparison between states is based on hashing techniques taking into account all elements above listed: state machine pointer, attributes values, local clock, message queues. Finally, contrary to many contributions, we are able to generate LRG directly from SysML model, without the need to use a pivot language. This facilitates the back-tracing to models, and avoids formally proving model transformations. This probably has a performance cost when generating the reachability graphs or more generally studying safety properties.
The labeled reachability graph of the SysML model may have hundred, thousands and even more states and transitions. Definitely, interpreting such a graph is impossible for Human. Also, the purpose of verification is not to check the entire behavior of the system in one operation. The question of which subset of the system can be defined and checked is then asked. The answer proposed by verification by abstraction is as follows: verification will zoom on a subset of the signals exchanged by pairs of blocks involved in the evolution of the system. To refer to the theories developed for Labeled Transitions Systems, these signals of interest play the role of observable events. Other signals become de facto invisible events. Transitions involving one signal exchange are labeled by the name of the signal. Other transitions are labeled by t. The objective of minimizing the Labeled Reachability Graph is to get rid of the transitions labeled by t and to keep the ones labeled by a signal name. Depending on the equivalence relation, the quotient automaton resulting from the minimization process may still contain t transitions.
TTool implements a 3-step algorithm: 1) Replace each ignored actions with a t action. 2) Remove all t transitions i.e. merging states s1 and s2 when there is a t transition between the two. 3) Minimize the graph.
The quotient automaton computation algorithm can be
sketched as follows. If the first two stages are quite
straightforward from an algorithmic point of view, the minimization
itself relies on the identification of coarse blocks, i.e. blocks
that are bisimulation-equivalent states. In order to identify
these blocks, we rely on the partitioning of the graphs —using
splitters— iterating on the different symbols in the graph, as
explained in [
The paper proposes a test sequence generation where the test sequences are generated from the quotient automaton 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 the SysML model.
A refusal graph [
Definition: Refusal Graph. A Refusal Graph is a 5-uple RG = (G; S; D; g0; Re f ) where Re f : G ! P(P(S)) is a mapping which defines for each state, the sets of actions that may be refused after the sequence leading to this state. To avoid redundancy, refusal sets must be minimal w.r.t. their inclusion set. Also, to avoid describing imaginary systems, only refused parts of the output set are considered.
The algorithm used to generate a Refusal Graph from a Quotient Automaton can be sketched as follows. It follows all possible paths in the input Quotient Automaton, but stops each time an already met state is encountered (cycle). A transition with a given label l is created in the RG each time the outgoing transitions of the QA contains this label at least once from the current state of QA.
Using refusal graphs enables using an operational procedure
for implementing the concept of canonical tester [
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 to all longest paths from the initial state to a termination state.
Definition: Test Case. A Test Case is a Labeled Transition System TC = (S; S; D; s0; v) where v : S ! fpass; f ailg. 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 we meet an already handled state, we stop handling this path. 3: metStates = fg 4: toHandleStates = f QA.getState(0)g fWe have a list of associations Assocfg between states in QA and RFg 5: State currentState = new State(0); 6: RG.add(currentState) 7: Assoc.add(QA.getState(0), currentState) fMain loopg 8: while toHandleStates is non empty do 9: currentQA = toHandleStates.get(0) 10: currentRefusal = Assoc.get(currentQA); 11: toHandleStates.remove(0) 12: metStates.add(currentQA) fFor each out transition of currentQA, we create a transition in currentRefusal if the transition does not yet exist with the same labelg 13: Loop on tr = currentQA out transitions 14: if not (tr.label exists in out transitions of currentRefusal) then 15: QA.add(newState) 16: Assoc(destination state of tr, newState) 17: currentRefusal.addOutTransition(to newState, label of tr) 18: if not (metStates contains destination state of tr) then 19: toHandleStates.add(destination state of tr) 20: end if 21: end if 22: Endloop 23: end while
The following case studies demonstrate the usability of our verification approach on a relevant system. The interest of generating graphs and test sequences from SysML model is shown by the clear relation between graph labels and the SysML model.
V. A CASE STUDY OF INTEROPERABILITY TESTING
Layered design of communication protocol commonly uses a 3-layer pattern where two protocol entities rely on one preexisiting communication service to render in turn a valueadded service. Similarly, the interoperatibility testing architecture defines a 3-layer architecture where the tester is located on top of one or several protocol entities (IUT1 and IUT2). The Implementation Under Test UTA1 and UT2 are themselves being on top of one pre-existing communication service. Assuming the networked system is made up of two protocol entities, Figure 1 (left part) defines a global testing architecture where the global tester is connected to both protocol entities. Figure 1 (right part) depicts a local testing architecture where the tester is connected to one protocol entity (IUT1).
This section abstractly defines a client/server protocol where the server may acknowledge or refuse the requests issued by the client.
The use-case diagram in Figure 2 delimits the boundary of the communication system and links it to the client and server applications, as well as to underlying, preexisting network.
Figure 3 depicts a successful completion of an inquiry procedure. The service primitive suffixes abbreviate request, indication, response, and confirm. Two Protocol Data Units are used: xREQ and xOK. For space reasons, the paper does not show the sequence diagrams developed for the inconclusive termination of the request. In brief, the sequence diagrams of Figures 3 and 4 are merely modified to replace ”ok” by ”nok” and ”OK” by ”NOK”.
Figure 5 depicts the communication architecture that use the client/server protocol.
In terms of protocol machines, Figure 6 depicts the protocol machine associated with the Requester. Figure 7 depicts the protocol machine associated with the Responder.
Figure 8 depicts the reachability graph generated from the SysML model by TTool. Making the reachability graph a Labeled Transition Systems, which enables reuse of verification techniques originally developed for LTS, in particular 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 intermediate state (e.g., a state different from 4 and 8), then x_req()
XREQ() WAITING XOK()
XNOK() x_cnf_ok() x_cnf_nok()
IDLE XREQ() x_ind()
WAITING x_rsp_ok()
x_rsp_nok() XOK()
XNOK()
Fig. 8. Reachability Graph Fig. 9. Quotient Automaton Preserving the Service Primitives block TransmissionDevices - p : Point; - p1 : Point; - p2 : Point; ~ out flight() ~ out takePictureOrder(...
block GNSSDeviceDriver - p : Point; ~ in setNewPosition(Poin... ~ out positionToPPM(Poi... the test fails. Otherwise, it succeeds.
VI. A CASE STUDY OF CONFORMANCE TESTING: A UAV
Conformance testing is the process of verifying the correctness of an artifact in the development cycle of a system against its model. For a black box testing approach one may use a testing architecture where the tester accesses the Implementation Under Test (IUT) via one or several Points of Control and Observations (PCOs). Assuming the design is a layered one, Figure 11 depicts such type of conformance testing architecture with two PCOs that respectively test the interfaces of the IUT with its upper and lower layers.
The UAV can autonomously take off, fly in a stabilized way, and land at its destination or whenever a critical situation is encountered. It takes pictures at given locations. Only the software related to taking pictures is modeled in this case study: the taking off, flying and landing actions are not modeled.
Pictures can be taken only when the drone is flying. A remote system located in a ground station can send picture order to the drone. A picture order contains the GPS position of the picture to be taken. To know its current position, a drone has an integrated GPS. When a picture GPS point is reached, with regards to a given threshold, the picture is taken, and then stored on a CompactFlash removable storage system. The system needs 2 seconds to take a picture, and between 4 and 5 seconds to store it in on the memory card. Pictures may be remotely downloaded from the ground station using a download order. Pictures can also be read from the CompactFlash once the drone has come back from its mission.
Figure 12 depicts the architecture of the UAV in the form of a block instance diagram.
The reachability graph of the UAV depicted by Figure 12 has 674 states and 927 transitions. The reachability graph is labeled to preserve a limited set of signal exchanges: requesting for the flight to start, taking pictures, and saving them. The minimization process outputs the quotient automaton depicted by Figure 13. Complying with the approach proposed by the paper, the quotient automaton serves as starting point for generating test sequences.
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
increasing development of networked systems has stimulated
research work on protocol testing In [
In [
In [
In [
In [
In [
In [
VIII. CONCLUSIONS
Test generation has been acknowledged as one of the most cost-prone activity in the design trajectory of complex systems. The expected benefits of using a model-based approach includes the possibility to reduce that cost by automating a test generation from a model of the system.
The paper proposes a novel approach for generating test sequences expressed in SysML and more precisely in the dialect of SysML supported by the free and open-source tool named TTool. The block instance diagram describing the architecture of the system and the state machine diagrams describing the behaviors of the block instances serve as input to a process that links test generation to formal verification. Indeed, assuming the reachability graph of the SysML model can be computed, TTool generates the latter as a Labeled Transition System whose transitions are labeled by events appropriately selected by the user of TTool. The labeled reachability graph is minimized using Milner’s observational equivalence. The resulting quotient automaton serves as starting point to build up a refusal graph, which serves in turn as starting point for generating test sequences.
Taking a UAV as case study, the paper illustrates the test
generation approach in the case of conformance testing. Other
types of testing, such as interoperability testing [