Article

Specification and verification of inter-component constraints in CTL

Authors:

Nguyen Truong Thang,

Takuya KatayamaAuthors Info & Claims

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

Pages 8 - es

https://doi.org/10.1145/1123058.1123067

Published: 05 September 2005 Publication History

Abstract

The most challenging issue of component-based software is about component composition. Current component specification, in addition to the syntactic level, is very limited in dealing with semantic constraints. Even so, only static aspects of components are specified. This paper gives a formal approach to make component specification more comprehensive by including component semantic. Fundamentally, the component semantic is expressed via the powerful temporal logic CTL. There are two semantic aspects in the paper, component dynamic behavior and consistency - namely a component does not violate some property in another when composed. Based on the proposed semantic, components can be efficiently cross-checked for their consistency by an incremental verification method - OIMC, even for many future component extensions.

References

[1]

D. Batory, C. Johnson, B. MacDonald, and D. V. Heeder. Achieving extensibility through product-lines and domain-specific languages: A case study. In Proc. International Conference on Software Reuse, July 2000.]]

Digital Library

[2]

R. Cavada, A. Cimatti, G. Keighren, et al. NuSMV 2.2 Tutorial. CMU and ITC-irst, [email protected], 2004.]]

[3]

A. Chakrabarti, L. de Alfaro, T. A. Henzinger, M. Jurdzinski, and F. Y. C. Mang. Interface compatibility checking for software modules. In Proceedings of the Computer-Aided Verification - CAV. LNCS Springer-Verlag, 2002.]]

Digital Library

[4]

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

Digital Library

[5]

L. de Alfaro and T. A. Henzinger. Interface automata. In Proceedings of the Symposium on Foundations of Software Engineering. ACM Press, 2001.]]

Digital Library

[6]

K. Fisler and S. Krishnamurthi. Modular verification of collaboration-based software designs. In Proc. Symposium on the Foundations of Software Engineering, September 2001.]]

Digital Library

[7]

D. Giannakopoulou, C. S. Pasareanu, and H. Barringer. Assumption generation for software component verification. In Proceedings of the International Conference on Automated Software Engineering, 2002.]]

Digital Library

[8]

O. Grumberg and D. E. Long. Model checking and modular verification. In International Conference on Concurrency Theory, volume 527 of Lecture Notes of Computer Science. Springer-Verlag, 1991.]]

Digital Library

[9]

J. Han. An approach to software component specification. In Proceedings of International Workshop on Component Based Software Engineering, 1999.]]

[10]

O. Kupferman and M. Y. Vardi. Modular model checking. In Compositionality: The Significant Difference, volume 1536 of Lecture Notes in Computer Science. Springer-Verlag, 1998.]]

Digital Library

[11]

K. Laster and O. Grumberg. Modular model checking of software. In Conference on Tools and Algorithms for the Constructions and Analysis of Systems, 1998.]]

Digital Library

[12]

B. Meyer. Object-oriented Software Construction. Prentice Hall, 1997.]]

Digital Library

[13]

T. T. Nguyen and T. Katayama. Handling consistency of software evolution in an efficient way. In Proc. IWPSE, pages 121--130, 2004.]]

Digital Library

[14]

C. S. Pasareanu, M. B. Dwyer, and M. Huth. Assume-guarantee model checking of software: A comparative case study. In Theoretical and Practical Aspects of SPIN Model Checking, volume 1680 of Lecture Notes of Computer Science. Springer-Verlag, 1999.]]

Digital Library

[15]

P. Tarr and H. Ossher. Hyper/J(TM) User and Installation Manual. IBM Research, IBM Corp., 2000.]]

[16]

J. Warmer and A. Kleppe. The Objects Constraint Language: Precise Modeling with UML. Addison-Wesley, 1999.]]

Digital Library

Cited By

Cordy MSchobbens PHeymans PLegay A(2012)Towards an incremental automata-based approach for software product-line model checkingProceedings of the 16th International Software Product Line Conference - Volume 210.1145/2364412.2364425(74-81)Online publication date: 2-Sep-2012
https://dl.acm.org/doi/10.1145/2364412.2364425
PHAM NAOKI TKATAYAMA T(2009)Modular Conformance Testing and Assume-Guarantee Verification for Evolving Component-Based SoftwareIEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences10.1587/transfun.E92.A.2772E92-A:11(2772-2780)Online publication date: 2009
https://doi.org/10.1587/transfun.E92.A.2772
Altahat ZElrad T(2009)Detection and Verification of Semantic Interaction In AOSDProceedings of the 2009 Sixth International Conference on Information Technology: New Generations10.1109/ITNG.2009.43(807-812)Online publication date: 27-Apr-2009
https://dl.acm.org/doi/10.1109/ITNG.2009.43
Show More Cited By

Index Terms

Specification and verification of inter-component constraints in CTL

Recommendations

Specification and verification of inter-component constraints in CTL

The most challenging issue of component-based software is about component composition. Current component specification, in addition to the syntactic level, is very limited in dealing with semantic constraints. Even so, only static aspects of components ...
Compositional Verification Using a Formal Component and Interface Specification
ICCAD '22: Proceedings of the 41st IEEE/ACM International Conference on Computer-Aided Design

Property-based specification s uch a s SystemVerilog Assertions (SVA) uses mathematical logic to specify the temporal behavior of RTL designs which can then be formally verified using model checking algorithms. These properties are specified for a ...
Using CTL formulae as component abstraction in a design and verification flow
ACSD '07: Proceedings of the Seventh International Conference on Application of Concurrency to System Design

In the context of component-based design, the verification of global properties (involving several components) is difficult to achieve, due to combinatorial explosion problem, while the verification of each component is easier to perform. Following the ...

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

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

6
Total Citations
View Citations
256
Total Downloads

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

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Cordy MSchobbens PHeymans PLegay A(2012)Towards an incremental automata-based approach for software product-line model checkingProceedings of the 16th International Software Product Line Conference - Volume 210.1145/2364412.2364425(74-81)Online publication date: 2-Sep-2012
https://dl.acm.org/doi/10.1145/2364412.2364425
PHAM NAOKI TKATAYAMA T(2009)Modular Conformance Testing and Assume-Guarantee Verification for Evolving Component-Based SoftwareIEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences10.1587/transfun.E92.A.2772E92-A:11(2772-2780)Online publication date: 2009
https://doi.org/10.1587/transfun.E92.A.2772
Altahat ZElrad T(2009)Detection and Verification of Semantic Interaction In AOSDProceedings of the 2009 Sixth International Conference on Information Technology: New Generations10.1109/ITNG.2009.43(807-812)Online publication date: 27-Apr-2009
https://dl.acm.org/doi/10.1109/ITNG.2009.43
Hung PKatayama T(2008)Modular Conformance Testing and Assume-Guarantee Verification for Evolving Component-Based SoftwareProceedings of the 2008 15th Asia-Pacific Software Engineering Conference10.1109/APSEC.2008.51(479-486)Online publication date: 3-Dec-2008
https://dl.acm.org/doi/10.1109/APSEC.2008.51
Li TYe JTan Q(2019)Towards functional verifying a family of systemC TLMsFrontiers of Computer Science10.1007/s11704-018-8254-yOnline publication date: 7-Mar-2019
https://doi.org/10.1007/s11704-018-8254-y
Bowles JBordbar B(2007)A Formal Model for Integrating Multiple ViewsProceedings of the Seventh International Conference on Application of Concurrency to System Design10.1109/ACSD.2007.39(71-79)Online publication date: 10-Jul-2007
https://dl.acm.org/doi/10.1109/ACSD.2007.39

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