Abstract
We build on a framework for modelling and investigating component-based systems that strictly separates the description of behavior of components from the way they interact. We discuss various properties of system behavior as liveness, local progress, local and global deadlock, and robustness. We present a criterion that ensures liveness and can be tested in polynomial time.
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
Allen, R., Garlan, D.: A Formal Basis for Architectural Connection. ACM Trans. Softw. Eng. Methodol. 6(3), 213–249 (1997)
Aoumeur, N., Saake, G.: A Component-Based Petri Net Model for Specifying and Validating Cooperative Information Systems. Data Knowl. Eng. 42(2), 143–187 (2002)
Arbab, F.: Abstract Behavior Types: A Foundation Model for Components and Their Composition. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 33–70. Springer, Heidelberg (2003)
Attie, P.C., Chockler, H.: Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 465–481. Springer, Heidelberg (2005)
Bastide, R., Barboni, E.: Component-Based Behavioural Modelling with High-Level Petri Nets. In: MOCA’04 Aahrus, Denmark, DAIMI, pp. 37–46 (2004)
Bastide, R., Barboni, E.: Software Components: A Formal Semantics Based on Coloured Petri Nets. In: Proceedings of FACS’05. ENTCS, Elsevier, Amsterdam (2005)
Baumeister, H., Hacklinger, F., Hennicker, R., Knapp, A., Wirsing, M.: A Component Model for Architectural Programming. In: Proc. of FACS’05. ENTCS, Elsevier, Amsterdam (2005)
Berger, K. et al.: A Formal Model for Componentware. In: Leavens, G.T., Sitaraman, M. (eds.) Foundations of Component-Based Systems, pp. 189–210. Cambridge Univ. Press, Cambridge (2000)
Chouali, S., Heisel, M., Souquières, J.: Proving Component Interoperability with B Refinement. In: Proceedings of FACS’05. ENTCS, Elsevier, Amsterdam (2005)
de Alfaro, L., Henzinger, T.A.: Interface Automata. In: Proceedings of ESEC 2001, pp. 109–120 (2001)
Gössler, G., Graf, S., Majster-Cederbaum, M., Martens, M., Sifakis, J.: Establishing Properties of Interaction Systems. Full paper in preparation (2006)
Gößler, G., Sifakis, J.: Component-Based Construction of Deadlock-Free Systems. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 420–433. Springer, Heidelberg (2003)
Gößler, G., Sifakis, J.: Priority systems. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2003. LNCS, vol. 3188, pp. 314–329. Springer, Heidelberg (2004)
Gössler, G., Sifakis, J.: Composition for Component-Based Modeling. Sci. Comput. Program. 55(1-3), 161–183 (2005)
Lynch, N.A., Tuttle, M.R.: An Introduction to Input/Output Automata. CWI-Quarterly 2(3), 219–246 (1989)
Magee, J., Dulay, N., Eisenbach, S., Kramer, J.: Specifying Distributed Software Architectures. In: Botella, P., Schäfer, W. (eds.) ESEC 1995. LNCS, vol. 989, pp. 137–153. Springer, Heidelberg (1995)
Majster-Cederbaum, M., Martens, M., Minnameier, C.: A Polynomial-Time Checkable Sufficient Condition for Deadlock-Freedom of Component-Based Systems. In: van Leeuwen, J., Italiano, G.F., van der Hoek, W., Meinel, C., Sack, H., Plášil, F. (eds.) SOFSEM 2007. LNCS, vol. 4362, pp. 888–899. Springer, Heidelberg (2007)
Martens, M., Minnameier, C., Majster-Cederbaum, M.: Deciding Liveness in Component-Based Systems is NP-Hard. Technical Report tr-2006-017, University of Mannheim, Fakultät Mathematik und Informatik (2006)
Minnameier, C.: Deadlock-Detection in Component-Based Systems is NP-Hard. Technical report tr-2006-015, University of Mannheim, Fakultät Mathematik und Informatik, submited for publication (2006)
Moschoyiannis, S., Shields, M.W.: Component-Based Design: Towards Guided Composition. In: Proceedings of ACSD’03, pp. 122–131. IEEE Computer Society Press, Los Alamitos (2003)
Nierstrasz, O., Achermann, F.: A Calculus for Modeling Software Components. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 339–360. Springer, Heidelberg (2003)
Pnueli, A.: In Transition from Global to Modular Temporal Reasoning about Programs. In: Logics and Models for Concurrent Systems, vol. 13, Springer, Heidelberg (1985)
Sifakis, J.: A Framework for Component-Based Construction. In: Proceedings of SEFM 05, IEEE Computer Society Press, Los Alamitos (2005)
Völzer, H., Varacca, D., Kindler, E.: Defining Fairness. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 458–472. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Gössler, G., Graf, S., Majster-Cederbaum, M., Martens, M., Sifakis, J. (2007). An Approach to Modelling and Verification of Component Based Systems. In: van Leeuwen, J., Italiano, G.F., van der Hoek, W., Meinel, C., Sack, H., Plášil, F. (eds) SOFSEM 2007: Theory and Practice of Computer Science. SOFSEM 2007. Lecture Notes in Computer Science, vol 4362. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69507-3_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-69507-3_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69506-6
Online ISBN: 978-3-540-69507-3
eBook Packages: Computer ScienceComputer Science (R0)