Abstract
A complementary verification method for real-time application with dynamic task structure has been developed. Here the real-time application is developed by means of Model-Driven Engineering. The basic verification technique is given by model checking. However, the model checking is executed at run-time whenever some reconfiguration of the task set takes place. Instead of exploring the entire state space of the model to be checked, only a partial state space at model level covering the execution trace of the checked task is explored. This on-line model checking can be seen as an extension to the traditional schedulability acceptance test which is needed anyway in systems with dynamic task set. Therefore this runtime verification is implemented as a service of the underlying operating system. In this paper we describe this method in general, explain some design and implementation decisions and provide experimental results.
This work is developed in the course of the Collaborative Research Center 614 - Self-Optimizing Concepts and Structures in Mechanical Engineering - Paderborn University, and is published on its behalf and funded by the Deutsche Forschungsgemeinschaft (DFG).
Chapter PDF
Similar content being viewed by others
References
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996); Foreword By-Wolper, Pierre
Berezin, S., Campos, S.V.A., Clarke, E.M.: Compositional reasoning in model checking. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 81–102. Springer, Heidelberg (1998)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)
Lee, W., Pardo, A., Jang, J.Y., Hachtel, G., Somenzi, F.: Tearing based automatic abstraction for ctl model checking. In: ICCAD 1996: Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, Washington, DC, USA, pp. 76–81. IEEE Computer Society, Los Alamitos (1996)
Zhao, Y., Oberthür, S., Kardos, M., Rammig, F.J.: Model-based runtime verification framework for self-optimizing systems. Electr. Notes Theor. Comput. Sci. 144(4), 125–145 (2006)
Zhao, Y., Rammig, F.J.: Model-based runtime verification framework. In: Proceedings of the Formal Engineering Approaches to Software Components and Architectures (FESCA 2009), New York, UK (March 2009)
Kent, S.: Model driven engineering. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 286–298. Springer, Heidelberg (2002)
Clark, E.M., Grumberg Jr., O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Baehni, S., Baldoni, R., Guerraoui, R., Pochon, B.: The driving philosophers. Technical report. In: Proceedings of the 3rd IFIP International Conference on Theoretical Computer Science (TCS 2004) (2004)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE 1999: Proceedings of the 21st international conference on Software engineering, pp. 411–420. IEEE Computer Society Press, Los Alamitos (1999)
Barnett, M., Schulte, W.: Spying on components: A runtime verification technique. In: Leavens, G.T., Sitaraman, M., Giannakopoulou, D. (eds.) Workshop on Specification and Verification of Component-Based Systems (October 2001)
Arkoudas, K., Rinard, M.: Deductive Runtime Certification. In: Proceedings of the 2004 Workshop on Runtime Verification (RV 2004), Barcelona, Spain (April 2004)
Tasiran, S., Qadeer, S.: Runtime Refinement Checking of Concurrent Data Structures. In: Proceedings of the 2004 Workshop on Runtime Verification (RV 2004), Barcelona, Spain (April 2004)
Chen, F., Rosu, G.: Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation. In: Proceedings of the 2003 Workshop on Runtime Verification (RV 2003), Boulder, Colorado, USA (2003)
Drusinsky, D.: The Temporal Rover and the ATG Rover. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 323–330. Springer, Heidelberg (2000)
Havelund, K., Rosu, G.: Java PathExplorer — a runtime verification tool. In: Proceedings 6th International Symposium on Artificial Intelligence, Robotics and Automation in Space (ISAIRAS 2001), Montreal, Canada (June 2001)
Easwaran, A., Kannan, S., Sokolsky, O.: Steering of discrete event systems: Control theory approach. Electr. Notes Theor. Comput. Sci. 144(4), 21–39 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rammig, F.J., Zhao, Y., Samara, S. (2009). On-Line Model Checking as Operating System Service. In: Lee, S., Narasimhan, P. (eds) Software Technologies for Embedded and Ubiquitous Systems. SEUS 2009. Lecture Notes in Computer Science, vol 5860. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10265-3_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-10265-3_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-10264-6
Online ISBN: 978-3-642-10265-3
eBook Packages: Computer ScienceComputer Science (R0)