FTR&D case study description

 

The FTR&D application is a telecommunication service build on top of embedded platform and service components. The complete application developed for Omega is a service called Depannage. The Depannage service is related to a specific user need (the subscriber): Medical and doctor, Fire brigade, car repairing, etc. It allows a user to call for a Depannage with a specific number. The service invocation firstly asks for authentication of the calling user, then will search the calling location. Once the calling location found, the service will search in a data base different potential called numbers corresponding to the depannage society and as close as possible from the calling user location. Once different numbers found, the service will try to connect the calling user to one of the potential called number (in a sequential or parallel way). In any case the calling user should be connected to a secretariat or to a vocal box.

The complete application is built from a set of components, a main component called Depannage that represents the final service logic, and a set of service components that focus on some embedded parts of the system. These service components should be reusable for different service logics and therefore they are specified independently of any embedding system. The environment is composed by different phones and users, with a non-deterministic nature.

The communication and all these components include time constraints.

Part of the architecture of the FTR&D application

 

Modelling and Verification with OMEGA

 

FTR&D used during the project a set of techniques in order to build the application by a step-by-step approach.

·         First, we describe a high level specification of the service and component behaviour, including the behaviour of the communication between these components. This description includes timed constraints. Then the consistency of this high level specification is validated with respect to end-to-end requirements. Such analysis is made with LSC, the Play Engine tool and simulation/animation.

·         In a second step, model checking techniques are used with the Play Engine tool in order to verify in a formal way some requirements. The Play Engine tool allows verifying model with timed constraints, but it implies restrictions on the model. Then, parts of the model should be identified, focusing on complex and/or critical behaviours.

·         Once these first steps done, a more complete model (with all the potential behaviours, including creation and destruction of objects) is done using the Rose CASE tool. This model is then translated towards the VERIMAG/IF tool and it is validated with respect to some requirements expressed with observers.

 

LSC and the Play Engine for high level specification and animation

 

The wish to specify components in a reusable way involves that the component specification should be done independently of any embedding architecture. Such specification should correspond in universal LSC to an abstract view of the component, an abstract view describing how the component will react to events coming from its provided ports and how (and when) this component will act on its required ports. For the system, the complete application, the specification should be enhanced by universal LSCs describing the communications between these components. Such LSCs could include time constraints and delays on the communication.

The end-to-end requirements are expressed by existential LSC and will be validated during the simulation/animation of the model.

We can also remark that the FTR&D application makes a very intensive use of the multiple symbolic instances functionality of the Play Engine tool.

We will focus our example description on some components (Search-on-list, API), the users and the communication between components.

 

Search On List component

This component has two ports:

·         SearchService in order to communicate with the application that will use it

·         SearchApi in order to communicate with platform components and indirectly with the users and the environment

This component should act on reception of the order EstablishSearch coming form the port SearchService. At reception of this event, it should try to make a connection to potential destination parties. It will search for the first potential destination, then, if no correct answer arrives, it will try the second potential destination. The connection establishment will be done by the event LegDest send to the port SearchApi.  The Search component will wait for an answer from the port SearchApi, and has to tackle four potential results:

·         the destination party is busy,

·         the destination party answers after a predefined time. It is THE good and conclusive behaviour, then the component should send the response EstablishSearchReturn to the port SearchService,

·         the destination party answers before a predefined time (too early), is means that the connection should not be established,

·         the destination party do nothing. Then, it means that a timer should be initiated and, if it expired before the reception of a result coming from the port SearchApi, something should be done (the connection to the other potential party or a result to the port SearchService with a false condition).

The first LSC specifies the reception of the EsatblishSearch event from the port SearchService, it puts the Timer to Set and send a request LegDest(2) to the port SearchApi.

Once LegDest (3) sent, the component is waiting for a return: LegCallReturn(Boolean).

·         If this event arrives, the LSC Search2 will be executed, then will, either send a return to the port SearchService, or try to make a connection with the Leg 2

·         Another connection will be tried if the return is False (then busy or another error) or if this return arrived too early (then we are connected to a vocal box)

·         The LSC SearchTimer corresponds to a Timer. It is initiated when the variable Tset is put ŕ true, then 7 time slots could be executed before the execution of the main chart. The main chart will, either try to make another connection, or will send back the return with false on the port SearchService.

