The undesired behavior is to have the gate open when the train is crossing the gate.
We want to check whether this undesired behavior can occur. To do this, we state
the problem as a model-checking problem. We generate automatically a model of the
system using the Formal Model Converter. We can also specify formally the property
that this model must satisfy, as a temporal logic property, for instance. Then we
use a model-checker to check that the model satisfies the property.
Using the Formal Model Converter with the model-checker NuSMV:
- double click on the Formal Model Converter box
- specify the Target File where the NuSMV model is to be stored
- select Kripke Structures as Model Type
- select CTL as Formula Type
- select Text Only as Output Type
- copy the following CTL formula in the Temporal Formula field:
!EF (Train.state=within & Gate.state=open)
- click Convert: you should get a file with the Kripke model
- run NuSMV on the file you just generated, e.g.:
/myPath/NuSMV myTargetFile.kripke
- you should get as output that the formula is true on this model
Using the Formal Model Converter with the model-checker Real-Time Maude:
- follow steps similar to the above, except that you should:
- select Real Time Maude Translation
- copy the following formula in the Temporal Formula field:
[] ~ ('Train @ 'within /\ 'Gate @ 'open)
- run rtmaude as follows:
/myPath/maude real-time-maude.maude
Maude> load myTargetFile.rtmaude