Abstract
State space explosion causes most relevant behavioral questions for component-based systems to be PSPACE-hard. Here, we exploit the structure of component-based systems to obtain a first approximation of the reachable global state space. In order to improve this approximation we introduce a new technique we call cross-checking. The resulting approximation can be used to study global properties of component-based systems, which we demonstrate here for local deadlock-freedom.
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
Attie, P., 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)
Allen, R., Garlan, D.: A Formal Basis for Architectural Connection. ACM Trans. Softw. Eng. Methodol. 6(3), 213–249 (1997)
Arnold, A.: Finite transition systems: semantics of communicating systems (Translator-John Plaice). Prentice Hall International (UK) Ltd., Hertfordshire (1994), Translator-John Plaice
George, A.S., Clarke, L.A., Naumovich, G.: Data flow analysis for checking properties of concurrent java programs. In: ICSE 1999: Proceedings of the 21st international conference on Software engineering, pp. 399–410. ACM, New York (1999)
Basu, A., Bozga, M., Sifakis, J.: Modeling Heterogeneous Real-time Components in BIP. In: Proceedings of SEFM 2006, pp. 3–12. IEEE Computer Society, Los Alamitos (2006)
Bernardo, M., Ciancarini, P., Donatiello, L.: Architecting Families of Software Systems with Process Algebras. ACM Trans. on Software Engineering and Methodology 11, 386–426 (2002)
Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstraction for model checking c programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 268–283. Springer, Heidelberg (2001)
de Alfaro, L., Henzinger, T.: Interface Automata. In: FSE 2001, pp. 109–120 (2001)
Esparza, J., Ganty, P., Schwoon, S.: Locality-based abstractions. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 118–134. Springer, Heidelberg (2005)
Goessler, G., Graf, S., Majster-Cederbaum, M., Martens, M., Sifakis, J.: 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. LNCS, vol. 4362, pp. 295–308. Springer, Heidelberg (2007)
Goessler, G., Graf, S., Majster-Cederbaum, M., Martens, M., Sifakis, J.: Ensuring Properties of Interaction Systems by Construction. In: Reps, T., Sagiv, M., Bauer, J. (eds.) Wilhelm Festschrift. LNCS, vol. 4444, pp. 201–224. Springer, Heidelberg (2007)
Goessler, G.: Component-based Design of Heterogeneous Reactive Systems in Prometheus. Technical Report 6057 INRIA (2006)
Goessler, 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)
Goessler, G., Sifakis, J.: Composition for Component-based Modeling. Sci. Comput. Program. 55(1-3), 161–183 (2005)
Kovalyov, A.V.:
Lynch, N.A., Tuttle, M.R.: An Introduction to Input/Output Automata. In: CWI-Quarterly, pp. 219–246 (1989)
Majster-Cederbaum, M., Martens, M.: Compositional Analysis of Tree-Like Component Architectures. In: Proceedings of EMSOFT 2008 (2008)
Majster-Cederbaum, M., Minnameier, C.: Everything is PSPACE-Complete in Interaction Systems. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 216–227. Springer, Heidelberg (2008)
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)
Majster-Cederbaum, M., Martens, M., Minnameier, C.: Liveness in Interaction Systems. In: Proceedings of FACS 2007. ENTCS (2007)
Minnameier, C., Schaube, R.: PrInSESSA - Proving Properties of Interaction Systems by Enhanced State Space Approximation (2008), http://134.155.88.3/main/chair_de/03/cmm_cross_checking/index_de.html
Sifakis, J.: Modeling Real-time Systems. In: Keynote talk RTSS 2004 (2004)
Sifakis, J.: A Framework for Component-based Construction. In: Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, pp. 293–300. IEEE Computer Society, Los Alamitos (2005)
Tanenbaum, A.: Modern Operating Systems, 3rd edn (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Majster-Cederbaum, M., Minnameier, C. (2009). Cross-Checking - Enhanced Over-Approximation of the Reachable Global State Space of Component-Based Systems. In: Bournez, O., Potapov, I. (eds) Reachability Problems. RP 2009. Lecture Notes in Computer Science, vol 5797. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04420-5_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-04420-5_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04419-9
Online ISBN: 978-3-642-04420-5
eBook Packages: Computer ScienceComputer Science (R0)