M2C: translate requirement to model
M2C synthesizes the runtime checker for a logic specification for safety properties and if a instrumented model file is provided, add the runtime checker to the model file. Safety property is encoded in Meta Event Definition Language (MEDL). A MEDL script defines events-things are true on some instance of the execution and conditions- facts last for a certain duration during the execution. Figure 2 shows a sample MEDL script.
import event isVisible, isInvisible, track, lost;
condition visible= [isVisible, isInvisible);
event becameTruelost= lost when visible;
alarm lostTrack=start (time(becameTruelost)-time(isVisible)>50);
End
Figure 2. dog.medl: a sample MEDL script.
In this example, MEDL script starts with the events it is monitoring. It defines condition visible as a interval between event isVisible and isInvisible. Event becameTruelost occurs when the event lost occurs and the condition visible is true. A unnamed condition is true when event becameTrueLost occurs more than 50 seconds after the event isVisible becomes true, and finally the event lostTrack is defined as the start of the unnamed condition. Note that the event lostTrack is defined as a special type of event, an alarm, which indicates that something wrong has happened.
C::=defined(C) | [E, E) | C&&C | C||C | Q>Q | Q==Q | Q< Q
E::= c | start(C) | end(C) | E||E | E&&E | E when C
Q::=time(E) | c | Q*Q | Q-Q | Q+Q | Q/Q
Figure 3. MEDL syntax [LKSO01]
Figure 3 shows the abstract syntax of MEDL. For the details of language specification, you may refer to MaC home page. Internally, M2C generates runtime checker from MEDL script. It has two options: If only MEDL script is provided but not the instrumented model file,
localhost> m2c dog.medl
Then it will produce the synthesized runtime checker for the manual instrumentation.
localhost>MEDL script parsed successfully.
localhost>The synthesized monitor is outputed to dogMonitor.cn
If a model file is provided,
localhost> p2c -i examples/cleanroom/dogInst.cn dog.pedl
Then it will produce the synthesized observer and add it to the model file as well,
localhost> PEDL script parsed successfully.
localhost>The synthesized observer is output to dogMoniter.cn
localhost>The model file is given at e:\Charon\examples\cleanroom\auto\dogInstMon\dogInst.cn
localhost>The instrumented model file is output to /home/tanli/examples/cleanroom/dogInstMon.cn
If the instrumented mode is provided and it comes with the correct information about event ids, then M2C will use this information to refer to events; otherwise, it will generate its own event maps like one below,
//* lost 0
//* track 1
//* isVisible 2
//* isInvisible 3