CETIC

20. The Requirements Animator

Christophe PONSARD — 2009-03-12T09:21:00Z

This article shows the goal-oriented requirements animator in action through some movies and snapshots. A demo version of the animator itself will be downloadable soon.

View the animator in action

The following videos require macromedia flash player. They were captured in 1024x768 and are best viewed in full screen or in a larger resolution.

Presentation of the train system [1'17] : this video explains the KAOS model of the railway system which will be animated. It is shown in the Objectiver requirements engineering tool in which the animator is integrated.

Starting the animator server [0'14] : this very short video show how to start an animator server and the P-FSM compilation step.

Playing a scenario with two trains [3'12] : this video truly shows the animator in action. An animator actor is started and connected to the animator server. Then a pre-recorded scenario is loaded and executed step-by-step. Various operations application are shown in parallel on multiple train/car instances: train progress, train stop at a station, door opening/closing, train/car crossing a gate, etc.

Monitoring a goal violation [2'28] : this last video shows the animator watchdog in action for monitoring a simple safety property Maintain[DoorClosedWhileMoving]. In the illustrated scenario, a model error allows a train to be started with its doors opened. Relevant events are logged and the goal violation detected. The origin of the error is then traced.

Some Animator Snapshots


Animation of the train system

10. The Refinement Checker

Christophe PONSARD — 2009-03-12T09:20:48Z

This article shows some screenshots and video of the early V&V tool in action.

What is the early formal V&V tool about ?

The purpose of this tool is to verify the correctness of KAOS constructs such as refinements and operationalisations. Those checks are local in nature and rely on the use of model-checking technology. By the production of related examples or counter-examples, this also allows the analyst to validate his work, especially when used together with the Requirements Animator.

View the tool in action

The following videos require macromedia flash player. They were captured in 1024x768 and are best viewed in full screen or in a larger resolution.

Presentation of the model of the train system [0'59] : this video explains the KAOS model of the railway system which will be animated. It is shown in the Objectiver requirements engineering tool in which the animator is integrated.

An Incorrect Goal Refinement [0'46] : in the inital model, the goal Achieve[TrainProgress] is refined into Achieve[SignalSetToGo] and Achieve[ProgressWhenSignalSetToGo]. Running the tool reveals a counter-example indicating the refinement is incomplete.

Correcting the Refinement [0'52] : the problem is fixed by requiring that a train should keep waiting by adding the goal Maintain[TrainWaiting]. The new check shows no more counter-example (on the searched domain).

Checking Operationalisations [2'52] : the verification of the equivalence between operations and the operationalized goal is illustrated on the operation MoeTrainToNextBlock and the goal Achieve[ProgressWhenGoSignal]

A Form-based Interface [2'32] : besides the textual interface, a form-based interface is also available. Through it, the analyst can easily configure the required parameters by simple drag'n drop of goals, instances, domain properties, etc.

Generating Check Reports [5'44] : this video shows how it is easy to generate both HTML and RTF documentation of the performed checks. It heavily relies on the Objectiver infrastructure for this.

[More advanced] Checking Conflicts and Obstructions [7'24] : other KAOS constructs can also be formally verified such as obstructions and conflicts. This video shows some related checks.

Some snapshots

30. The Acceptance Tests Generator

Christophe PONSARD — 2009-03-12T09:20:34Z

Acceptance tests are crucial, for example for getting the assurance that a subcontracted development meets its requirements. The FAUST generator enables the analyst to define high quality acceptance tests from requirements documents.

Acceptance Tests

The purpose of testing is to provide a reasonable assurance of the correction of the developed code. This also means that tests are not about proving the code is correct: all behavior cannot be inspected. The assurance is provided by a coverage criterion.

Several kind of tests can be distinguished because correction can be expressed in relation with different kinds of documents expressing the system behavior at different levels : from the component level (unit tests), design level (integration tests), up to the software reception by the customer (acceptance tests). Those levels are best illustrated by the "V-model" in the following figure.


The V-Model.

The purpose of the FAUST toolbox is to help achieving high assurance in the Requirements Engineering (RE) process. With respect to testing its area is acceptance testing. The approach is goal-oriented and the acceptance tests cases are thus generated from a goal-model. It has a number of interesting properties:
test generation does not require an operational model: a prescriptive model is enough (ie. a model stating the required properties but now how to achieve them). This allows one to genere high level tests without imposing specific design choices.
the coverage criterion is goal-based: the potential system behaviors stated in the goals have to be covered.
besides the goals, others concepts are also taken into accounts such as the possible refinement pattern (such as case/milestone) and obstacles/conflicts (ie impedimenting the goal realisation and thus revealing limit conditions)

In this introductory article we will just highlight how the test generator works without entering into implementation details which rely on constraint programming. For more information the interested reader is directed to the article "Deriving Acceptance Tests from Goal Requirements".

A Simple Example

As simple example, let's consider an elementary train boarding system depicted hereafter. The system is composed of a boarding block with a direct access to it and a waiting block in case a train is already on the boarding block.


Train Example: Domain.

Among the goals, one can distinguish:
progress goals, stating that every incoming train will eventually leave the system unloaded.
safety goals: train crash have to be avoided. In our system we will explicitely choose a block system design with at most one train per block.

In this example, acceptance tests generation is essentially derived from the progress goals so we will only refine them in the following figure:


Train Example: Goal Model

In the process of the elaboration of that goal model, the following object model stating the vocabulary used in the temporal logic assertion is also produced.


Train Example: Object Model.

Acceptance Tests Generation

The acceptance tests generation process is composed of two major steps:
acceptance tests classes are elaborated, for now mainly based on the information in the goal refinements. In the above example composed of one "case" refinement and two "milestone" refinement: the case refinement will give rise to two classes of step-by-step temporal behaviors.
best representatives are chosen in those tests classes based on a number of heuristics such as minimal length traces (maximal progress), reaching limit conditions (temporal constraints, untils...). Moreover some well chosen contextual information is also required such as initial/final states, and the number of instances being considered.

Acceptances tests are generated by unfolding temporal formulas which can be translated into a constraint problem for exploring all possible behaviors. Additional constraints are then added for specifying tests classes and the representative selection criterion. The resulting set of constraints is fed into a constraint solver that yields a concrete test trace.

The resulting trace can be depicted as a scenario between the system under test and its operational environment. As exemple the following figure shows an interesting limit test where two trains are introduced into the system: the first heading directly to the unload block and the second going through the waiting block until the unload block becomes free.


Train Example: Generated Test.