research-article

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

Authors:

Mila Majster-Cederbaum,

Moritz MartensAuthors Info & Claims

EMSOFT '08: Proceedings of the 8th ACM international conference on Embedded software

Pages 199 - 206

https://doi.org/10.1145/1450058.1450085

Published: 19 October 2008 Publication History

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]

R. Allen and D. Garlan. A Formal Basis for Architectural Connection. ACM Trans. Softw. Eng. Methodol., 6(3):213--249, 1997.

Digital Library

[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.

Digital Library

[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]

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.

Digital Library

[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]

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.

Digital Library

[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]

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.

Digital Library

[13]

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.

Digital Library

[14]

G. Gössler. Component-based Design of Heterogeneous Reactive Systems in Prometheus. Technical report 6057, INRIA, December 2006.

[15]

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.

Digital Library

[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]

G. Gössler and J. Sifakis. Composition for component-based modeling. Sci. Comput. Program., 55(1-3):161--183, 2005.

Digital Library

[21]

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.

Digital Library

[22]

N. A. Lynch and M. R. Tuttle. An Introduction to Input/Output Automata. CWI-Quarterly, 2(3):219--246, Sept. 1989.

[23]

M. Majster-Cederbaum and M. Martens. Robustness in Interaction Systems. In Proceedings of FORTE'07, volume 4574 of LNCS, pages 325--340, 2007.

Digital Library

[24]

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.

Digital Library

[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.

Digital Library

[27]

M. Majster-Cederbaum and C. Minnameier. Everything is PSPACE-complete in Interaction Systems, 2008. Accepted for Publication at ICTAC'08.

Digital Library

[28]

M. Martens and M. Majster-Cederbaum. Deadlock-Freedom for Acyclic Component Architectures with Multiway Cooperation, 2008. submitted for publication.

[29]

S. Moschoyiannis and M. Shields. Component-Based Design: Towards Guided Composition. In Proceedings ACSD'03, pages 122--131. IEEE Computer Society, 2003.

Digital Library

[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.

Digital Library

[32]

J. Sifakis. Modeling Real-time Systems. In Proceedings of RTSS'04, pages 5--6. IEEE Computer Society, 2004.

Digital Library

[33]

J. Sifakis. A Framework for Component-Based Construction. In Proceedings of SEFM'05, pages 293 -- 300. IEEE Computer Society, 2005.

Digital Library

Cited By

Oliveira MAntonino PRamos RSampaio AMota ARoscoe A(2016)Rigorous development of component-based systems using component metadata and patternsFormal Aspects of Computing10.1007/s00165-016-0375-128:6(937-1004)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1007/s00165-016-0375-1
Majster-Cederbaum MSemmelrock N(2015)A basis for compositionally ensuring safety properties and its connection to relational algebraic operatorsScience of Computer Programming10.1016/j.scico.2014.07.00698:P4(516-530)Online publication date: 1-Feb-2015
https://dl.acm.org/doi/10.1016/j.scico.2014.07.006
Majster-Cederbaum MSemmelrock N(2013)Reachability in Cooperating Systems with Architectural Constraints is PSPACE-CompleteElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.138.1138(1-11)Online publication date: 30-Dec-2013
https://doi.org/10.4204/EPTCS.138.1
Show More Cited By

Index Terms

Compositional analysis of deadlock-freedom for tree-like component architectures
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program specifications
      2. Program verification

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 Engineering

We 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

EMSOFT '08: Proceedings of the 8th ACM international conference on Embedded software

October 2008

284 pages

ISBN:9781605584683

DOI:10.1145/1450058

Program Chairs:
Luca de Alfaro
University of California, Santa Cruz
,
Jens Palsberg
University of California, Los Angeles

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 October 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ESWEEK 08

Sponsor:

ESWEEK 08: Fourth Embedded Systems Week

October 19 - 24, 2008

GA, Atlanta, USA

Acceptance Rates

Overall Acceptance Rate 60 of 203 submissions, 30%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
189
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Oliveira MAntonino PRamos RSampaio AMota ARoscoe A(2016)Rigorous development of component-based systems using component metadata and patternsFormal Aspects of Computing10.1007/s00165-016-0375-128:6(937-1004)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1007/s00165-016-0375-1
Majster-Cederbaum MSemmelrock N(2015)A basis for compositionally ensuring safety properties and its connection to relational algebraic operatorsScience of Computer Programming10.1016/j.scico.2014.07.00698:P4(516-530)Online publication date: 1-Feb-2015
https://dl.acm.org/doi/10.1016/j.scico.2014.07.006
Majster-Cederbaum MSemmelrock N(2013)Reachability in Cooperating Systems with Architectural Constraints is PSPACE-CompleteElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.138.1138(1-11)Online publication date: 30-Dec-2013
https://doi.org/10.4204/EPTCS.138.1
Li CHuang LChen LLuo W(2013)Deadlock detection and recovery for component-based systemsMathematical and Computer Modelling10.1016/j.mcm.2012.12.03558:5-6(1362-1378)Online publication date: Sep-2013
https://doi.org/10.1016/j.mcm.2012.12.035
Lambertz CMajster-Cederbaum M(2011)Analyzing component-based systems on the basis of architectural constraintsProceedings of the 4th IPM international conference on Fundamentals of Software Engineering10.1007/978-3-642-29320-7_5(64-79)Online publication date: 20-Apr-2011
https://dl.acm.org/doi/10.1007/978-3-642-29320-7_5
Lambertz CMajster-Cederbaum M(2010)Port Protocols for Deadlock-Freedom of Component SystemsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.38.338(7-11)Online publication date: 26-Oct-2010
https://doi.org/10.4204/EPTCS.38.3
Hennicker RJanisch SKnapp A(2010)On the Observable Behaviour of Composite ComponentsElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2009.12.035260(125-153)Online publication date: 1-Jan-2010
https://dl.acm.org/doi/10.1016/j.entcs.2009.12.035
Majster-Cederbaum MMinnameier C(2009)Cross-Checking - Enhanced Over-Approximation of the Reachable Global State Space of Component-Based SystemsProceedings of the 3rd International Workshop on Reachability Problems10.1007/978-3-642-04420-5_18(189-202)Online publication date: 27-Aug-2009
https://dl.acm.org/doi/10.1007/978-3-642-04420-5_18
Majster-Cederbaum MMinnameier C(2008)Everything Is PSPACE-Complete in Interaction SystemsProceedings of the 5th international colloquium on Theoretical Aspects of Computing10.1007/978-3-540-85762-4_15(216-227)Online publication date: 1-Sep-2008
https://dl.acm.org/doi/10.1007/978-3-540-85762-4_15

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten