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.
of the architecture of the FTR&D application
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
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
Search On List
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
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
for Search Component with Timer
We decided in OMEGA to simplify this part of
There are predefined phones for fixed, mobile
and secretary user,
We decided to define only one phone of each
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 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.
of the Depannage service specification
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).
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.
between components Location and Depannage
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.
Quick answer should be followed by normal answer
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
and time constraints
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.
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
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.
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.
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
We hereafter described in more details the
behaviour of some of the classes.
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.
state machine: dynamics of class Caller
The class Depannage is mainly
responsible of the choice between the two kinds of searches. Here, we implement
this choice as non deterministic.
of class Depannage
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.
of class ParaSearch
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).
of class Search
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.
of class GSM
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
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