Compositional analysis of deadlock-freedom for tree-like component architectures

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.

REFERENCES

• 1: Robert Allen , David Garlan, A formal basis for architectural connection, ACM Transactions on Software Engineering and Methodology (TOSEM), v.6 n.3, p.213-249, July 1997 [doi>10.1145/258077.258078]
• 2: 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.
• 3: 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.
• 4: 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.
• 5: R. Bastide and E. Barboni. Software Components: A Formal Semantics Based on Coloured Petri Nets. In Proceedings of FACS'05, ENTCS, 2005.
• 6: Ananda Basu , Marius Bozga , Joseph Sifakis, Modeling Heterogeneous Real-time Components in BIP, Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods, p.3-12, September 11-15, 2006 [doi>10.1109/SEFM.2006.27]
• 7: 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.
• 8: Marco Bernardo , Paolo Ciancarini , Lorenzo Donatiello, Architecting families of software systems with process algebras, ACM Transactions on Software Engineering and Methodology (TOSEM), v.11 n.4, p.386-426, October 2002 [doi>10.1145/606612.606614]
• 9: M. Bozga, O.Constant, B. Josko, Q. Ma, and M. Skipper. SPEEDS Metamodel Syntax and Static Semantics, February 2007. Deliverable D2.1b.
• 10: 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.
• 11: 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.
• 12: Luca de Alfaro , Thomas A. Henzinger, Interface automata, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 13: Patrice Godefroid , Pierre Wolper, Using partial orders for the efficient verification of deadlock freedom and safety properties, Formal Methods in System Design, v.2 n.2, p.149-164, April 1993 [doi>10.1007/BF01383879]
• 14: G. Gössler. Component-based Design of Heterogeneous Reactive Systems in Prometheus. Technical report 6057, INRIA, December 2006.
• 15: Gregor Gössler , Sussane Graf , Mila Majster-Cederbaum , M. Martens , Joseph Sifakis, An Approach to Modelling and Verification of Component Based Systems, Proceedings of the 33rd conference on Current Trends in Theory and Practice of Computer Science, January 20-26, 2007, Harrachov, Czech Republic [doi>10.1007/978-3-540-69507-3_24]
• 16: 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.
• 17: 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.
• 18: G. Gössler and J. Sifakis. Composition for Component-Based Modeling. In Proceedings of FMCO 02, volume 2852 of LNCS, pages 443--466, 2003.
• 19: G. Gössler and J. Sifakis. Priority Systems. In Proceedings of FMCO'03), volume 3188 of LNCS, pages 314--329, 2004.
• 20: Gregor Gössler , Joseph Sifakis, Composition for component-based modeling, Science of Computer Programming, v.55 n.1-3, p.161-183, March 2005 [doi>10.1016/j.scico.2004.05.014]
• 21: Paola Inverardi , Sebastián Uchitel, Proving Deadlock Freedom in Component-Based Programming, Proceedings of the 4th International Conference on Fundamental Approaches to Software Engineering, p.60-75, April 02-06, 2001
• 22: N. A. Lynch and M. R. Tuttle. An Introduction to Input/Output Automata. CWI-Quarterly, 2(3):219--246, Sept. 1989.
• 23: Mila Majster-Cederbaum , Moritz Martens, Robustness in Interaction Systems, Proceedings of the 27th IFIP WG 6.1 international conference on Formal Techniques for Networked and Distributed Systems, June 27-29, 2007, Tallinn, Estonia [doi>10.1007/978-3-540-73196-2_21]
• 24: Mila Majster-Cederbaum , Moritz Martens , Christoph Minnameier, A Polynomial-Time Checkable Sufficient Condition for Deadlock-Freedom of Component-Based Systems, Proceedings of the 33rd conference on Current Trends in Theory and Practice of Computer Science, January 20-26, 2007, Harrachov, Czech Republic [doi>10.1007/978-3-540-69507-3_77]
• 25: M. Majster-Cederbaum, M. Martens, and C. Minnameier. Liveness in Interaction Systems. In Proceedings of FACS'07, ENTCS, 2007.
• 26: 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.
• 27: Mila Majster-Cederbaum , Christoph Minnameier, Everything Is PSPACE-Complete in Interaction Systems, Proceedings of the 5th international colloquium on Theoretical Aspects of Computing, p.216-227, September 01-03, 2008, Istanbul, Turkey [doi>10.1007/978-3-540-85762-4_15]
• 28: M. Martens and M. Majster-Cederbaum. Deadlock-Freedom for Acyclic Component Architectures with Multiway Cooperation, 2008. submitted for publication.
• 29: S. Moschoyiannis , M. W. Shields, Component-Based Design: Towards Guided Composition, Proceedings of the Third International Conference on Application of Concurrency to System Design, p.122, June 18-20, 2003
• 30: O. Nierstrasz and F. Achermann. A Calculus for Modeling Software Components. In Proceedings of FMCO'02, volume 2852 of LNCS, pages 339--360, 2003.
• 31: 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.
• 32: Joseph Sifakis, Modeling Real-Time Systems, Proceedings of the 25th IEEE International Real-Time Systems Symposium, p.5-6, December 05-08, 2004 [doi>10.1109/REAL.2004.34]
• 33: Joseph Sifakis, A Framework for Component-based Construction Extended Abstract, Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, p.293-300, September 07-09, 2005 [doi>10.1109/SEFM.2005.3]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques; Mechanical verification

General Terms:
Design, Theory, Verification

Keywords:
architecture, component-based systems, compositionality, deadlock-freedom, design patterns, interaction systems