Model-based self-monitoring embedded programs with temporal logic specifications

ABSTRACT

We propose a model-based framework for developing self-monitoring embedded programs with temporal logic specifications. In our framework the requirement specification of an embedded program is encoded in the temporal logic MEDL. We propose an algorithm that synthesizes a model-based monitor from a MEDL script. We also introduce a technique that instruments a system model to emit events defined in the model-based primitive event definition language mPEDL. The synthesized model-based monitor may be composed with the instrumented model to form a self-monitoring model, which can be simulated for design-level verification; the composed self-monitoring model can also be used to generate a self-monitoring embedded program, which can monitor its own execution on the target platform in addition to its normal functions. Our approach combines the rigidness of temporal logic specifications with the easy use of a toolkit M²IST that we developed to automate the process of building a self-monitoring embedded program from a system model and its requirement specification.

REFERENCES

• 1: R. Alur , C. Courcoubetis , N. Halbwachs , T. A. Henzinger , P.-H. Ho , X. Nicollin , A. Olivero , J. Sifakis , S. Yovine, The algorithmic analysis of hybrid systems, Theoretical Computer Science, v.138 n.1, p.3-34, Feb. 6, 1995 [doi>10.1016/0304-3975(94)00202-T]
• 2: R. Alur, T. Dang, J. Esposito, Y. Hur, F. IvančiĆ, V. Kumar, I. Lee, P. Mishra, G. Pappas, and O. Sokolsky. Hierarchical modeling and analysis of embedded systems. Proc. of IEEE, 91:11--28, 2003.
• 3: K. Havelund and G. Rosu. Monitoring java programs with java pathexplorer. In RV'01, 2001.
• 4: M. Kim, S. Kannan, I. Lee, and O. Sokolsky. Java-mac: a run-time assurance tool for Java. In RV'01, 2001.
• 5: Oded Maler , Zohar Manna , Amir Pnueli, From Timed to Hybrid Systems, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.447-484, June 03-07, 1991
• 6: M2IST toolkit. University of pennsylvania. In http://www.cis.upenn.edu/~tanli/tools/mist.html, 2003.
• 7: Aloysius K. Mok , Guangtian Liu, Efficient Run-Time Monitoring of Timing Constraints, Proceedings of the 3rd IEEE Real-Time Technology and Applications Symposium (RTAS '97), p.252, June 09-11, 1997
• 8: Simulink and Stateflow. The MathWorks, Inc. In http://www.mathworks.com.
• 9: Janos Sztipanovits , Gabor Karsai, Model-Integrated Computing, Computer, v.30 n.4, p.110-111, April 1997 [doi>10.1109/2.585163]
• 10: L. Tan, J. Kim, and I. Lee. Testing and monitoring model-based generated program. In RV'03, volume 89 of Electronic Notes in Theo. Comp. Sci., 2003.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.6 SIMULATION AND MODELING
      I.6.4 Model Validation and Analysis

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

General Terms:
Algorithms, Design, Verification

Keywords:
embedded systems, run-time verification, temporal logic