DOC

Discrete Systems Modeling

By Regina Elliott,2014-04-15 15:44
11 views 0
High level system design and analysis using Abstract State Machines. In Current Trends in Applied Formal Methods (FM-Trends 98) (D. Hutter, W. Stephan,

Discrete Systems Modelling

Egon Börger

Università di Pisa

OUTLINE

    I. Sequential Systems

    II. Distributed Systems

    III. Validation and Verification of Systems

GLOSSARY

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

    below.

    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,

    and

    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,

    etc.

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

    priority declarations),

    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

     cond1 action1

    

     condn actionn

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

Report this document

For any questions or suggestions please email
cust-service@docsford.com