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.
ERCIM FMICS Home Page,
GMD FOKUS Home Page
Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST,
Axel Rennoch