ETOILE-specifications: An Object-oriented Algebraic Formalism with Refinement

摘要

In this paper, we investigate the formal specification of reactive systems described in an object-oriented style. We define a formalism, called ETOILE-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.ETOILE-specifications emphasize systems composed of object types. Consequently, the ETOILE-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 ETOILE-specifications, which enables one to build his(her) specification in an incremental way.