Discrete Systems Modelling
Università di Pisa
I. Sequential Systems
II. Distributed Systems
III. Validation and Verification of Systems
Algorithm. A procedure, also the finite text describing it, that can be mechanized, at least
in principle. Examples are electronic booking procedures, or the operating system of a computer, or protocols which govern the interaction of multiple computer programs in the internet. An important special group of algorithms are those procedures that compute
functions, i.e. procedures which, started with any given argument, eventually terminate and yield the value of the function for that argument as output. Examples are the well-
known methods for computing the four elementary arithmetical functions, or more
generally computer programs which compute numerical functions.
Computer Program. A finite text, satisfying the syntactical conditions of the (so-called
programming) language in which it is formulated, which can be executed on a computer.
A computer program refers to the specific data structures of the programming language to which it belongs. A particularly important class of computer programs are the so-called reactive programs whose role is to continuously execute the actions associated to them, as distinguished from so-called sequential transformational programs that compute an input-output relation.
Finite State Machine. A machine to execute a set of instructions which determine, for
each of a finite number of so-called internal (or control) states, and for each of a finite number of possible finite inputs, the next internal state and the (equally finite) output. A more precise definition of these transformational sequential FSMs is given in the text
Logic. The branch of mathematics that develops rigorous systems of reasoning, which are also called logics, and studies their mathematical properties. Usually a system of logic is defined syntactically by a formal language, establishing the set of legal expressions (also called formulae) of this logic, together with a system of rules allowing to deduce from given formulae (the so-called axioms) their logical consequences. Semantically, a logic is defined by characterizing the intended interpretations of its formulae, yielding classes of models where the axioms, and the consequences deduced from them by the rules, are
―true‖. For first-order logic, such models are so-called structures, consisting of finitely
many domains with functions and relations defined over them.
Abstract State Machine. A generalization of Finite State Machines to arbitrary
structures, instead of finitely many control states, and to distributed runs, instead of sequential computations that transform input to output. The two major subclasses of Abstract State Machines are the sequential ASMs and the distributed (multi-agent) ASMs. Such machines encompass any known form of virtual machines and real computers, in a way that can be made rigorous (see the explanation of the ASM Thesis below, where also a precise definition of ASMs is given).
Discrete Systems are dynamic systems that evolve in discrete steps, due to the abrupt occurrence of internal or external events. The system evolution is typically modelled as resulting from firing state transforming rules, which are triggered when certain (internal and/or external) conditions become true. Such systems encompass sequential (also called transformational) algorithms and their implementations as computer programs, but also systems of distributed (asynchronous concurrent) processes, like telecommunication systems, operating on physically or logically separate architectures and typically triggered by external (discrete or continuous physical) events. Methods for modelling sequential or distributed systems are intimately related to methods for validating and verifying these systems against their models.
I. Sequential Systems.
Sequential discrete systems are dynamic systems with a law that determines how they evolve in discrete steps, producing for every initial state a sequence of states resulting from firing state transforming rules, which are triggered when certain conditions become true. Such sequences S, S, … are determined by the evolution law, usually rules which 01
model the dynamics of the system, and by the initial state S. This sequence constitutes 0
what is also called a computation of the algorithmic or transformational process defined by the rules. There is a great variety of such algorithmic systems, including manufacturing, transportation, business, administrative, and information handling processes as well as computers, where the rules are described by computer programs. Numerous general purpose or specialized languages exist which are used to model and implement such systems.
A widespread criterion to classify different modelling languages is whether the system definitions they allow to formulate are state-transformation-based (also called operational) or purely logico-functional (also called declarative). This dichotomy came into use around 1970 with the denotational and algebraic approaches to system descriptions, which were biased to modelling systems by sets of algebraic equations or axioms. A representative example is the Vienna Development Method (VDM) for constructing models of software systems in early design stages. Also declarative set-theoretic
modelling, e.g. in Z, belongs here, as well as numerous forms of system modelling by axioms of specific logics, like temporal logics, logics of action, logics of belief, etc. The stateless form of modeling underlies also functional programming (e.g. in pure LISP or ML) and logic programming (e.g. in PROLOG), as opposed to imperative or object-oriented programming (e.g. in FORTRAN, C, JAVA).
The fundamental problem, to whose solution the distinction between declarative and operational system models has been set out to contribute, is the necessity to provide the system designer with abstraction methods that enable one to cope with the ever increasing complexity of software and hardware systems. The idea was to tackle this problem by developing system definitions at levels of abstraction higher than the level of the machines where these systems are implemented, so that the resulting models can be analysed before the detailed design, coding, and testing are started. Unfortunately, formalizations by logical axioms inherently lead to global descriptions; in fact in addition to formalizing dynamic changes of mostly local system elements, the overwhelming part of the sets of axioms usually is concerned with stating that, under the specified conditions, all the other system parameters do not change. This phenomenon is known as the frame
problem and yields high-level system models that are considerably larger than the final
system. E.g. in the SCR method, which uses the temporal logic x/x’ notation within table
based modelling of systems, the frame problem yields numerous so-called NC (No Change) clauses. Furthermore, it is usually difficult to reliably relate the (stateless) logical descriptions, by a sequence of stepwise refinements, to imperative code, which is executed and tested on state-transforming machines. See for instance the difficulties encountered in attempts to extend logical characterizations of passive databases by descriptions of the inherently reactive behaviour of active databases, in particular when it comes to model multiple database transactions that may happen during the execution of an active rule. Thus logico-functional modelling methods contribute to the gap, experienced in the practice of large-scale system design, between high-level system models and their executable counterpart on virtual or physical machines.
The same idea, namely to abstract from machine details, which are only relevant for the implementation, to obtain better understandable and verifiable high-level system models, underlies the development, since the end of the 60’ies, of numerous notions and specimens of abstract machines, also called virtual machines. Famous examples, developed for the implementation of programming languages, are the class concept of Simula67, Wirth’s P-Machine (for executing PASCAL programs), Warren’s Abstract
Machine (for efficient implementations of PROLOG programs), Peyton Jones’ spineless tagless G-Machine (for efficient implementations of functional programs), the Java Virtual Machine (for platform independent execution of JAVA programs). Such machines split the implementation of programs into two steps, a compilation into intermediate byte code, and the interpretation of byte code by an abstract machine or its further compilation into runnable code. Virtual machines appear also in other areas, see for example the numerous forms of database machines, instruction set architectures, etc. This development paralleled for over twenty years the rich deployment of logico-algebraic specification methods, without having been connected to it, so that no general notion of abstract machine came out which could have been used as uniform and practical
basis for high-level system modelling coming together with methods for refining the
abstract models to executable and thereby testable ones.
Gurevich’s notion of Abstract State Machine (ASM) resolves the impractical dichotomy
between declarative and operational modelling methods and yields a simple universal
concept of virtual machines. The intended abstractions are realized by
a) the appropriate choice of the relevant, a priori arbitrary, data structures, which can
be tailored to the system under investigation to make up the needed notion of states,
b) providing corresponding abstract machine instructions which describe the intended
evolution (transformation) of states, at the desired level of detailing.
A . Sequential Abstract State Machines.
Sequential Abstract State Machines capture the notion of sequential algorithm, in the
sense that for every sequential algorithm, there exists an equivalent sequential ASM (i.e.
with the same set of states, the same set of initial states, and the same state transformation
law). This Sequential ASM Thesis relies upon the following three postulates for sequential
algorithms from which it can be proved. The sequential time postulate expresses that every
sequential algorithm is associated with a set of states, a subset of initial states and a state
transformation law (which is a function from states to states). The abstract-state postulate
requires that the states of a sequential algorithm are first-order structures, with fixed
domain and signature, and closed under isomorphisms (respecting the initial states and
the state transformation law). The bounded exploration postulate states that for every
sequential algorithm, the transformation law depends only upon a finite set of terms over
the signature of the algorithm, in the sense that there exists a finite set of terms such that
for arbitrary states X and Y which assign the same values to each of these terms, the
transformation law triggers the same state changes for X and Y.
A sequential ASM is defined as a set of transition rules of form
If Condition then Updates
which transform first-order structures (the states of the machine), where the guard
Condition, which has to be satisfied for a rule to be applicable, is a variable free first-order
formula, and Updates is a finite set of function updates (containing only variable free terms) of form
f (t,…,t) := t . 1nThe execution of these rules is understood as updating, in the given state and in the
indicated way, the value of the function f at the indicated parameters, leaving everything
else unchanged. This proviso avoids the frame problem of declarative approaches. In
every state, all the rules which are applicable are simultaneously applied (if the updates
are consistent) to produce the next state. If desired or useful, declarative features can be
built into an ASM by integrity constraints and by assumptions on the state, on the
environment, and on the applicability of rules.
Computations of sequential ASMs formalize the so-called transformational character of
sequential systems, namely that each step of the system consists of an ordered sequence
of two substeps of the environment and of the transformational program of the system.
First the environment prepares the input on which the program is expected to be run, then
the program fires its rules on the given input without further intervention from the
environment. An example can be found in current implementations of active databases,
where the occurrence of external events and the processing of active rules alternate. Part
of the second substep may be that the program produces some output, which may be used
by the environment for preparing the next input. This is often considered a third substep
in this sequence of interactions between the environment and the transformational
program, which together constitute the sequential system.
In a sequential ASM M, this separation of the action of the environment from that of the
transformational program is reflected in the following classification of functions, which
make up the state of the system. A function f is called static, or rigid, if its values do not
change in any of the states of M; f is called dynamic, or flexible, if its values may change
from one to the next state of M. Dynamic functions are further classified into input
functions, controlled functions, output functions, and shared functions. Input functions for
M are those functions that M can only read, which means that these functions are
determined entirely by the environment of M. These functions are often also called
monitored functions, because they are used to reflect the occurrence of events which
trigger rules. Controlled functions of M are those which are updated by some of the rules of M and are never changed by the environment. This means that M and only M can
update these functions. Output functions for M are functions which M can only update but not read, whereas the environment can read them (without updating them). Shared
functions are functions which can be read and updated by both M and the environment,
which means that their consistency has to be guaranteed by special protocols.
This function classification includes a fundamental distinction for selection functions,
which are an abstract form of scheduling algorithms. In fact static selection functions,
like Hilbert’s ε-operator, whose values depend only upon the value of the set they choose
from, are distinguished from dynamic selection functions, whose choice may depend
upon the entire computation state. There is a standard notation for not furthermore
specified selection functions, which is often used for modeling the phenomenon of non-
determinism in discrete systems, namely for applying a rule for an element which
satisfies a given condition:
choose x satisfying cond (x) in rule (x).
The above-defined abstract machines provide a practical (and by the Sequential ASM
Thesis most general) framework for high-level modeling of complex discrete systems and
for refining high-level models to executable system models. Important examples are
given below. There are various ways to refine high-level ASM models to executable
models, using various tools for executing ASMs (e.g. ASMGofer, ASM Workbench,
XASM), coming also with implementations of natural ASM definitions for standard
programming constructs, like sequentialization, iteration, and submachine calls.
B. Specialized Modelling Languages for Sequential Systems .
Most of the numerous specification and programming languages are tailored to the
particular modelling needs of the given domain of application, or of the given framework
for modelling (read: defining and implementing) the class of systems of interest.
The best known group of examples is constituted by programming languages belonging
to the major (non-concurrent) programming paradigms, namely functional, logical,
imperative, and object-oriented programming. All these modelling approaches can be
viewed naturally, and in a rigorous way, as producing instantiations of ASMs at the
corresponding level of abstraction. This has been proved explicitly for numerous
programming languages, e.g. PROLOG, C, JAVA, by defining their semantics and their
implementations on virtual machines as ASMs. In this way ASMs have been used also
for modeling and analyzing protocols, architectures, ASICS, embedded software systems,
Also active databases are special forms of ASMs, essentially systems of rules with so-
called event, condition and action component. The event and condition part together form
the ASM rule guard; the event describes the trigger which may result in firing the rule;
the condition extracts, from the context in which the event has taken place, that part
which must be satisfied to actually execute the rule, by performing the associated action.
This action part describes the task to be carried out by the database rule, if the event did
occur and the condition was true; it corresponds to the updates of ASM rules. Different
active databases result from variations of
a) the underlying notions of state, as constituted by the signature of events,
conditions and actions, and of their relation to the database states,
b) the scheduling of the evaluation of condition and action components
relative to the occurrence of events (e.g. using coupling modes and
c) the rule ordering (if any), etc.
ASMs provide a rigorous and flexible semantical basis to reflect and analyse these
different models for the interaction between active rules and the database proper, and to
classify their implementations. The Sequential ASM Thesis guarantees, for instance, that
the intuitive notion of active database ―actions‖, which may range from performing
simple operations to the execution of arbitrary programs, is captured completely by the
rigorous concept of ASM rule.
For some other widely used forms of system models, we now provide their explicit
definition in terms of ASMs.
One of the historically first and most important types of system models is constituted by
finite automata, also called Moore automata or Finite State Machines (FSM), which are
sequential ASMs where all the rules have the form
If ctl = i and in = a then ctl := j
with functions in for input, and ctl for internal (control) states, which assume only a finite
number of values. FSMs which yield also output (also called Mealy automata) are
equipped with an additional function out for output, which assumes only a finite number
of values, and is controlled by an additional update out := b in the ASM rule above. By analogy, Mealy-ASMs are ASMs whose rules are like those of Mealy automata, but with
the output update replaced by a fully blown ASM rule. In a similar fashion one can define
all the classical models of computation (e.g. the varieties of Turing machines, Thue
systems, Markov algorithms, Minsky machines, Recursive Functions, Scott machines,
Eilenberg’s X machines, Push Down Automata) and their modern extensions, like
relational database machines, Wegner’s interaction machines or timed automata or
Discrete Event Systems (DES).
DES are tailored to describe the control structure for the desired occurrence of events, in
the system to be modelled, by specifying allowed event sequences as belonging to
languages generated by finite automata. Time can be incorporated into Discrete Event
Systems by timer variables, whose update rules relate event occurrences and the passage
of time, thus constituting one among many other timed extensions of finite automata for
modelling real-time systems.
Wegner’s interacting machines add to Turing machines that each computation step may depend upon and also influence the environment, namely by reading input, and by yielding an output that may affect the choice of the next input by the environment. This
comes up to the following instantiation of ASMs, where ctl represents the current internal
state, headpos the current position of the reading head, and mem the function which
yields the current content (read: the memory value) of a tape position. In the traditional
notation of Turing machines by sets of instructions, the functions nextstate, move, print,
correspond to the machine program. They determine how the machine changes its control
state, the content of its working position, and this position itself, depending on the current
values of these three parameters. output represents an abstract output action, which
depends on the same parameters.
ctl := nextstate(ctl, mem(headpos), input)
headpos := move(ctl, mem(headpos), input)
mem(headpos) := print(ctl, mem(headpos), input)
output (ctl, mem(headpos), input)
Considering the output as written on the in-out tape comes down to defining the output
action as follows, where out is a function determined by the program instructions:
output:= input*out(ctl, mem(headpos), input).
Similarly, viewing the input as a combination of preceding outputs and the new user
input comes down to defining input as follows, where user-input is a monitored
function, and combine formalizes the way the environment mixes the past output with the new input:
input = combine (output, user-input)
The differentiation between Single and Multiple Stream Interacting Turing Machines is
only a question of instantiating input to a tuple (inp,…,inp) of independent input 1n
functions, each representing a different environment agent.
The classical models of computation come with simple data structures, typically integers
or strings, into which other structures have to be encoded to guarantee the universality of
the computational model. Modern modelling languages offer more and richer data
structures, but nevertheless the level of abstraction is usually fixed und thereby leads to
the necessity of encoding, when structures have to be modelled whose data types are not
directly supported by the modelling language. E.g. VDM models are instances of
sequential ASMs with fixed abstraction level, which is described by the VDM-SL ISO
standard. It is obtained by restricting sets to VDM-SL types (built from basic types by
constructors), functions to those with explicit or implicit definitions, operations to
procedures (with possible side effects), and states to records of read/write variables (0-
ary instead of arbitrary functions). Similarly CSP models, as well as their refinements to
OCCAM programs that can be executed on the TRANSPUTER, are known to be
instances of ASMs equipped with agents and with mechanisms for communication and
for non-deterministic choice. Parnas tables, which underlie the SCR approach to system
modelling, classify functions into monitored or controlled, without providing support for
system modularisation by auxiliary external functions. The table notation, used in SCR
for updating dynamic functions of time, reflects particular instances of ASMs. For
example, normal Parnas tables, which specify how a function value f(x,y) will change to
say t when a row condition r(x) and a column condition c(y) are true, represent the i,jij
ASM with the following rules (for all row indices i and all column indices j ):
If r(x) and c(y) then f(x,y) := t iji,j
Relational machines add to Turing machines arbitrary, but fixed relational structures.
The Unified Modeling Language (UML) shares with the ASM approach a general first-
order view of data structures, although UML documents do not formulate anything
which goes as far as the abstract-state postulate. Instead they describe the general first-
order view of data structures only vaguely by declaring the intended models to consist of
(read: universes of) ―things‖ (―abstractions that are first-class citizens in a model‖)
together with their relationships. UML comes with a set of graphical notations, which are
proposed as ―visual projections‖ into the textual, fully detailed specifications of system
models. This includes activity diagrams, state diagrams, and use case diagrams
(supported by collaboration and sequence diagrams), which are offered to model the
dynamic aspects of discrete systems, although no precise meaning is defined for these
diagram types by the UML documents. The dynamic semantics of these diagrams has
been defined rigorously using particular classes of ASMs, as a matter of fact sequential
ASMs for all diagrams that describe purely sequential system behaviour. For instance,
each sequential UML activity diagram, that is activity diagram with only synchronous
concurrent nodes, can be built from composing alternating branching and action nodes as
shown in Fig.1.
Fig. 1. ASM normal form of sequential UML activity diagrams
The meaning of alternating branching and action nodes is a generalization of the above
ASM rules for FSMs. In moving through such a diagram, along the arrows to perform in
succession the actions inscribed in the rectangles, being placed on an arc i visualizes
being in the control state i (i.e. ctl = i ); changing the position from one to another arc, as indicated by the arrows, visualizes changing the control state correspondingly. The input
, reading condition in = a in the FSM rules above is generalized to an arbitrary guard condj
which labels an arc exiting a branching node and leading to an action node action; it j
visualizes that when the control is positioned on the branching node, one is allowed to
perform action and to move correspondingly the control - namely from the arc entering j
the branching node, along the arc guarded by cond , to the arc, say j, which exits the jaction node action - if the condition cond is true in the current state. The output action jjout := b is generalized to an arbitrary ASM rule, which provides a rigorous semantical definition for what in UML is called and verbally described as an (atomic) action. Due to
the simultaneous firing of all rules of an ASM, in any state, this rational reconstruction of
an atomic UML action as one step of an ASM provides, within sequential systems, an
interpretation also for synchronous concurrent UML nodes.
Therefore Fig. 1 visualizes the ASM with the following set of rules (for all 0
If ctl = i and condthen action j j
ctl := j
where i,j stand for the control states visualized by the corresponding arcs.
Via this ASM normal form representation of sequential UML activity diagrams, the experimental evidence provided by the experience of 50 years of computing, namely that these diagrams represent a notation for a most general modelling language, is theoretically confirmed by the above-mentioned proof for the Sequential ASM Thesis.
The remaining UML diagrams, in particular class (object, component, deployment) diagrams, are used for modelling the static aspects of discrete systems, namely the signature of the model, together with the constraints imposed on its structure.
Sequential ASMs also naturally reflect the computational model of synchronous programming languages, like ESTEREL, that are widely used for modelling parallel synchronous systems. This is due to the ASM concept of simultaneous execution of all applicable rules, which is enhanced by the following operator to apply a rule for all elements satisfying a given condition:
forall x satisfying cond (x) do rule (x).
A typical use of such a rule is illustrated in the ASM model for Conway’s Game of Life, which consists of the following rule:
Forall c in Cell: if aliveNeighb(c) = 3 then resume(c)
if aliveNeighb(c) < 2 or aliveNeighb(c) > 3 then suspend(c)
where resume (c ) stands for alive(c) := true and suspend(c) for alive(c) := false. The rule expresses how at each step, for all cells in the system, their life status may change from non-alive to alive or vice-versa.
II. Distributed Systems.
Distributed systems consist of physically or logically separate, but concurrently executed sequential systems, which interact with each other via communication and synchronization, and typically lack global control while manifesting causal dependencies. From the point of view of each sequential component of a distributed system, the other components can be regarded in their entirety as environment, which continuously interacts with this component, concurrently and without any a priori known order of component and environment actions.
Distributed systems can be modelled as sets of cooperating sequential systems, independently of whether the transfer of information between the interacting agents is based upon shared memory, or upon a form of (synchronous or asynchronous) message-passing mechanism or of remote procedure calls. For distributed ASMs, the notion of run, which is defined for sequential systems as sequence of computation steps of a single