Article

A specification language for coordinated objects

Authors:

Gabriel Ciobanu,

Dorel LucanuAuthors Info & Claims

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

Pages 3 - es

https://doi.org/10.1145/1123058.1123062

Published: 05 September 2005 Publication History

Abstract

The paper presents a specification language of autonomous objects supervised by a coordinating process. The coordination is defined by means of an interaction wrapper. The coordination semantics is described in the terms of bisimulation relations. The properties of the coordinated objects are expressed as temporal formulas, and verified by specific model-checking algorithms. We use the alternating bit protocol to exemplify our specification language and its semantics.This approach allows a clear separation of concerns: the same coordinating process can be used with different concurrent objects, and the same objects can be used with a different coordinator. Thus our specification language allows easy modifications and customization. The method is effective in assembling increasingly complex systems from components. Moreover, composing different coordinating processes can be done without changing the code of the coordinated objects. In this way, the difficult task of implementing the mechanism of coordination becomes substantially easier.

References

[1]

R. Allen and D. Garlan. A Formal Basis for Architectural Connection. ACM Transactions on Software Engineering and Methodology, vol.6, pp.213--249, 1997.

Digital Library

[2]

G. Ciobanu and D. Lucanu. Specification and verification of synchronizing concurrent objects. In J. Derrick E. Boiten and G. Smith (Eds.): Integrated Formal Methods 2004, Lecture Notes in Computer Science, vol.2999, pp.307--327, Springer, 2004.

[3]

G. Ciobanu and D. Lucanu. Communicating Concurrent Objects in HiddenCCS. Electronic Notes in Theoretical Computer Science, vol.117, pp.353--373, Elsevier, 2004.

Digital Library

[4]

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

Digital Library

[5]

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. F. Quesada Maude: Specification and Programming in Rewriting Logic Theoretical Computer Science, vol. 285, pp.187--243, 2002.

Digital Library

[6]

F. Durán and J. Meseguer. Structured Theories and Institutions. Theoretical Computer Science, vol.309, pp.357--380, 2003.

Digital Library

[7]

S. Frølund and G. Agha. A language framework for multi-object coordination. In Proc. ECOOP'93, Lecture Notes in Computer Science, vol. 707, pp.346--360, Springer, 1993.

Digital Library

[8]

J. Goguen, and G. Malcolm. A hidden agenda. Theoretical Computer Science vol.245, pp.55--101, 2000.

Digital Library

[9]

Gh. Grigoraş. and D. Lucanu. On Hidden Algebra Semantics of Object Oriented Languages. Sci. Ann. of the "A.I.Cuza" Univ. of laşi, 14(Computer Science), pp.51--68, 2004.

[10]

B. Jacobs. Coalgebraic Reasoning about Classes in Object-Oriented Languages. In Electronic Notes in Theoretical Computer Science, vol.11, pp.231--242, Elsevier, 1998.

[11]

D. Lucanu, and G. Ciobanu. Model Checking for Object Specifications in Hidden Algebra. In B. Steffen, G. Levi (Eds.) Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Computer Science vol.2937, Springer, pp.97--109, 2004.

[12]

J. Magee, J. Krammer, and D. Giannnakopoulou. Analysing the Behaviour of Distributed Software Architecture: a Case Study. In Proc. of the 5th IEEE Workshop on Future Trends of Distributed Computing Systems, Tunis, pp.240--245, 1997.

Digital Library

[13]

K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

Digital Library

[14]

R. Milner. Communicating and Mobile Systems: then π-calculus. Cambridge Uiversity Press, 1999.

Digital Library

[15]

J. Rutten. Universal Coalgebra: A Theory of Systems. Theoretical Computer Science vol.249, pp.3--80, 2000.

Digital Library

[16]

G. Salaün, M. Allemand, and C. Attiogbé. A Formalism Combining CCS and CASL. Research Report 00.14, IRIN, Univ. Nantes, 2001.

[17]

M. Shaw and D. Garlan. Formulations and Formalisms in Software Architecture. In J. van Leeuwen (Ed.): Computer Science Today: Recent Trends and Developments, Lecture Notes in Computer Science, vol.1000, Springer, 1995.

[18]

A. Verdejo, and N. Martí-Oliet. Implementing CCS in Maude 2. In 4th WRLA, Electronic Notes in Theoretical Computer Science, vol.71, pp.239--257, Elsevier, 2002.

Digital Library

Cited By

Król DZelmozer M(2008)A comparison of performance-evaluating strategies for data exchange in multi-agent systemProceedings of the 2nd KES International conference on Agent and multi-agent systems: technologies and applications10.5555/1787839.1787930(793-802)Online publication date: 26-Mar-2008
https://dl.acm.org/doi/10.5555/1787839.1787930
Król DZelmozer M(2008)A Comparison of Performance-Evaluating Strategies for Data Exchange in Multi-agent SystemAgent and Multi-Agent Systems: Technologies and Applications10.1007/978-3-540-78582-8_80(793-802)Online publication date: 2008
https://doi.org/10.1007/978-3-540-78582-8_80
Danes MLucanu DCiobanu G(2005)Specification of Coordinated Objects and Verification of Their Temporal PropertiesProceedings of the Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing10.1109/SYNASC.2005.67Online publication date: 25-Sep-2005
https://dl.acm.org/doi/10.1109/SYNASC.2005.67

Index Terms

Recommendations

A specification language for coordinated objects

The paper presents a specification language of autonomous objects supervised by a coordinating process. The coordination is defined by means of an interaction wrapper. The coordination semantics is described in the terms of bisimulation relations. The ...
Communicating Concurrent Objects in HiddenCCS

In this paper we add value-passing communication to hiddenCCS, a new formalism proposed in G. Ciobanu, and D. Lucanu. Specification and Verification of Synchronizing Concurrent Objects. In E. Boiten, J. Derrick, and G. Smith (Eds.) IFM 2004, Lecture ...
A Preliminary Comparative Study on the Expressive Power of Reo and Linda

Component-based Software Development is an emerging discipline in the field of Software Engineering. In this context, coordination languages may be used to specify the interactive behavior of software components, and most of the proposals presented in ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

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

3
Total Citations
View Citations
256
Total Downloads

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

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Król DZelmozer M(2008)A comparison of performance-evaluating strategies for data exchange in multi-agent systemProceedings of the 2nd KES International conference on Agent and multi-agent systems: technologies and applications10.5555/1787839.1787930(793-802)Online publication date: 26-Mar-2008
https://dl.acm.org/doi/10.5555/1787839.1787930
Król DZelmozer M(2008)A Comparison of Performance-Evaluating Strategies for Data Exchange in Multi-agent SystemAgent and Multi-Agent Systems: Technologies and Applications10.1007/978-3-540-78582-8_80(793-802)Online publication date: 2008
https://doi.org/10.1007/978-3-540-78582-8_80
Danes MLucanu DCiobanu G(2005)Specification of Coordinated Objects and Verification of Their Temporal PropertiesProceedings of the Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing10.1109/SYNASC.2005.67Online publication date: 25-Sep-2005
https://dl.acm.org/doi/10.1109/SYNASC.2005.67

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.

Media

Figures

Other

Tables

View Table of Contents