Article

Component-interaction automata as a verification-oriented component-based system specification

Authors:

Pavlína Vařeková,

Barbora ZimmerovaAuthors Info & Claims

SAVCBS '05: Proceedings of the 2005 conference on Specification and verification of component-based systems

Pages 4 - es

https://doi.org/10.1145/1123058.1123063

Published: 05 September 2005 Publication History

Abstract

In the paper, we present a new approach to component interaction specification and verification process which combines the advantages of both architecture description languages (ADLs) at the beginning of the process, and a general formal verification-oriented model connected to verification tools at the end. After examining current general formal models with respect to their suitability for description of component-based systems, we propose a new verification-oriented model, Component-Interaction automata, and discuss its features. The model is designed to preserve all the interaction properties to provide a rich base for further verification, and allows the system behaviour to be configurable according to the architecture description (bindings among components) and other specifics (type of communication used in the synchronization of components).

References

[1]

Divine - Distributed Verification Environment. http://anna.fi.muni.cz/divine.

[2]

J. Adamek and F. Plasil. Behavior protocols capturing errors and updates. In Proceedings of the Second International Workshop on Unanticipated Software Evolution (USE 2003), ETAPS, pages 17--25, Warsaw, Poland, April 2003. University of Warsaw, Poland.

[3]

R. J. Allen. A Formal Approach to Software Architecture. PhD thesis, Carnegie Mellon University, School of Computer Science, May 1997.

Digital Library

[4]

