Paper Info
Title
ÉTOILE-specifications: An Object-oriented Algebraic Formalism with Refinement
Abstract
In this paper, we investigate the formal specification of reactive systems described in an object-oriented style. We define a formalism, called ÉTOILE1-specifications, to deal with concurrent (active) object systems, and propose to extend algebraic approaches to dynamic and concurrent aspects by considering implicit states and implicit transitions, respectively. ÉTOILE-specifications emphasize systems composed of object types. Consequently, the ÉTOILE-formalism is split into two sub-formalisms. The first one enables us to specify the behaviour of object types. Then, it is extended from object types to systems by adding new requirements, mainly to describe the underlying architectural aspects of the system under specification (i.e. relationships between objects). The complexity of real systems results in the definition of formal means to manage their size. To deal with this issue, we propose a refinement of object type specifications by systems in the framework of ÉTOILE-specifications, which enables one to build his(her) specification in an incremental way.
Year
DOI
Venue
2004
10.1093/logcom/14.2.145
J. Log. Comput.
Keywords
DocType
Volume
Object-oriented Algebraic Formalism,object system,implicit transition,formal specification,implicit state,object type specification,algebraic approach,concurrent aspect,formal mean,real systems result,object type
Journal
14
Issue
ISSN
Citations 
2
0955-792X
2
PageRank 
References 
Authors
0.36
0
1
Name
Order
Citations
PageRank
Marc Aiguier19814.95