Article

Component-Based Algebraic Specification and Verification in CafeOBJ

Authors:

Razvan Diaconescu,

Kokichi Futatsugi,

Shusaku IidaAuthors Info & Claims

FM '99: Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume II

Pages 1644 - 1663

Published: 20 September 1999 Publication History

Abstract

We present a formal method for component-based system specification and verification which is based on the new algebraic specification language CafeOBJ, which is a modern successor of OBJ incorporating several new developments in algebraic specification theory and practice.

We first give an overview of the main features of CafeOBJ, including its logical foundations, and then we focus on the behavioural specification paradigm in CafeOBJ, surveying the object-oriented CafeOBJ specification and verification methodology based on behavioural abstraction.

The last part of this paper further focuses on a component-based behavioural specification and verification methodology which features high reusability of both specification code and verification proof scores. This methodology constitutes the basis for an industrial strength formal method around CafeOBJ.

References

[1]

Rod Burstall and Joseph Goguen. The semantics of Clear, a specification language. In Dines Bjorner, editor, Proceedings, 1979 Copenhagen Winter School on Abstract Software Specification, pages 292-332. Springer, 1980. Lecture Notes in Computer Science, Volume 86.

[2]

Manuel Clavel, Steve Eker, Patrick Lincoln, and Jose Meseguer. Principles of Maude. Electronic Notes in Theoretical Computer Science, 4, 1996. Proceedings, First International Workshop on Rewriting Logic and its Applications. Asilomar, California, September 1996.

[3]

Razvan Diaconescu. Category-based semantics for equational and constraint logic programming, 1994. DPhil thesis, University of Oxford.

[4]

Razvan Diaconescu. Behavioural coherence in object-oriented algebraic specification. Technical Report IS-RR-98-0017F, Japan Advanced Institute for Science and Technology, June 1998. Submitted to publication.

[5]

Razvan Diaconescu. Extra theory morphisms for institutions: logical semantics for multiparadigm languages. J. of Applied Categorical Structures, 6(4):427-453, 1998.

[6]

Razvan Diaconescu and Kokichi Futatsugi. Logical foundations of CafeOBJ. 1998. Submitted to publication.

[7]

Razvan Diaconescu and Kokichi Futatsugi. CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification, volume 6 of AMAST Series in Computing. World Scientific, 1998.

[8]

Razvan Diaconescu, Kokichi Futatsugi, and Shusaku Iida. Component-based algebraic specifications: - behavioural specification for component based software engineering -. In Behavioural Semantics of Object-oriented Business and System Specification. Kluwer, 1999.

[9]

Razvan Diaconescu, Joseph Goguen, and Petros Stefaneas. Logical support for modularisation. In Gerard Huet and Gordon Plotkin, editors, Logical Environments, pages 83-130. Cambridge, 1993. Proceedings of a Workshop held in Edinburgh, Scotland, May 1991.

[10]

Kokichi Futatsugi, Joseph Goguen, Jean-Pierre Jouannaud, and Jose Meseguer. Principles of OBJ2. In Proceedings of the 12th ACM Symposium on Principles of Programming Languages, pages 52-66. ACM, 1985.

[11]

Joseph Goguen and Rod Burstall. Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery, 39(1):95-146, January 1992.

[12]

Joseph Goguen and Razvan Diaconescu. An Oxford survey of order sorted algebra. Mathematical Structures in Computer Science, 4(4):363-392, 1994.

[13]

Joseph Goguen and Razvan Diaconescu. Towards an algebraic semantics for the object paradigm. In Harmut Ehrig and Fernando Orejas, editors, Recent Trends in Data Type Specification, volume 785 of Lecture Notes in Computer Science, pages 1-34. Springer, 1994.

[14]

Joseph Goguen and Grant Malcolm. A hidden agenda. Technical Report CS97-538, University of California at San Diego, 1997.

[15]

Joseph Goguen and JosÉ Meseguer. Eqlog: Equality, types, and generic modules for logic programming. In Douglas DeGroot and Gary Lindstrom, editors, Logic Programming: Functions, Relations and Equations, pages 295-363. Prentice-Hall, 1986.

[16]

Joseph Goguen and JosÉ Meseguer. Unifying functional, object-oriented and relational programming, with logical semantics. In Bruce Shriver and PeterWegner, editors, Research Directions in Object-Oriented Programming, pages 417-477. MIT, 1987.

[17]

Joseph Goguen and JosÉ Meseguer. Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science, 105(2):217-273, 1992.

[18]

Joseph Goguen, Timothy Winkler, JosÉ Meseguer, Kokichi Futatsugi, and Jean-Pierre Jouannaud. Introducing OBJ. In Joseph Goguen, editor, Algebraic Specification with OBJ: An Introduction with Case Studies. Cambridge. To appear.

[19]

Rolf Hennicker and Michel Bidoit. Observational logic. In A. M. Haeberer, editor, Algebraic Methodology and Software Technology, number 1584 in LNCS, pages 263-277. Springer, 1999. Proc. AMAST'99.

[20]

JosÉ Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96(1):73-155, 1992.

[21]

