Specification of Dynamic Systems
The people of this group mainly involved in this area are
E.Astesiano ,
G.Reggio (Contact person) and
E.Coscia .
Here by dynamic systems we mean systems able to evolve along the time, thus
they include reactive, parallel, concurrent systems, for example particular instances are
a software\hardware parallel architecture, an embedded system and a hydroelectric plant
automatically controlled.
This group is mainly concerned with the following issues.
ADS: Algebraic Dynamic Specifications
Algebraic Dynamic Specifications, shortly ADS,
extend the algebraic specifications
of abstract data types to the specification of types of dynamic systems,
dynamicdata types (cfr. the difference with dynamic datatypes );
see Algebraic Dynamic Specifications: An Outline.
Models for dynamic systems
In the ADS approach a type of dynamic systems
is modelled by a labelled transition system (shortly lts),
which is a triple (STATE, LABEL,>),
where STATE and LABEL are two sets whose elements
are, respectively, the states and the labels of the system,
while >, a subset of STATE x LABEL x STATE, represents
the transition relation.
A single dynamic system D can be modelled by an initial state s0 belonging to STATE.
The elements in STATE that can be reached starting from
s0 are the intermediate interesting states in the life of D,
while the transition relation > describes the capabilities of D to pass
from one intermediate state to another one
and labels provide information both on
the conditions on the external world making effective this capability and on the
changes in the external world caused by it.
An lts can be represented algebraically by a
dynamic algebra A, i.e. a manysorted
algebra (firstorder structure) with a signature
having two sorts, say state and label
(whose elements correspond to the states
and the labels of the system), and
a predicate _  _ > _ : state x label x state
representing the transition relation.
Clearly, we can handle
algebraically also lts's modelling structured dynamic elements;
i.e. lts's where components of the states are in turn states of other lts's;
in these cases we have dynamic algebras with several sorts corresponding to states and labels,
together with the associated transition predicates.
Requirement specifications
The purpose of an ADS is to define, by an appropriate semantics,
classes of
abstract dynamicdata type's (shortly addt),
i.e. isomorphisms classes of dynamic algebras.
Following the usual algebraic style we give a signature and then, by means of axioms,
describe the relationships holding among operations and predicates of that signature,
obtaining an ADS,
to emphasize that we are abstractly specifying dynamicdata types.
In the past we have also used the name algebraic transition systems
(e.g. in
SMoLCSDriven Concurrent Calculi).
Thus we can consider ADSs with
"loose" semantics: i.e., specifications which determine a class of
nonisomorphic addt's;
which are called requirement specifications, since they may be used to formally
define the requirements on some dynamic system by determining the class of all the addt's
describing systems satisfying those requirements.
Firstorder logic allows to express only few requirements on dynamic systems
as properties of the static parts, limited
properties on the system structure and on the activity of the dynamic systems.
Much more interesting and relevant properties, as safety\liveness and absence of deadlocks, cannot be expressed.
Thus firstorder logic for ADS has been extended in various ways to cope with such
properties.
For what concerns dynamic properties,
Abstract Dynamic Data Types: a Temporal Logic Approach
and
Specification of Abstract Dynamic Data Types: A Temporal Logic Approach
present an integration of the
combinators of classical branchingtime temporal logic into ADS for expressing
the classical safety\liveness properties;
while Event Logic for Specifying Abstract Dynamic Data Types and
Specifying Reactive Systems by Abstract Events
propose a
new logic based on the concept of "abstract event" for expressing overall properties on the
activity of the dynamic systems
(e.g. a certain activity, not necessarily atomic [i.e. consisting of
one state\transition], will be eventually followed by the sequential composition of two other
nonatomic activities).
Recently, in
Deontic Concepts in the Algebraic Specification of Dynamic Systems:
The Permission Case
an extension based on concepts of the deontic logics has been studied
Instead, for the properties concerning the concurrent structure of dynamic systems
entity specifications have been proposed (see
Entities: an Institution for Dynamic Systems
and
A Metalanguage for the Formal Requirement Specification of Reactive Systems)
where it is possible to express properties
on the structure by a special predicate saying if (in a certain state) a dynamic
system is component of another one.
Design specifications
As in the classic (static) case, an ADS may determine different
addt's depending on the chosen semantics;
for example we can consider as semantics the
(isomorphism class of the) initial elements of the class of the models (initial approach) or the
isomorphism class of a particular model satisfying some observational
constraints (monomorphic specifications).
An ADS determining ONE addt is called design specification,
since it may be used to define abstractly and formally the addt
describing the complete design of a dynamic system.
Only conditional ADSs admit initial
models with interesting properties and particular observational models,
so design specifications must be conditional ADSs.
The inital model ISP of a conditional ADS SP is characterized by
for all t1, t2 ground terms of the same sort
ISP = t1 = t2 iff SP  t1 = t2;
for all predicates pr and all ground terms t1, ..., tn of appropriate sorts
ISP = pr(t1, ..., tn) iff SP  pr(t1, ..., tn);
where  denotes firstorder provability
(and there exists a Birkhofflike sound and complete deductive system for such axioms).
Moreover, it is formally defined when a
design (requirement) ADS SP1 correctly implements
a requirement ADS SP2:
the model (models) of SP1 are (is) contained
"essentially" in those of SP2 ,
where "essentially" means up to renaming, deletion, addition
of nonrelevant parts.
Methods and applications related to ADS
A specification method for dynamic system based on ADS,
called SMoLCS has been developed, whose main
features are:
broadspectrum of applications, i.e. it has not been
developed for a restricted class of applications,
but admits specialized variants;
a lot of emphasis is put on the apsects of modularity and of
structuring of complex specifications (of complex) systems;
it is intended for a "real" use in an industrial environment.
The method offers the following (conceptual) tools to support the use
of ADS for the development of real dynamic systems.
METAL, a friendly specification language for writing both design and requirement
ADSs
(METAL: a Metalanguage for SMoLCS).
Structuring of dynamic systems
A dynamic system is
structured, whenever has at least two cooperating components,
and simple otherwise.
Its components may be further disitinct into:
active (in turn dynamic systems) and passive (data types).
In turn the states and the labels of a dynamic system are
data types (the states of a structured systems are
obtained by composing those of its components).
These simple ideas suggest a natural way to
guide the modular structuring of a specification.
Clearly the definition of the activity of a structured system
must be done starting from those of its active components and from the
values of its passive ones.
The method offers also the possibility to further
decompose this phase, by starting defining
some basic partial cooperations among the components and after
composing them together, step after step, till to define the whole
activcity of the system
(see SMoLCSDriven Concurrent Calculi
Corresponding informal specifications
Recently the method has been extended following what we call
the principle of the "tworail" (see
FormallyDriven Friendly Specifications of Concurrent Systems:
A TwoRail Approach).
the specification must be given following two parallel rails,
an informal one and a formal one;
so that for each formal specification there exists a strictly corresponding
informal one (i.e. a natural language text written following particular schemas).
It is important to notice that this does not mean to give at the end an
informal paraphrase of previously produced formal specifications,
but instead to make explicitly the intermediate
stage between the informal description of the system provided by the client
and its formal specification.
That is intended to help the interaction between the
developer using formal specifications and the
nonspecialist ones (the clients, the final implementers,
the writer of manuals and so on);
moreover also the writing of formal specifications
is helped by this intermediate stage.
Experimental software tools
An experimental software toolset
has been developed to support the development of ADSs,
consisting of:
a checker of the static correctness for METAL;
a rapid prototyper which, given a design ADS
of a dynamic system and one of its states generates the execution three
starting from such state;
and a graphical userinterface for it (The SMoLCS Toolset).
Applications
ADS and the related specification method have been used
in A Dynamic
Specification of the RPCMemory Problem
and
to specify some industrial case studies given by ENELCRA (the national producer of electric power)
(see Specification of a Hydroelectric Power Station:
Revised ToolChecked Version
and
Specification of a HighVoltage Substation:
Revised ToolChecked Version).
An initial version of the method, developed in the national project
"Progetto Finalizzato
(Obiettivo CNET)" has been used to specify a communication net node
(Formal Specification of a Concurrent
Architecture in a Real Project)
and within the project
CEEMAP (DDCCRAI) for the formal definition of Ada
(see
The Ada Challenge for New Formal
Semantic Techniques)
to specify the underlying concurrent model of Ada programs.
A SMoLCS Based Kit for Defining the Semantics of
HighLevel Algebraic Petri Nets
shows how ADS can be used to extend and complement Petri nets.
Please send suggestions and comments to:

Last Updated:

Gianna Reggio reggio@disi.unige.it

7 june, 1996
