The MSC Conformity View
Note: MSC conformity check is undergoing a lot of refactorings and should therefore in AF3 2.6 be considered experimental
Introduction
AF3 allows to check that a logical architecture is conform to a given MSC (Message Sequence Chart):
- is there indeed a trace in the logical architecture which corresponds to the MSC? (``feasibility'' of the MSC in the logical architecture)
- do the MSC necessity messages indeed hold in the logical architecture?
Installing NuSMV
To use the MSC Conformity functionality in AF3, it is required to install the NuSMV mode checker.
You only have to make sure that NuSMV is in the PATH. To check whether AF3 can access NuSMV, just press the "NuSMV Version" button from the
"Analyses Master View". If NuSMV is correctly installed, a dialog showing its version
is displayed (as below), otherwise an error message will be displayed.
Using the "MSC Conformity Analyzer"
First open the "MSC Conformity" view by clicking on the button from the toolbar
.
The conformity analysis requires a component of the logical architecture and an MSC,
as show the status labels "none" in the above picture.
The selection of both can be done either by clicking directly in their editor, if open, or by clicking on their name in the Model Navigator.
Clicking the button "Check MSC conformity" then performs the analysis.
To be able to do so, the following properties must hold:
- every MSC entity must correspond to an object of the selected component (i.e., have the same name);
- every message port in the MSC must correspond to a channel port in the selected component
(except for those of external entities);
- every message must be a valid expression whose type is the one of the values carried by the channel
(e.g., if the channel carries integers, then the message itself must be an integer).
If all these requirements are satisfied then the analysis is performed.
There can be three results:
- The MSC is conform!
- The MSC is not conform!
- The MSC is not feasible!
The first case means that both the feasability and necessity analyses passed.
If so, a NuSMV example corresponding to an execution of the component which satisfies the MSC, is displayed (see below).
By pressing the "Open Simulator" button, this sequence of states can be simulated.
The second one means that the MSC is feasible but the necessity aspect of messages is not satisfied:
there exists a trace containing all the possibility messages but not one of the necessity ones.
If so, a NuSMV example corresponding to such a trace is displayed (see below), which can, again be simulated.
The third case means that the MSC is not even feasible, i.e., the sequence of messages of the MSC cannot be achieved in the
component architecture.