JosÉ Meseguer. Membership algebra as a logical framework for equational specification. In F. Parisi-Pressice, editor, Proc. WADT'97, number 1376 in Lecture Notes in Computer Science, pages 18-61. Springer, 1998.

Cited By

Barlas KBerki EStefaneas PKoletsos G(2017)Towards formal open standardsInnovations in Systems and Software Engineering10.1007/s11334-016-0283-913:1(51-66)Online publication date: 1-Mar-2017
https://dl.acm.org/doi/10.1007/s11334-016-0283-9
Gonçalves RBatory DSobral J(2016)ReFlOSoftware and Systems Modeling (SoSyM)10.1007/s10270-014-0403-715:2(377-395)Online publication date: 1-May-2016
https://dl.acm.org/doi/10.1007/s10270-014-0403-7
Barlas KBerki EAdomnita INalam TNejad GVeijalainen JSokratis KMichael HTheodoros ADimosthenis AElias CTheodora VMara N(2014)Formal Specification of Open Standards and the Case of RSS v2.0Proceedings of the 18th Panhellenic Conference on Informatics10.1145/2645791.2645809(1-6)Online publication date: 2-Oct-2014
https://dl.acm.org/doi/10.1145/2645791.2645809
Show More Cited By

Component-Based Algebraic Specification and Verification in CafeOBJ
1. Theory of computation
  1. Formal languages and automata theory
    1. Formalisms

Recommendations

From ASN.1 into CafeOBJ: Some First Steps
SEEFM '09: Proceedings of the 2009 Fourth South-East European Workshop on Formal Methods

Abstract Syntax Notation One (ASN.1) is a very popular specification language with many applications in networking. We work towards the correct translation from ASN.1, into the powerful algebraic specification language CafeOBJ. Our aim is to create a ...
Specification, Refinement and Verification of Concurrent Systems—An Integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of ...
Formal Methods in CafeOBJ
FLOPS '02: Proceedings of the 6th International Symposium on Functional and Logic Programming

Formal methods are still expected to improve the practice of software engineering. The areas in which formal methods will play important roles include at least: (1) distributed component software, (2) network/system security, (3) embedded systems. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

FM '99: Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume II

September 1999

923 pages

ISBN:3540665889

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 20 September 1999

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Barlas KBerki EStefaneas PKoletsos G(2017)Towards formal open standardsInnovations in Systems and Software Engineering10.1007/s11334-016-0283-913:1(51-66)Online publication date: 1-Mar-2017
https://dl.acm.org/doi/10.1007/s11334-016-0283-9
Gonçalves RBatory DSobral J(2016)ReFlOSoftware and Systems Modeling (SoSyM)10.1007/s10270-014-0403-715:2(377-395)Online publication date: 1-May-2016
https://dl.acm.org/doi/10.1007/s10270-014-0403-7
Barlas KBerki EAdomnita INalam TNejad GVeijalainen JSokratis KMichael HTheodoros ADimosthenis AElias CTheodora VMara N(2014)Formal Specification of Open Standards and the Case of RSS v2.0Proceedings of the 18th Panhellenic Conference on Informatics10.1145/2645791.2645809(1-6)Online publication date: 2-Oct-2014
https://dl.acm.org/doi/10.1145/2645791.2645809
Futatsugi K(2010)Fostering proof scores in CafeOBJProceedings of the 12th international conference on Formal engineering methods and software engineering10.5555/1939864.1939866(1-20)Online publication date: 17-Nov-2010
https://dl.acm.org/doi/10.5555/1939864.1939866
Ghezzi CMocci AMonga MPenta MLanza M(2007)Efficient recovery of algebraic specifications for stateful componentsNinth international workshop on Principles of software evolution: in conjunction with the 6th ESEC/FSE joint meeting10.1145/1294948.1294972(98-105)Online publication date: 3-Sep-2007
https://dl.acm.org/doi/10.1145/1294948.1294972
Diaconescu R(2005)Behavioural specification for hierarchical object compositionTheoretical Computer Science10.1016/j.tcs.2005.06.015343:3(305-331)Online publication date: 17-Oct-2005
https://dl.acm.org/doi/10.1016/j.tcs.2005.06.015
Diaconescu RFutatsugi K(2002)Logical foundations of CafeOBJTheoretical Computer Science10.1016/S0304-3975(01)00361-9285:2(289-318)Online publication date: 28-Aug-2002
https://dl.acm.org/doi/10.1016/S0304-3975%2801%2900361-9
Clavel MDurán FEker SLincoln PMartí-Oliet NMeseguer JQuesada J(2002)MaudeTheoretical Computer Science10.1016/S0304-3975(01)00359-0285:2(187-243)Online publication date: 28-Aug-2002
https://dl.acm.org/doi/10.1016/S0304-3975%2801%2900359-0
Martí-Oliet NMeseguer J(2002)Rewriting logicTheoretical Computer Science10.1016/S0304-3975(01)00357-7285:2(121-154)Online publication date: 28-Aug-2002
https://dl.acm.org/doi/10.1016/S0304-3975%2801%2900357-7

View Options

View options

Media

Figures

Other

Tables

View Table of Contents