Abstract
Verification of component-based systems still suffers from limitations such as state space explosion since a large number of different components may interact in an heterogeneous environment. Those limitations entail the need for complementary verification methods such as runtime verification based on dynamic analysis and prone to scalability. In this paper, we integrate runtime verification into the BIP (Behavior, Interaction, and Priority) framework. BIP is a powerful component-based framework for the construction of heterogeneous systems. Our method augments BIP systems with monitors checking a user-provided specification. This method has been implemented in RV-BIP, a prototype tool that we used to validate the whole approach on a robotic application.
This work is partially supported by the FP7 IP ASCENS.
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.
Similar content being viewed by others
References
Bliudze, S., Sifakis, J.: A Notion of Glue Expressiveness for Component-Based Systems. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 508–522. Springer, Heidelberg (2008)
Runtime Verification (2001-2010), http://www.runtime-verification.org
Bauer, A., Leucker, M., Schallhart, C.: Comparing ltl semantics for runtime verification. J. Log. Comput. 20, 651–674 (2010)
Falcone, Y., Fernandez, J.C., Mounier, L.: Runtime verification of safety-progress properties. In: [27], pp. 40–59
Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: 4th IEEE Int. Conf. on Software Engineering and Formal Methods (SEFM 2006), pp. 3–12 (2006)
Bliudze, S., Sifakis, J.: The algebra of connectors—structuring interaction in BIP. IEEE Transactions on Computers 57, 1315–1330 (2008)
Stolz, V.: Temporal assertions with parametrised propositions. In: Sokolsky, O., Taşıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 176–187. Springer, Heidelberg (2007)
Fleury, S., Herrb, M., Chatila, R.: GenoM: A Tool for the Specification and the Implementation of Operating Modules in a Distributed Robot Architecture. In: Proceedings of Intelligent Robots and Systems, IROS 1997, pp. 842–848. IEEE, Los Alamitos (1997)
Bensalem, S., Gallien, M., Ingrand, F., Kahloul, I., Nguyen, T.H.: Toward a more dependable software architecture for autonomous robots. IEEE Robotics and Automaton Magazine, Special issue on Soft. Engineering for Robotics 16, 67–77 (2008)
Umrigar, Z.D., Pitchumani, V.: Formal verification of a real-time hardware design. In: DAC 1983: Proceedings of the 20th Design Automation Conference, pp. 221–227. IEEE Press, Los Alamitos (1983)
Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)
Clarke, E.M., Emerson, E.A.: Synthesis of synchronisation skeletons for branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
McMillan, K.: Symbolic model checking. Kluwer Academic Publishers, Boston (1993)
Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic model checking: 1020 states and beyond. In: Proceedings of the 5th Syposium on Logic in Computer science, pp. 428–439 (1990)
Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19, 7–34 (2001)
Clarke, E., Long, D., McMillan, K.: Compositional model checking. In: Proceedings of the 4th Annual Symposium on LICS, pp. 353–362. IEEE Computer Society Press, Los Alamitos (1989)
Chang, E., Manna, Z., Pnueli, A.: Compositional verification of real-time systems. In: Symposium on Logic in Computer Science. IEEE, Los Alamitos (1994)
Long, D.E.: Model Checking, Abstraction, and Compositional Reasoning. PhD thesis, Carnegie Mellon (1993)
Bensalem, S., Bozga, M., Sifakis, J., Nguyen, T.H.: Compositional verification for component-based systems and application. Software Journal, Special Issue on Automated Compositional Verification 4, 181–193 (2010)
Bensalem, S., Bogza, M., Legay, A., Nguyen, T.H., Sifakis, J., Yan, R.: Incremental component-based construction and verification using invariants. In: FMCAD (2010)
Meyer, B.: Applying design by contract. Computer 25, 40–51 (1992)
Abadi, M., Lamport, L.: Composing specifications. ACM Transaction on Programming Languages and Systems 15, 73–132 (1993)
Ben-Hafaiedh, I., Graf, S., Quinton, S.: Reasoning about safety and progress using contracts. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 436–451. Springer, Heidelberg (2010)
Kähkönen, K., Lampinen, J., Heljanko, K., Niemelä, I.: The lime interface specification language and runtime monitoring tool. In: [27], pp. 93–100
Bodden, E., Lam, P., Hendren, L.J.: Clara: A framework for partially evaluating finite-state runtime monitors ahead of time. In: [28], pp. 183–197
Falcone, Y.: You should better enforce than verify. In: [28], pp. 89–105
Bensalem, S., Peled, D. (eds.): RV 2009. LNCS, vol. 5779. Springer, Heidelberg (2009)
Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G.J., Rosu, G., Sokolsky, O., Tillmann, N. (eds.): RV 2010. LNCS, vol. 6418. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Falcone, Y., Jaber, M., Nguyen, TH., Bozga, M., Bensalem, S. (2011). Runtime Verification of Component-Based Systems. In: Barthe, G., Pardo, A., Schneider, G. (eds) Software Engineering and Formal Methods. SEFM 2011. Lecture Notes in Computer Science, vol 7041. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24690-6_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-24690-6_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24689-0
Online ISBN: 978-3-642-24690-6
eBook Packages: Computer ScienceComputer Science (R0)