Mila Majster-Cederbaum
ABSTRACT
We study architectural constraints for component systems in order to be able to guarantee safety-properties. Representing safety-properties, we investigate deadlock-freedom. We present a compositional and hence polynomial time condition for deadlock-freedom for a class of component-systems whose architecture is tree-like. The architectural constraints that are developed can be understood as a design pattern that helps to construct systems satisfying safety-properties on the one hand. On the other hand, they might help to draw attention to potentially critical situations in a design. To model component-systems we use the formalism of interaction systems as proposed by Sifakis et al. The ideas can be transferred to other formal models where subsystems are cooperating via synchronous communication.
- R. Allen and D. Garlan. A Formal Basis for Architectural Connection. ACM Trans. Softw. Eng. Methodol., 6(3):213--249, 1997. Google Scholar
Digital Library
- F. Arbab. Abstract Behavior Types: A Foundation Model for Components and Their Composition. In Proceedings of FMCO'02, volume 2852 of LNCS, pages 339--360, 2003.Google Scholar
- P. Attie and H. Chockler. Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs. In Proceedings of VMCAI'05, volume 3385 of LNCS, pages 465--481, 2005. Google ScholarDigital Library
- E. Badouel, A. Benveniste, M. Bozga, B. Caillaud, O.Constant, B. Josko, Q. Ma, R. Passerone, and M. Skipper. SPEEDS Metamodel Syntax and Draft Semantics, January 2007. Deliverable D2.1c.Google Scholar
- R. Bastide and E. Barboni. Software Components: A Formal Semantics Based on Coloured Petri Nets. In Proceedings of FACS'05, ENTCS, 2005.Google Scholar
- A. Basu, M. Bozga, and J. Sifakis. Modeling Heterogeneous Real-Time Components in BIP. In Proceedings of SEFM'06, pages 3--12. IEEE Computer Society, 2006. Google ScholarDigital Library
- H. Baumeister, F. Hacklinger, R. Hennicker, A. Knapp, and M. Wirsing. A Component Model for Architectural Programming. In Proceedings of FACS'05, volume 160 of ENTCS, pages 75--96. Elsevier, 2006.Google Scholar
- M. Bernardo, P. Ciancarini, and L. Donatiello. Architecting Families of Software Systems with Process Algebras. ACM Trans. on Software Engineering and Methodology, 11:386 -- 426, October 2002. Google ScholarDigital Library
- M. Bozga, O.Constant, B. Josko, Q. Ma, and M. Skipper. SPEEDS Metamodel Syntax and Static Semantics, February 2007. Deliverable D2.1b.Google Scholar
- M. Broy. Towards a Logical Basis of Software Engineering. In M. Broy and R. Steinbrüggen, editors, Calculational System Design, IOS 1999, volume 158 of NATO ASI Series, Series F: Computer and System Sciences, pages 101 -- 131. 1999.Google Scholar
- S. Chouali, M. Heisel, and J. Souquières. Proving Component Interoperability with B Refinement. In Proceedings of FACS 05, volume 160 of ENTCS, pages 67--84, 2006.Google Scholar
- L. de Alfaro and T. A. Henzinger. Interface Automata. In Proceedings of the Ninth Annual Symposium on Foundations of Software Engineering (FSE 01), pages 109--120, 2001. Google ScholarDigital Library
- P. Godefroid and P. Wolper. Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. Form. Methods Syst. Des., 2(2):149--164, 1993. Google ScholarDigital Library
- G. Gössler. Component-based Design of Heterogeneous Reactive Systems in Prometheus. Technical report 6057, INRIA, December 2006.Google Scholar
- G. Gössler, S. Graf, M. Majster-Cederbaum, M. Martens, and J. Sifakis. An Approach to Modelling and Verification of Component Based Systems. In Proceedings of SOFSEM 07, volume 4362 of LNCS, pages 295--308, 2007. Google ScholarDigital Library
- G. Gössler, S. Graf, M. Majster-Cederbaum, M. Martens, and J. Sifakis. Ensuring Properties of Interaction Systems. In Program Analysis and Computation, Theory and Practice, volume 4444 of LNCS, pages 201--224, 2007.Google Scholar
- G. Gössler and J. Sifakis. Component-Based Construction of Deadlock-Free Systems. In Proceedings of FSTTCS'03, volume 2914 of LNCS, pages 420--433, 2003.Google Scholar
- G. Gössler and J. Sifakis. Composition for Component-Based Modeling. In Proceedings of FMCO 02, volume 2852 of LNCS, pages 443--466, 2003.Google Scholar
- G. Gössler and J. Sifakis. Priority Systems. In Proceedings of FMCO'03), volume 3188 of LNCS, pages 314--329, 2004.Google Scholar
- G. Gössler and J. Sifakis. Composition for component-based modeling. Sci. Comput. Program., 55(1-3):161--183, 2005. Google ScholarDigital Library
- P. Inverardi and S. Uchitel. Proving Deadlock Freedom in Component-Based Programming. In Proceedings of FASE'01, volume 2029 of LNCS, pages 60--75, 2001. Google ScholarDigital Library
- N. A. Lynch and M. R. Tuttle. An Introduction to Input/Output Automata. CWI-Quarterly, 2(3):219--246, Sept. 1989.Google Scholar
- M. Majster-Cederbaum and M. Martens. Robustness in Interaction Systems. In Proceedings of FORTE'07, volume 4574 of LNCS, pages 325--340, 2007. Google ScholarDigital Library
- M. Majster-Cederbaum, M. Martens, and C. Minnameier. A Polynomial-Time-Checkable Sufficient Condition for Deadlock-freeness of Component Based Systems. In Proceedings of SOFSEM 07, volume 4362 of LNCS, pages 888--899, 2007. Google ScholarDigital Library
- M. Majster-Cederbaum, M. Martens, and C. Minnameier. Liveness in Interaction Systems. In Proceedings of FACS'07, ENTCS, 2007.Google Scholar
- M. Majster-Cederbaum and C. Minnameier. Deriving Complexity Results for Interaction Systems from 1-safe Petri Nets. In Proceedings of SOFSEM'08, volume 4910 of LNCS, pages 352--363. Springer, 2008. Google ScholarDigital Library
- M. Majster-Cederbaum and C. Minnameier. Everything is PSPACE-complete in Interaction Systems, 2008. Accepted for Publication at ICTAC'08. Google ScholarDigital Library
- M. Martens and M. Majster-Cederbaum. Deadlock-Freedom for Acyclic Component Architectures with Multiway Cooperation, 2008. submitted for publication.Google Scholar
- S. Moschoyiannis and M. Shields. Component-Based Design: Towards Guided Composition. In Proceedings ACSD'03, pages 122--131. IEEE Computer Society, 2003. Google ScholarDigital Library
- O. Nierstrasz and F. Achermann. A Calculus for Modeling Software Components. In Proceedings of FMCO'02, volume 2852 of LNCS, pages 339--360, 2003.Google Scholar
- P. Parizek and F. Plasil. Modeling Environment for Component Model Checking from Hierarchical Architecture. In Proceedings of FACS'06, volume 182 of ENTCS, pages 139--153. Elsevier, 2007. Google ScholarDigital Library
- J. Sifakis. Modeling Real-time Systems. In Proceedings of RTSS'04, pages 5--6. IEEE Computer Society, 2004. Google ScholarDigital Library
- J. Sifakis. A Framework for Component-Based Construction. In Proceedings of SEFM'05, pages 293 -- 300. IEEE Computer Society, 2005. Google ScholarDigital Library
Index Terms
- Compositional analysis of deadlock-freedom for tree-like component architectures
Recommendations
Using Architectural Constraints for Deadlock-Freedom of Component Systems with Multiway Cooperation
TASE '09: Proceedings of the 2009 Third IEEE International Symposium on Theoretical Aspects of Software EngineeringWe present a compositional analysis of deadlock-freedom in component systems with multiway cooperation. We require the systems to satisfy architectural constraints which make sure that the communication structure between the components is given by a ...
Deadlock-freedom in component systems with architectural constraints
We present a compositional analysis of deadlock-freedom in component systems with multiway cooperation. We require the systems to satisfy an architectural constraint which makes sure that the communication structure between the components is given by a ...
Component-based verification using incremental design and invariants
We propose invariant-based techniques for the efficient verification of safety and deadlock-freedom properties of component-based systems. Components and their interactions are described in the BIP language. Global invariants of composite components are ...
Comments