Specification and verification of inter-component constraints in CTL

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Specification and verification of inter-component constraints in CTL

Full text

Pdf (190 KB)

Source

ACM SIGSOFT Software Engineering Notes archive
Volume 31 , Issue 2 (March 2006) table of contents

SESSION: Specification and Verification of Component-Based Systems Workshop (SAVCBS 2005) table of contents

Article No. 8

Year of Publication: 2006

ISSN:0163-5948

Also published in ...

Authors

Nguyen Truong Thang	Japan Advanced Institute of Science and Technology
Takuya Katayama	Japan Advanced Institute of Science and Technology

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 29, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	10.1145/1108768.1123067

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

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Don S. Batory , Clay Johnson , Bob MacDonald , Dale von Heeder, Achieving Extensibility Through Product-Lines and Domain-Specific Languages: A Case Study, Proceedings of the 6th International Conerence on Software Reuse: Advances in Software Reusability, p.117-136, June 27-29, 2000
	2	R. Cavada, A. Cimatti, G. Keighren, et al. NuSMV 2.2 Tutorial. CMU and ITC-irst, nusmv@irst.itc.it, 2004.
	3	Arindam Chakrabarti , Luca de Alfaro , Thomas A. Henzinger , Marcin Jurdzinski , Freddy Y. C. Mang, Interface Compatibility Checking for Software Modules, Proceedings of the 14th International Conference on Computer Aided Verification, p.428-441, July 27-31, 2002
	4	Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
	5	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
	6	Kathi Fisler , Shriram Krishnamurthi, Modular verification of collaboration-based software designs, 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
	7	Dimitra Giannakopoulou , Corina S. Psreanu , Howard Barringer, Assumption Generation for Software Component Verification, Proceedings of the 17th IEEE international conference on Automated software engineering, p.3, September 23-27, 2002
	8	Orna Grumberg , David E. Long, Model Checking and Modular Verification, Proceedings of the 2nd International Conference on Concurrency Theory, p.250-265, August 26-29, 1991
	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.
	11	Karen Laster , Orna Grumberg, Modular Model Checking of Software, Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.20-35, March 28-April 04, 1998
	12	Bertrand Meyer, Object-Oriented Software Construction, Prentice-Hall, Inc., Upper Saddle River, NJ, 1988
	13	Nguyen Truong Thang , Takuya Katayama, Handling Consistency of Software Evolution in an Efficient Way, Proceedings of the Principles of Software Evolution, 7th International Workshop on (IWPSE'04), p.121-130, September 06-07, 2004 [doi>10.1109/IWPSE.2004.13]
	14	Corina S. Pasareanu , Matthew B. Dwyer , Michael Huth, Assume-Guarantee Model Checking of Software: A Comparative Case Study, Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, p.168-183, September 21-24, 1999
	15	P. Tarr and H. Ossher. Hyper/J(TM) User and Installation Manual. IBM Research, IBM Corp., 2000.
	16	Jos Warmer , Anneke Kleppe, The object constraint language: precise modeling with UML, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1998