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
