5th International Workshop on

Formal Methods for Industrial Critical Systems

Berlin, April 3-4, 2000

Cooperative Information Systems Modelling and Validation Using the Co-nets Approach: The Chessmen Making Shop Case Study

The Co-nets approach that we are developing is an object oriented speci cation model based on a sound and complete integration of object oriented (OO) concepts and constructions into a variant of algebraic Petri nets named Ecatnets . The Co-nets approach is interpreted in rewriting logic and is particularly suited for specifying and validating advanced information systems as autonomous, distributed, but yet cooperative components. This suitability is especially re ected by the following main Co-nets features. First, the approach is based on a perception of classes rather as modules with hidden (structural and behavioural) features enhancing autonomy and external features which may be exchanged with the environment and other classes. Second, the approach allows an incremental constructions of complex components, as a hierarchy of modules, through different forms of inheritance, object composition and aggregations; where each component behaves with respect to an appropriate intra-component evolution pattern supporting intra- as well as inter-object concurrency. Third, for interacting components, an appropriate inter-component interaction pattern is proposed promoting concurrency and keeping encapsulated all local features of communicating components. Fourth, due to their interpretation in rewriting logic, Co-nets modules can be rapid-prototyped using concurrent rewriting techniques.

Besides a didactic presentation of this approach, the objective of this paper is to enhance its practicability by handling a complex case study dealing with a Chessmen Making Shop(CMS) as a specific variant of a complex production system. In this system more than six autonomous components cooperate through explicit interfaces for achieving final (chessmess) products. Moreover, from a methodological point of view the paper shows how to specify and validate the corresponding Co-nets modules from their informal OO description, using well-known diagram notations, is a very straightforward way.

Note: The content of the following files is part of GMD Report No. 91 and subject to its copyright.


Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST, Axel Rennoch