·         The Timer should be cleared when an event comes back from the port SearchApi (a user answer). It is done in LSC by a forbidden element.

First LSC for Search Component

Second LSC for Search Component

 

LSC for Search Component with Timer

Component platform: API

We decided in OMEGA to simplify this part of the model.

·         There are predefined phones for fixed, mobile and secretary user,

·         We decided to define only one phone of each category,

·         The phones may return busy or answer when they are called

The LSC CalledLeg will send an event callArrived to the corresponding phone. The LSCs APIanswer and APIbusy will return the associated state of the destination phone. We introduce in the LSC APIanswer a potential delay in the communication, the variable CondTime could be modified before the execution. In the reality, this delay corresponds to potential delays in the network.

The ApiCall component

The Depannage service specification

The following figures represent only a part of the specification of the depannage service, from the call to the component Location to the call of the component Search-on-list.

Part of the Depannage service specification

The Environment: the users

We model a simple view of user behaviour, focusing for a fixed phone on three possible states (or user action): busy, answer with a delay, or no-answer. The specification of mobile phone introduces the notion of quick answer. In the reality, if a mobile phone is reachable but in a not connected state, the communication will be connected to the vocal box of the phone. This connection is done quickly. This behaviour should be taken into account, some service logics do not want to connect the calling party to some vocal boxes (as for depannage service when we want to be connected to a person which is free or to a secretary or to the vocal box of the depannage company).

 

The Mobile Phone

The communication view

Universal LSC should be done when we create a new application. Following the architecture diagram, these LSC will specify the communications between components.

These LSC for connector behaviours are more or less complex, depending on

·         time constraints and delays

·         the parallel execution of execution threads

The following figure represents the communication between the Location and the depannage components. In these LSCs we introduce time delay on the communication. The LSC DepToLoc1 specifies that the signal SearchLocation will take between 1 and 2 time units.

Connectors between components Location and Depannage

Property: No connection to a personal vocal box

We want to verify that there is no possible connection from the calling party to the vocal box of a personal mobile phone. The  following picture shows the result of the Play Out execution when User3 makes a quick answer and the connection is establish without a correct answer of User2. This execution is done with a time delay on Api Object execution.

Property: Quick answer should be followed by normal answer

 

Violation of the property

Play Engine model checking for Time verification

The model checking tool allows obtaining a formal verification of the requirements. In order to use the model checking tool, some restrictions should be made on the model: no symbolic instances, only one parameter for each signal. We have also to work on parts of the model in order to avoid the well-known state-explosion problem (explosion of the graph which is enforced with time constraints). It means that we have to focus our work on the more complex part of the behaviour.

When we make formal verification, we wish to verify that all possible execution of the model will satisfy the requirements. The smart Play-Out approach allows executing all the execution paths and, during this execution, will search for the satisfaction of a property (an existential LSC).

The requirements we want to verify are: d1 ≤ Time_Duration ≤ d2, were Time_Duration is the end-to-end time execution.  Using the smart Play-Out tool we have to express a property that will violate the requirements, thus, the formal verification is done when this property is not satisfied by the model.

For example, for a requirement such as Time_Duration should always be more than 1 time unit (or equal to 1), we express the property by the TestFalse2 LSC (Time_Duration < 1), and we verify that this LSC is not satisfied. As counterexample, we verify that the LSC TestFalse can be satisfied.

 Components and time constraints

Requirements

For requirements such as: for all behaviours Time_Duration ≤ d, we have to express the property Time_Duration > d and verify that this property is not satisfied. But, with smart Play-Out, the time evolves even after the end of the execution. Here, we need to introduce universal LSC that will record different scenarios depending of the delays (and corresponding to the end of the behaviour). Then, the verification will be done using an existential LSC for each potential requirement. For example, the LSC TestTrue3 is not satisfied with the value T<4 in the Universal LSC release, but is satisfied with the time condition T<=3.

Existential LSC for verification

Part of the model with component Search

This part of the model focuses on the behaviour of the component Search-on-list, the API component and the users. We want to verify that the behaviour of all these components is still conform with the specification, depending on the actions made by the users and on the delay communication on the signal exchanges.

To do so, we have to introduce several existential LSC for each requirement. The different user behaviours will be modified using the Jump Start functionality of the tool. Before play-out the model, we initiate a specific jump start with one of the user actions: answer, noanswer, quickanswer, busy.

