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 hydro-electric 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, 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.

Requirement specifications
The purpose of an ADS is to define, by an appropriate semantics, classes of 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 (e.g. in SMoLCS-Driven Concurrent Calculi).
Thus we can consider ADSs with "loose" semantics: i.e., specifications which determine a class of non-isomorphic ad-dt'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 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 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 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 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 non-atomic 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 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 features are: 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 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 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, 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 user-interface for it (The SMoLCS Toolset).

Applications
ADS and the related specification method have been used in A Dynamic Specification of the RPC-Memory Problem and 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 and Specification of a High-Voltage Substation: Revised Tool-Checked 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 CEE-MAP (DDC-CRAI) 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 High-Level 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