A Lightweight Container Architecture for Runtime Verification | SpringerLink
Skip to main content
Springer Nature Link
Log in

A Lightweight Container Architecture for Runtime Verification

  • Conference paper
Runtime Verification (RV 2008)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5289))

Included in the following conference series:

Abstract

We present in this paper a runtime verification architecture that enforces formal contracts for component-based systems. The contracts are based on logical assertions combined with state-transition systems. They are expressed separately from the implementation logic. A set of static analyses can be applied on the contracts but ultimately further verifications have to be performed on-line. This is the main purpose of the monitoring system we describe in this paper. The monitoring architecture is based on a model of lightweight hierarchical containers that exhibits a high-level of flexibility and extensibility. For instance, containers can be dynamically composed and unplugged on a per-instance basis. Beyond runtime verification, the monitoring architecture is reused for other purposes such as QoS monitoring and component hot-swapping. A performance comparison with other design by contract environments is also proposed.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, Englewood Cliffs (1997)

    MATH  Google Scholar 

  2. Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification, vol. 55, pp. 185–208. Elsevier, Amsterdam (2005)

    MATH  Google Scholar 

  3. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  4. Szyperski, C.: Component Software: Beyond Object-Oriented Programming. Addison-Wesley Longman Publishing Co., Inc., Boston (2002)

    MATH  Google Scholar 

  5. Deveaux, D., Jezequel, J.M.: Increase software trustability with self-testable classes in java. In: IEEE Software Engineering Conference (2001)

    Google Scholar 

  6. Karaorman, M., Hlzle, U., Bruno, J.: jContractor: A reflective Java library to support design by contract. In: Cointe, P. (ed.) Reflection 1999. LNCS, vol. 1616. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  7. Reussner, R., Poernomo, I., Schmidt, H.W.: Reasoning about software architectures with contractually specified components. In: Cechich, A., Piattini, M., Vallecillo, A. (eds.) Component-Based Software Quality. LNCS, vol. 2693, pp. 287–325. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  8. Findler, R.B., Latendresse, M., Felleisen, M.: Behavioral contracts and behavioral subtyping. In: ESEC/FSE-9: Proceedings of the 8th European software engineering conference, pp. 229–236. ACM Press, New York (2001)

    Chapter  Google Scholar 

  9. Liskov, B.H., Wing, J.M.: A behavioral notion of subtyping, vol. 16, pp. 1811–1841. ACM Press, New York (1994)

    Google Scholar 

  10. Belhaouari, H., Peschanski, F.: An integrated platform for contract-oriented development. Formal Languages and Analysis of Contract-Oriented Software (2007)

    Google Scholar 

  11. Beckert, B., Posegga, J.: leantap: Lean tableau-based deduction. J. Autom. Reasoning 15, 339–358 (1995)

    Article  MATH  Google Scholar 

  12. Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Heidelberg (1996)

    Book  MATH  Google Scholar 

  13. Toth, H.: On theory and practice of assertion based software development. Journal of Object Technology 4, 109–129 (2005)

    Article  Google Scholar 

  14. Zaremski, A.M., Wing, J.M.: Specification matching of software components, vol. 6, pp. 333–369. ACM Press, New York (1997)

    Google Scholar 

  15. Zampunieris, D., Charlier, B.L.: An efficient algorithm to compute the synchronized product, vol. 00, p. 77. IEEE Computer Society, Los Alamitos (1995)

    Google Scholar 

  16. Fowler, M.: Inversion of control containers and the dependency injection pattern (2004), http://www.martinfowler.com/articles/injection.html

  17. Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns. Addison-Wesley, Boston (1995)

    MATH  Google Scholar 

  18. Chen, F., Rosu, G.: Mop: an efficient and generic runtime verification framework. In: OOPSLA, pp. 569–588. ACM, New York (2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire d’Informatique de Paris 6, UPMC Paris Universitas, France

    Hakim Belhaouari & Frédéric Peschanski

Authors
  1. Hakim Belhaouari
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Frédéric Peschanski
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute for Informatics I4, TU Munich, Boltzmannstr. 3, 85748, Garching, Germany

    Martin Leucker

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Belhaouari, H., Peschanski, F. (2008). A Lightweight Container Architecture for Runtime Verification. In: Leucker, M. (eds) Runtime Verification. RV 2008. Lecture Notes in Computer Science, vol 5289. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89247-2_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-89247-2_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-89246-5

  • Online ISBN: 978-3-540-89247-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation