What is M2IST?
M2IST stands for Model-based Monitor Instrumenting and Synthesizing Toolkit. It is a software pacakge which implements model-based monitoring, initially proposed in [TKL03]. Model-based monitoring enhances system models with model-based runtime verifiers so that the enhanced models could verify their own execution. Figure 1 shows the concept of model-based runtime verification.
Figure 1 The concept of model-based runtime verification
Model-based monitoring has the following characteristics,
1. Provide runtime assurance to the practice of model-based design.
2. Require no changes on the original model-based design environment. It works on models, not on the structure of existing tools.
3. Provide both design-level and implementation-level validations. The enhanced model is nothing but a regular model in the targeted design language, so the existing code generation mechinism can be deployed to generate a self-monitoring program from the enhanced model.
The targeted design language in MIST is CHARON, a modeling langage for hybrid system. The safety property in MIST is given in MEDL, a linear temporal logic instroduced in MaC system for program monitoring. MIST synthesize a runtime verifier in CHARON , instrumenting model to emit events, and finally add the runtime verifier to the instrumented model, and all of them are done automatically.
How does it work?
M2IST has two parts: P2C is a software program which can synthesize observers and, if a system model is provided, instrument the original system model; M2C is a software program which can synthesize monitors (runtime checkers) and, if a instrumented model is provided, add the runtime checkers to the instrumented model.
How may I use it?
Model your system in CHARON, write the properties you wish to monitor in MEDL, and let M2IST do the rest of job. It is that simple and best of all, it is free, so check out it now. Click left side button for more information on how to use each individual component in MIST.
One possible way of learning MIST is to follow the case study on SONY Robotic dog. In the case study, we provide the CHARON model, MEDL script, and PEDL script for this example. You may also find the step-by-step instruction for specifying the property, applying MIST, and carrying out design-level and implementation-level validation.
Questions and comments?
Please contact Li Tan with your questions or comments.