Specification of Dynamic Systems
The people of this group mainly involved in this area are
G.Reggio (Contact person) and
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 hydro-electric plant
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,
dynamic-data types (cfr. the difference with dynamic data-types );
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 many-sorted
algebra (first-order 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.
The purpose of an ADS is to define, by an appropriate semantics,
abstract dynamic-data type's (shortly ad-dt),
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 dynamic-data types.
In the past we have also used the name algebraic transition systems
SMoLCS-Driven Concurrent Calculi).
Thus we can consider ADSs with
"loose" semantics: i.e., specifications which determine a class of
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 ad-dt's
describing systems satisfying those requirements.
First-order 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 first-order logic for ADS has been extended in various ways to cope with such
For what concerns dynamic properties,
Abstract Dynamic Data Types: a Temporal Logic Approach
Specification of Abstract Dynamic Data Types: A Temporal Logic Approach
present an integration of the
combinators of classical branching-time 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
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
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
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.
As in the classic (static) case, an ADS may determine different
ad-dt'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 ad-dt is called design specification,
since it may be used to define abstractly and formally the ad-dt
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 first-order provability
(and there exists a Birkhoff-like 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 non-relevant parts.
Methods and applications related to ADS
A specification method for dynamic system based on ADS,
called SMoLCS has been developed, whose main
broad-spectrum 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
(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 SMoLCS-Driven Concurrent Calculi
Corresponding informal specifications
Recently the method has been extended following what we call
the principle of the "two-rail" (see
Formally-Driven Friendly Specifications of Concurrent Systems:
A Two-Rail 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
non-specialist 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 tool-set
has been developed to support the development of ADSs,
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 user-interface for it (The SMoLCS Toolset).
ADS and the related specification method have been used
in A Dynamic
Specification of the RPC-Memory Problem
to specify some industrial case studies given by ENEL-CRA (the national producer of electric power)
(see Specification of a Hydroelectric Power Station:
Revised Tool-Checked Version
Specification of a High-Voltage Substation:
Revised Tool-Checked Version).
An initial version of the method, developed in the national project
(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
CEE-MAP (DDC-CRAI) for the formal definition of Ada
The Ada Challenge for New Formal
to specify the underlying concurrent model of Ada programs.
A SMoLCS Based Kit for Defining the Semantics of
High-Level Algebraic Petri Nets
shows how ADS can be used to extend and complement Petri nets.
Please send suggestions and comments to:
Gianna Reggio email@example.com
7 june, 1996