Advertisement

Runtime Verification of Temporal Patterns for Dynamic Reconfigurations of Components

  • Julien Dormoy
  • Olga Kouchnarenko
  • Arnaud Lanoix
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7253)

Abstract

Dynamic reconfigurations increase the availability and the reliability of component-based systems by allowing their architectures to evolve at runtime. Recently we have proposed a temporal pattern logic, called FTPL, to characterize the correct reconfigurations of component-based systems under some temporal and architectural constraints.

As component-based architectures evolve at runtime, there is a need to check these FTPL constraints on the fly, even if only a partial information is expected. Firstly, given a generic component-based model, we review FTPL from a runtime verification point of view. To this end we introduce a new four-valued logic, called RV-FTPL (Runtime Verification for FTPL), characterizing the “potential” (un)satisfiability of the architectural constraints in addition to the basic FTPL semantics. Potential true and potential false values are chosen whenever an observed behaviour has not yet lead to a violation or satisfiability of the property under consideration. Secondly, we present a prototype developed to check at runtime the satisfiability of RV-FTPL formulas when reconfiguring a Fractal component-based system. The feasability of a runtime property enforcement is also shown. It consists in supervising on the fly the reconfiguration execution against desired RV-FTPL properties. The main contributions are illustrated on the example of a HTTP server architecture.

Keywords

Temporal Logic Linear Temporal Logic Java Modelling Language Architectural Element Component Architecture 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Aguilar Cornejo, M., Garavel, H., Mateescu, R., De Palma, N.: Specification and Verification of a Dynamic Reconfiguration Protocol for Agent-Based Applications. Research Report RR-4222, INRIA (2001)Google Scholar
  2. 2.
    Aguirre, N., Maibaum, T.: A temporal logic approach to the specification of reconfigurable component-based systems. In: Automated Software Engineering (2002)Google Scholar
  3. 3.
    Aldric, J.: Using types to enforce architectural structure. In: WICSA 2008, pp. 23–34 (2008)Google Scholar
  4. 4.
    Baldan, P., Corradini, A., König, B., Lluch Lafuente, A.: A Temporal Graph Logic for Verification of Graph Transformation Systems. In: Fiadeiro, J.L., Schobbens, P.-Y. (eds.) WADT 2006. LNCS, vol. 4409, pp. 1–20. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  5. 5.
    Barringer, H., Gabbay, D.M., Rydeheard, D.E.: From Runtime Verification to Evolvable Systems. In: Sokolsky, O., Taşıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 97–110. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  6. 6.
    Basin, D.A., Klaedtke, F., Müller, S., Pfitzmann, B.: Runtime monitoring of metric first-order temporal properties. In: IARCS, FSTTCS 2008, India. LIPIcs, vol. 2, pp. 49–60. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2008)Google Scholar
  7. 7.
    Bauer, A., Leucker, M., Schallhart, C.: Model-based runtime analysis of distributed reactive systems. In: ASWEC’iso 2006. IEEE (2006)Google Scholar
  8. 8.
    Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL Semantics for Runtime Verification. Journal of Logic and Computation (JLC) (2010)Google Scholar
  9. 9.
    Bellegarde, F., Groslambert, J., Huisman, M., Julliand, J., Kouchnarenko, O.: Verification of liveness properties with JML. Technical report RR-5331, INRIA (2004)Google Scholar
  10. 10.
    Bruneton, E., Coupaye, T., Leclercq, M., Quéma, V., Stefani, J.-B.: The fractal component model and its support in java. Softw., Pract. Exper. 36(11-12), 1257–1284 (2006)CrossRefGoogle Scholar
  11. 11.
    Chauvel, F., Barais, O., Borne, I., Jézéquel, J.-M.: Composition of qualitative adaptation policies. In: ASE 2008, pp. 455–458. IEEE (2008) (short paper)Google Scholar
  12. 12.
    David, P.-C., Ledoux, T., Léger, M., Coupaye, T.: FPath and FScript: Language support for navigation and reliable reconfiguration of Fractal architectures. Annales des Télécommunications 64(1-2), 45–63 (2009)CrossRefGoogle Scholar
  13. 13.
    Dormoy, J., Kouchnarenko, O.: Event-based Adaptation Policies for Fractal Components. In: AICCSA 2010, pp. 1–8. IEEE (May 2010)Google Scholar
  14. 14.
    Dormoy, J., Kouchnarenko, O., Lanoix, A.: Using Temporal Logic for Dynamic Reconfigurations of Components. In: Barbosa, L.S., Lumpe, M. (eds.) FACS 2010. LNCS, vol. 6921, pp. 200–217. Springer, Heidelberg (2010)Google Scholar
  15. 15.
    Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE, pp. 411–420 (1999)Google Scholar
  16. 16.
    Falcone, Y., Mounier, L., Fernandez, J.-C., Richier, J.-L.: Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods in System Design 38(3), 223–262 (2011)zbMATHCrossRefGoogle Scholar
  17. 17.
    Giorgetti, A., Groslambert, J., Julliand, J., Kouchnarenko, O.: Verification of class liveness properties with java modelling language. IET Software (2008)Google Scholar
  18. 18.
    Graf, S., Peled, D., Quinton, S.: Achieving Distributed Control through Model Checking. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 396–409. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  19. 19.
    Lanoix, A., Dormoy, J., Kouchnarenko, O.: Combining proof and model-checking to validate reconfigurable architectures. In: FESCA 2011. ENTCS (2011)Google Scholar
  20. 20.
    Léger, M.: Fiabilité des Reconfigurations Dynamiques dans les Architectures à Composant. PhD thesis, Ecole Nationale Supérieure des Mines de Paris (2009)Google Scholar
  21. 21.
    Léger, M., Ledoux, T., Coupaye, T.: Reliable Dynamic Reconfigurations in a Reflective Component Model. In: Grunske, L., Reussner, R., Plasil, F. (eds.) CBSE 2010. LNCS, vol. 6092, pp. 74–92. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  22. 22.
    Ligatti, J., Bauer, L., Walker, D.: Run-time enforcement of nonsafety policies. ACM TISSEC 12, 19:1–19:41 (2009)CrossRefGoogle Scholar
  23. 23.
    Schneider, F.B.: Enforceable security policies. ACM TISSEC 3, 30–50 (2000)CrossRefGoogle Scholar
  24. 24.
    Trentelman, K., Huisman, M.: Extending JML Specifications with Temporal Logic. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 334–348. Springer, Heidelberg (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Julien Dormoy
    • 1
  • Olga Kouchnarenko
    • 1
  • Arnaud Lanoix
    • 2
  1. 1.University of Franche-ComtéBesançonFrance
  2. 2.Nantes UniversityNantesFrance

Personalised recommendations