Abstract
By integrating formal specification and formal verification into the design phase of a system development process, the correctness of the system can be ensured to a great extent. However, it is not sufficient for a self-optimizing system that needs to exchange its components safely and consistently over time. Therefore, this paper presents a comprehensive verification framework to guarantee the dependability of such a self-optimizing system at the design phase (off-line verification) as well as at the runtime phase (on-line verification). The proposed verification framework adopts AsmL as intermediate representation for the system specification and on-the-fly model checking technique for alleviating the state space explosion problem. The off and the on -line verifications are performed at (RT-UML) model level. The properties to be checked are expressed by RT-OCL where the underlying temporal logic is restricted to time-annotated ACTL/LTL formulae. In particular, the on-line verification is achieved by running the on-the-fly model checking interleaved with the execution of the checked system in a pipelined manner.
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).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Giese, H., Tichy, M., Burmester, S., Schäfer, W., Flake, S.: Towards the Compositional Verification of Real-time UML Designs. In: Proceedings of the European Software Engineering Conference (ESEC), Helsinki, Finland (2003)
Giese, H., Burmester, S.: Real-time Statechart Semantics. Technical Report tr-ri-03-239, Computer Science Department, Paderborn University (2003)
Flake, S., Mueller, W.: An OCL Extension for Real-time Constraints. In: Clark, A., Warmer, J. (eds.) Object Modeling with the OCL. LNCS, vol. 2263, p. 150. Springer, Heidelberg (2002)
Emerson, E.A., Mok, A.K., Sistla, A.P., Srinivasan, J.: Quantitative temporal reasoning. In: Proceedings of the 2nd International Workshop on Computer Aided Verification, London, UK, pp. 136–145. Springer, Heidelberg (1991)
Gurevich, Y., Schulte, W., Campbell, C., Grieskamp, W.: AsmL: The Abstract State Machine Language Version 2.0., http://research.microsoft.com/~foundations/AsmL/
Gurevich, Y.: Evolving Algebras 1993: Lipari Guide. In: Börger, E. (ed.) Specification and Validation Methods. Oxford University Press, Oxford (1995)
Zhao, Y.: Build Asml Model from Real-time UML Statechart. Technical report, Heinz Nixdorf Institute, Paderborn University (2005)
Grumberg, O., Long, D.E.: Model Checking and Modular Verification. ACM Transactions on Programming Languages and Systems 16, 843–872 (1994)
Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XV, London, UK, pp. 3–18. Chapman & Hall, Ltd., Boca Raton (1995)
Shukla, S., Rosenkrantz, D.J., Hunt III, H.B., Stearns, R.E.: A HORNSAT Based Approach to the Polynomial Time Decidability of Simulation Relations for Finite State Processes. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 35. American Mathematical Society (1997)
Schaefer, T.J.: The complexity of satisfiability problems. In: Proceedings of the tenth annual ACM symposium on Theory of computing, pp. 216–226. ACM Press, New York (1978)
Ausiello, G., Italiano, G.F.: On-line algorithms for polynomially solvable satisfiability problems. J. Log. Program. 10, 69–90 (1991)
Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional horn formulae. J. Log. Program. 1, 267–284 (1984)
Itai, A., Makowshy, J.A.: Unification as a complexity measure for logic programming. J. Log. Program. 4, 105–117 (1987)
Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. Form. Methods Syst. Des. 1, 275–288 (1992)
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 (2001)
Arkoudas, K., Rinard, M.: Deductive Runtime Certification. In: Proceedings of the 2004 Workshop on Runtime Verification (RV 2004), Barcelona, Spain (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: SPIN, pp. 323–330 (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 (2001)
Zhao, Y., Oberthür, S., Kardos, M., Rammig, F.J.: Model-based runtime verification framework for self-optimizing systems. In: Proceedings of the 2005 Workshop on Runtime Verification (RV 2005), Edinburgh, Scotland, UK (2005)
Diethers, K., Goltz, U., Huhn, M.: Model checking UML statecharts with time. In: Jürjens, J., Cengarle, M.V., Fernandez, E.B., Rumpe, B., Sandner, R. (eds.) Critical Systems Development with UML – Proceedings of the UML 2002 workshop, Technische Universität München, Institut für Informatik, pp. 35–52 (2002)
Knapp, A., Merz, S., Rauh, C.: Model checking - timed uml state machines and collaborations. In: Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 395–416. Springer, Heidelberg (2002)
David, A., Möller, M.O.: From huppaal to uppaal: A translation from hierarchical timed automata to flat timed automata. Technical Report RS-01-11, BRICS (2001)
Schäfer, T., Knapp, A., Merz, S.: Model checking UML state machines and collaborations. Electronic Notes in Theoretical Computer Science 55, 13 pages (2001)
Shen, W., Compton, K.J., Huggins, J.: A toolset for supporting uml static and dynamic model checking. In: COMPSAC, pp. 147–152 (2002)
Anlauff, M.: Xasm - an extensible, component-based asm language. In: Proceedings of Abstract State Machine Workshop, pp. 69–90 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhao, Y., Kardos, M., Oberthür, S., Rammig, F.J. (2005). Comprehensive Verification Framework for Dependability of Self-optimizing Systems. In: Peled, D.A., Tsay, YK. (eds) Automated Technology for Verification and Analysis. ATVA 2005. Lecture Notes in Computer Science, vol 3707. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11562948_6
Download citation
DOI: https://doi.org/10.1007/11562948_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29209-8
Online ISBN: 978-3-540-31969-6
eBook Packages: Computer ScienceComputer Science (R0)