First, we verify the existential LSC with respect to the model and to the initial configuration. For example, if the Jump Start is done with “UserAction = quickanswer”, only one LSC should be satisfied (quickanswer).

Second, we introduce other time constraints on the components and the communications and we verify if the resulting behaviour is still correct. The model checking concludes non satisfaction of the existential LSC quickanswer if the Tanswer0601 is introduced and the Jump Start is done with UserAction=quickanswer (and the answer existential scenario will be satisfied). It means we have to modify the value of the time constraints on the EstablishSeacrh22 LSC.

 

Component Search behaviour

The communication behaviour

The Properties specification

IF tool for formal specification and verification of complete systems

The objectives of our work with the IF tool was to make a formal verification of a more complete model. The model developed here includes more complex behaviours corresponding to the call termination. It involves the creation and destruction of objects and more complex message exchanges patterns. In this model, we introduce also another behaviour that was not completely described with the LSC tool: the fact that several calls can be initiated in parallel in order to search the called party. In this behaviour, only the first answering called party will be connected to the calling party, the other initiated calls should be killed. The LSC and the Play Engine tool do not allow to model such behaviours, or in a too complex way (the model is then not readable anymore).

The model of the application was done with the Rose tool.

 

Rose class diagrams

The Figure presents the architecture of the application done with the Rose UML tool. The Class USER is the calling party, the subscriber of the service who initiates the service invocation. The class caller manages the invocations, sends requests to the localisation component then to the depannage component. The class depannage initiates the search, calling either the component ParaSearch for parallel search, or the component SeqSearch for sequential search. The class Search has the objective to make a unitary call to a destination party. Three kinds of destination parties are implemented: fix phones, mobile phones (GSM), and secretariat (with different behaviours). The class APICall should establish the communication between the calling user and the final called party.

We hereafter described in more details the behaviour of some of the classes.

 

Caller

The dynamic behaviour of the class Caller is shown on the following figure. It is composed of three states. Once a call is received, the localisation is initiated by a method call lanceLocalization(). Once the localisation obtained, the method LanceDepannage allows initiating the search of the different potential called numbers. In the state WaitDepannage, the reception of the message receiveDepannage alows to know if a called party was found.

Caller state machine: dynamics of class Caller

Depannage

The class Depannage is mainly responsible of the choice between the two kinds of searches. Here, we implement this choice as non deterministic.

Dynamics of class Depannage

ParaSearch

The class ParaSearch initiates calls to the potentially called parties (the professionals) in parallel. In the state WaitResponse, parallel calls are initiated. The state Idle is reached if, either a response arrives from a called party, or a timer TooLate expired (no called party is found in a reasonable delay). If a response arrives, all the other initiated calls are killed.

Dynamics of class ParaSearch

Search

The class Search manages the calls to the different potentially called parties. In the Idle state, when a message SeqSearch arrives, two timers are set in order to limit the duration of the research (Timer TooLate), and in order to reject the call if it reached the voice mail of a mobile phone (Timer TooEarly). When the signal KillSearch arrives, all the calls are killed. Once the duration TooEarly has passed, in the state WaitResponse the component waits for one of the events: timeout of the timer TooLate (moment at which all the calls are killed), the signal killSearch (on which also all the calls are killed), or a response to one of the calls (then all the other calls are killed).

Dynamics of class Search

GSM

We describe here only the class GSM for mobile phones. The other phone classes are even simpler. It includes the specification of the behaviour for a call arriving to the vocal box.

Dynamics of class GSM

Properties

We expressed some properties in order to verify the correctness of the model with respect to the service requirements.

The first validation consisted in ensuring the correctness of the model with respect to the main expected behaviour: each service invocation will lead to the search of the professionals corresponding to the called number.

Then we used the IF observers in order to express and verify more complex properties:

• If a call succeeds, all the other initiated calls are killed.
• A call never succeeds to the vocal box of a mobile phone.

The second property was verified on the initial model.

The satisfaction of the first property needed some remodelling. Indeed, on the initial model this property was not satisfied. After problem analysis, we found that the problem stems from an erroneous implementation of the search mechanism: the fact that the decision to kill objects was done in a distributed way, implies difficulties to define a critical section allowing a correct scheduling of message exchanges. The model was modified by centralising the scheduling decision in one component:  ParaSearch or SeqSearch. After modification of the model, the property was verified.