J. Barnat, L. Brim, I. Černá, and P. Šimeček. Divine - The Distributed Verification Environment. In Proceedings of the Workshop on Parallel and Distributed Methods in verifiCation (PDMC'05), July 2005.

[5]

M. Beek, C. Ellis, J. Kleijn, and G. Rozenberg. Synchronizations in Team Automata for Groupware Systems. Computer Supported Cooperative Work---The Journal of Collaborative Computing, 12(1):21--69, 2003.

Digital Library

[6]

E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, January 2000.

Digital Library

[7]

L. de Alfaro and T. A. Henzinger. Interface automata. In Proceedings of the Ninth Annual Symposium on Foundations of Software Engineering, pages 109--120. ACM Press, 2001.

Digital Library

[8]

L. de Alfaro and T. A. Henzinger. Interface-based design. In Proceedings of the 2004 Marktoberdorf Summer School. Kluwer, 2004.

[9]

C. Ellis. Team Automata for Groupware Systems. In Proceedings of the International ACM SIGGROUP Conference on Supporting Group Work: The Integration Challenge (GROUP'97), pages 415--424. ACM Press, New York, 1997.

Digital Library

[10]

D. Giannakopoulou. Model Checking for Concurrent Software Architectures. PhD thesis, University of London, Imperial College of Science, Technology and Medicine, January 1999.

[11]

D. C. Luckham. Rapide: A language and toolset for simulation of distributed systems by partial orderings of events. In Proceedings of DIMACS Partial Order Methods Workshop IV, July 1996.

Digital Library

[12]

N. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, San Mateo, CA, 1996.

Digital Library

[13]

N. A. Lynch and M. R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of PODC, pages 137--151, April 1987.

Digital Library

[14]

N. A. Lynch and M. R. Tuttle. An introduction to input/output automata. CWI Quarterly, 2(3):219--246, September 1989.

[15]

J. Magee, N. Dulay, S. Eisenbach, and J. Kramer. Specifying distributed software architectures. In Proceedings of 5th European Software Engineering Conference (ESEC'95), September 1995.

Digital Library

[16]

J. Magee, J. Kramer, and D. Giannakopoulou. Behaviour analysis of software architectures. In Proceedings of the 1st Working IFIP Conference on Software Architecture (WICSA1), February 1999.

Digital Library

[17]

F. Plasil and S. Visnovsky. Behavior protocols for software components. IEEE Transactions on Software Engineering, 28(11):1056--1076, November 2002.

Digital Library

[18]

M. R. Tuttle. Hierarchical correctness proofs for distributed algorithms. Master's thesis, Massachusetts Institute of Technology, Laboratory for Computer Science, April 1987.

Cited By

Sun CYao QMa J(2017)Certia: Certifying Interface Automata for Cyber-Physical Systems2017 IEEE International Conference on Smart Computing (SMARTCOMP)10.1109/SMARTCOMP.2017.7946992(1-3)Online publication date: May-2017
https://doi.org/10.1109/SMARTCOMP.2017.7946992
Kamath S(2013)Linking Business and Application ArchitecturesAligning Enterprise, System, and Software Architectures10.4018/978-1-4666-2199-2.ch011(209-228)Online publication date: 2013
https://doi.org/10.4018/978-1-4666-2199-2.ch011
Beneš NČerná IŠtefaňák F(2012)Factorization for component-interaction automataProceedings of the 38th international conference on Current Trends in Theory and Practice of Computer Science10.1007/978-3-642-27660-6_45(554-565)Online publication date: 21-Jan-2012
https://dl.acm.org/doi/10.1007/978-3-642-27660-6_45
Show More Cited By

Index Terms

Component-interaction automata as a verification-oriented component-based system specification

Recommendations

Component-interaction automata as a verification-oriented component-based system specification

In the paper, we present a new approach to component interaction specification and verification process which combines the advantages of both architecture description languages (ADLs) at the beginning of the process, and a general formal verification-...
A compositional specification theory for component behaviours
ESOP'12: Proceedings of the 21st European conference on Programming Languages and Systems

We propose a compositional specification theory for reasoning about components that interact by synchronisation of input and output (I/O) actions, in which the specification of a component constrains the temporal ordering of interactions with the ...
A Method on Specification and Verification of Component Interaction in Real-Time Reactive Systems
ICACTE '08: Proceedings of the 2008 International Conference on Advanced Computer Theory and Engineering

We present Timed Component-Interaction Automata with Cost (TCIAC) to specify and verify component interaction behavior, timing cost and timing constraint information in component-based real-time reactive systems. TCIAC extends the description ability of ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

SAVCBS '05: Proceedings of the 2005 conference on Specification and verification of component-based systems

September 2005

95 pages

ISBN:1595933719

DOI:10.1145/1123058

Program Chair:
Gary T. Leavens
Iowa State

ACM SIGSOFT Software Engineering Notes Volume 31, Issue 2
March 2006
193 pages
ISSN:0163-5948
DOI:10.1145/1118537
Issue’s Table of Contents

Copyright © 2005 Authors.

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 September 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Acceptance Rates

SAVCBS '05 Paper Acceptance Rate 15 of 15 submissions, 100%;

Overall Acceptance Rate 37 of 46 submissions, 80%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

58
Total Citations
View Citations
571
Total Downloads

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

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Sun CYao QMa J(2017)Certia: Certifying Interface Automata for Cyber-Physical Systems2017 IEEE International Conference on Smart Computing (SMARTCOMP)10.1109/SMARTCOMP.2017.7946992(1-3)Online publication date: May-2017
https://doi.org/10.1109/SMARTCOMP.2017.7946992
Kamath S(2013)Linking Business and Application ArchitecturesAligning Enterprise, System, and Software Architectures10.4018/978-1-4666-2199-2.ch011(209-228)Online publication date: 2013
https://doi.org/10.4018/978-1-4666-2199-2.ch011
Beneš NČerná IŠtefaňák F(2012)Factorization for component-interaction automataProceedings of the 38th international conference on Current Trends in Theory and Practice of Computer Science10.1007/978-3-642-27660-6_45(554-565)Online publication date: 21-Jan-2012
https://dl.acm.org/doi/10.1007/978-3-642-27660-6_45
Kamath S(2011)Capabilities and FeaturesProceedings of the 2011 Ninth Working IEEE/IFIP Conference on Software Architecture10.1109/WICSA.2011.12(12-21)Online publication date: 20-Jun-2011
https://dl.acm.org/doi/10.1109/WICSA.2011.12
Besova GWehrheim HWagner A(2011)Reputation-based Reliability Prediction of Service CompositionsElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2011.11.008279:2(3-16)Online publication date: 1-Dec-2011
https://dl.acm.org/doi/10.1016/j.entcs.2011.11.008
Fernandes FPassama RRoyer JDeshpande KJalote PRajamani S(2009)Event strictness for components with complex bindingsProceedings of the 2nd India software engineering conference10.1145/1506216.1506225(47-56)Online publication date: 23-Feb-2009
https://dl.acm.org/doi/10.1145/1506216.1506225
Jing-zhou ZHong-min RXiao-Kun GLe-Qiu QSan-Yuan Z(2009)Research on Component Behavior Protocols Mismatch Detection and Limited AssemblyProceedings of the 2009 10th ACIS International Conference on Software Engineering, Artificial Intelligences, Networking and Parallel/Distributed Computing10.1109/SNPD.2009.83(192-199)Online publication date: 27-May-2009
https://dl.acm.org/doi/10.1109/SNPD.2009.83
Qian Z(2009)Testing Component-Based Web Applications Using Component AutomataProceedings of the 2009 WASE International Conference on Information Engineering - Volume 0110.1109/ICIE.2009.64(455-458)Online publication date: 10-Jul-2009
https://dl.acm.org/doi/10.1109/ICIE.2009.64
Beneš NBrim LČerná ISochor JVařeková PZimmerova B(2009)Partial Order Reduction for State/Event LTLProceedings of the 7th International Conference on Integrated Formal Methods10.1007/978-3-642-00255-7_21(307-321)Online publication date: 16-Feb-2009
https://dl.acm.org/doi/10.1007/978-3-642-00255-7_21
Hill JGokhale A(2008)Model-driven specification of component-based distributed real-time and embedded systems for verification of systemic QoS properties2008 IEEE International Symposium on Parallel and Distributed Processing10.1109/IPDPS.2008.4536573(1-8)Online publication date: Apr-2008
https://doi.org/10.1109/IPDPS.2008.4536573
Show More Cited By

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