Transformation-Based Reactive Systems Development

Frontmatter

What was Llull up to?

Anthony Bonner

Llull as computer scientist or why Llull was one of us

Abstract

Crucial notions on which Computer Science is based originated in Ramon Llull (a 13th-century philosopher from Majorca). Here we explore some of his original insights — and his plausible inspiration sources— and how these ideas have been available to us by way of Leibniz (and others).

Ton Sales

Deductive verification of real-time systems using STeP

Abstract

We present a modular framework for proving temporal properties of real-time systems, based on clocked transition systems and linear-time temporal logic. We show how deductive verification rules, verification diagrams, and automatic invariant generation can be used to establish properties of real-time systems in this framework. As an example, we present the mechanical verification of the generalized railroad crossing case study using the Stanford Temporal Prover, STeP.

Nikolaj S. Bjørner, Zohar Manna, Henny B. Sipma, Tomás E. Uribe

Refinement of Time

Abstract

We introduce a mathematical model of the timed behaviour of components with streams as input and output using a hierarchy of timing concepts. We distinguish non-timed streams, discrete streams with discrete or with continuous time, and dense streams with continuous time. We introduce a notion of a timed system component and formulate requirements for the time flow. We show how to compose timed systems in a modular way. We show that the introduction of time into a system model as well as the change of the timing model in the system development process is a refinement step.

Manfred Broy

The verus language: Representing time efficiently with BDDs

Abstract

There have been significant advances on formal methods to verify real-time systems recently. Nevertheless, these methods have not yet been accepted as a realistic alternative to the verification of industrial systems. One reason for this is that formal methods are still difficult to apply efficiently. Another reason is that current verification algorithms are still not efficient enough to handle many complex systems. This work addresses the problem by presenting a language designed especially to simplify writing real-time programs. It is an imperative language with a syntax similar to C. Special constructs are provided to allow the straightforward expression of timing properties. The familiar syntax makes it easier for non-experts to use the tool. The special constructs make it possible to model the timing characteristics of the system naturally and accurately. A symbolic representation using BDDs, model checking and quantitative algorithms are used to check system timing properties. The efficiency of the representation allows complex realistic systems to be verified.

Sérgio Campos, Edmund Clarke

Refining interval temporal logic specifications

Abstract

Interval Temporal Logic (ITL) was designed as a tool for the specification and verification of systems. The development of an executable subset of ITL, namely Tempura, was an important step in the use of temporal logic as it enables the developer to check, debug and simulate the design. However, a design methodology is missing that transforms an abstract ITL specification to an executable (concrete) Tempura program. The paper describes a development technique for ITL based on refinement calculus. The technique allows the development to proceed from high level “abstract” system specification to low level “concrete” implementation via a series of correctness preserving refinement steps. It also permits a mixture of abstract specification and concrete implementation at any development step.

To allow the development of such a technique, ITL is extended to include modularity, resources and explicit communication. This allows synchronous, asynchronous and shared variable concurrency to be explicitly expressed. These constructs also help in solving the problems, like lack of expressing modularity, timing and communication, discovered during the use of ITL and Tempura for a large-scale application [2].

Antonio Cau, Hussein Zedan

Integrating temporal logics and model checking algorithms

Abstract

Temporal logic and model checking algorithms are often used for checking system properties in various environments. The diversity of systems and environments implies a diversity of logics and algorithms. But there are no tools to aid the logician or practitioner in the experimentation with different varieties of temporal logics and model checkers. Such tools could give users the ability to modify and extend a temporal logic and model checker as their problem domain changes. We have developed a set of tools that provide these capabilities by placing the model checking problem in an algebraic framework. These tools provide a temporal logic test bed that allows for quick prototyping and easy extension to logics and model checkers. Here we discuss the usage of these tools to generate model checker algorithms as algebraic mappings (i.e., embeddings of one algebra into another algebra by derived operations) with the temporal logic as the source algebra and the sets of nodes of a model as the target algebra. We demonstrate these tools by extending CTL and its model checker by introducing formulas that quantify the paths over which the satisfaction of the temporal operators is defined. This is made possible by permitting propositions to label the edges as well as the nodes in the model. We use this logic and its model checker to analyze program process graphs during the parallelization phase of an algebraic compiler.

Teodor Rus, Eric van Wyk

PLC-automata: A new class of implementable real-time automata

Abstract

We introduce a new class of automata which are tailored for dealing with real-time properties modelling the behaviour of Programmable Logic Controllers (PLC) that are often used in practice to solve controlling problems. A semantics in an appropriate temporal logic (Duration Calculus) is given and an implementation schema is presented in a programming language for PLCs that fits the semantics. Finally, a case study shows the suitability of this approach.

Henning Dierks

Communication concepts for statecharts: A semantic foundation

Abstract

Statecharts have proved their usefulness for the development of real-time systems; one imagines that a precise semantics of communication between components is required for any successful application to embedded systems. This contribution shows how to do this. First, sequential automata and a parallel composition operator are introduced. Then, we introduce a scoping construct for ‘feedback’ (signal sharing between explicitly-named components of a parallel composition). The syntactic closure of these operations is called the class of ‘Mini-Statecharts’. We then discuss three different semantics that may be given to the feedback operator. They all have advantages and disadvantages, mainly mathematical, which are forthrightly discussed in depth and with clarity, using examples where necessary. The discussion is conducted within the framework of stream processing functions.

Peter Scholz, Dieter Nazareth

Regular processes and timed automata

Abstract

In [7], an algebra for timed automata has been introduced. In this article, we introduce a syntactic characterisation of finite timed automata in terms of that process algebra. We show that regular processes, i.e., processes defined using finitely many guarded recursive equations, are as expressive as finite timed automata. The proof uses only the axiom system and unfolding of recursive equations. Since the proofs are basically algorithms, we also provide an effective method to translate from one model into the other.

Pedro R. D'Argenio

A visual formalism for real time requirement specifications

Abstract

This paper presents a semantical basis of a graphical specification language, called real-time symbolic timing diagrams (RTSTD), to express real-time requirements of embedded systems. RTSTD allow a concise and unambigous formulation of real-time properties that are intuitively understandable by hardware designers. We give a precise semantical foundation of this graphical language in terms of real-time temporal logic. Due to this interpretation RTSTD can be embedded into existing verification tools to check whether an implementation satiesfies the given specification expressed as RTSTD.

Konrad Feyerabend, Bernhard Josko

Formal specification and verification method of concurrent and distributed systems by restricted timed automata

Abstract

In this paper, we propose the specification and verification method of distributed systems. We can easily specify fairness and timing constraints, and can effectively verify distributed systems by our proposed method. In order to specify fairness, an enable condition and a performed condition are attached to a finite set of states in our proposed specification method. In order to effectively verify distributed systems, we restrict timing constraints of timed automaton such that in cycles we must specify timing constraints about the clock variables after they are reset to zero.

We have developed the verification systems based on our proposed method, and have shown it effective by timed Alternating Bit Protocol.

Satoshi Yamane

Transformational formal development of real-time systems

Abstract

This paper presents techniques for the transformational formal development of reactive and real-time systems, using a combination of the VDM⁺⁺ formal method and the HRT-HOOD method. A case study of a chemical control system is used to illustrate the techniques.

K. Lano, A. Sanchez

A transformation of monitor into communication synchronized parallel processes: A systematic refinement step in design

Abstract

A systematic transformation of a program formed by a set of parallel processes, which invoke a monitor, into an equivalent program formed by the same set of parallel processes, but with a new parallel communicating process simulating the proper monitor, is introduced. Monitor invocations are replaced by simple rendez-vous communications with the new monitor process. The transformation is classified as a systematic (deterministic) refinement transformation since more detail is added and uncovered.

The place and functionality of the transformation within the Ramon Llull System, a development environment for concurrent and distributed programs being used at industry and academia, is commented and related to other transformations within it. Some extensions and modifications of the basic transformation are proposed, to widen its application scope.

Miquel Bertran

Contracts for ODP

Abstract

Contracts have been introduced to clarify the dependencies and relations between objects and thus to ease component reuse. In the OO design trajectory, contracts can be used at different levels of abstraction. We focus on a computational view of objects. We consider systems described as configurations of interacting objects and we deal with two types of communications: message passing and flows. In message passing, signals (from one object to another) are conveyed through the (implicit) underlying infrastructure. This form of interaction is suitable for client/server applications where no strong real time or ordering constraints are needed from the communication infrastructure. In contrast, in a flow type of communication, signals are conveyed through third party (binding) objects that may be explicitly called for in order to ensure specific QoS requirements needed by specific applications. We first define an abstract semantics of the behaviour of configurations of computational objects. Our semantics will be based on the observation of interactions. An Interaction takes place between two interfaces of two objects and may have one of two issues: success or failure. We introduce COC, a calculus of object contracts. In our setting, a contract is merely a process which observes and arbitrates the collective behaviour of configurations of objects. A contract observes objects and depending on the outcome of their interactions (success or failure) may identify and incriminate faulty objects. We also abstract from observers and define the concepts of satisfaction, realization and refinement.

Arnaud Février, Elie Najm, Jean -Bernard Stefani

Affine transformations in Signal and their application in the specification and validation of real-time systems

Abstract

In this paper we present affine transformations as an extension of the Signal language for the specification and validation of real-time systems. To each Signal program is associated a system of equations which specify synchronization constraints on clock variables. The Signal compiler resolves these equations and verifies if the control of a program is functionally safe. By means of the new transformations, affine relations can be defined between clocks and it gets necessary to enhance the compiler with facilities for the resolution of synchronization constraints on these clocks. We propose thus an extension of the compiler based essentially on a canonical form of the affine relations.

Irina Smarandache, Paul Le Guernic

Action-based concurrency and synchronization for objects

Abstract

We extend the Action-Oberon language for executing action systems with type-bound actions. Type-bound actions combine the concepts of type-bound procedures (methods) and actions, bringing object orientation to action systems. Type-bound actions are created at runtime along with the objects of their bound types. They permit the encapsulation of data and code in objects. Allowing an action to have more than one participant gives us a mechanism for expressing n-ary communication between objects. By showing how type-bound actions can logically be reduced to plain actions, we give our extension a firm foundation in the Refinement Calculus.

Ralph Back, Martin Büchi, Emil Sekerinski

Communication Extended Abstract Types in the refinement of parallel communicating processes

Abstract

A systematic refinement transformation of a program involving processes communicating through simple rendez-vous type connections is described. Both new connections and new processes are introduced in the refined program form. The refinement is based in the concept of Communications Extended Abstract Type (CAT), which is also covered, and it amounts to either selecting, or unhiding, a CAT implementation.

This refinement approach is made possible in the framework of a notation, PADD, which treats parallelism and parametric abstract types as two independent entities, combining them simply. Then, the operations of CAT implementations may involve parallel internal composition. As a consequence, a CAT may have both behavioral (unrefined) as well as structural (refined) implementations.

A framework for the organization and partition of correctness proofs, including timing aspects, is given. It is based on the refinement method and the CAT concept. The constructs and tools associated with the method are being incorporated into The Llull System (TLS), the current environment for the PADD notation, being used both at the university and industry.

Miquel Bertran, Felipe Alvarez-Cuevas, Albert Duran

Verification and refinement of distributed programs in a fair framework

Abstract

In this paper, we present a technique to prove progress properties of non-terminating concurrent programs and to refine them in such a way that these properties are preserved. We rely on strong fairness assumptions about the language implementation.

We define a simple language based on Hoare-78 CSP. A program denotes a set of finite and infinite traces corresponding to all its possible computations. The semantics of a program is defined as the set of its fair traces. We also give a liveness-preserving implementation notion. Proof rules concerning progress properties and correction of refinements are given. We show that these proof rules are consistent with the given fair semantics. Finally, we verify and refine a non-trivial case study.

Luis A. Galán, Ricardo Peña

Formalizing real-time scheduling as program refinement

Abstract

This paper shows how the feasibility of scheduling a realtime program consisting of a number of parallel processes (tasks) can be proved as a step in the refinement of the program from its specification. Verification of this step of refinement makes formal use of methods and results from real-time scheduling theory.

Zhiming Liu, Mathai Joseph

Specification and refinement of continuous real-time systems

Abstract

This paper describes techniques for the specification and refinement of control and simulation software for systems involving continuous and discrete data. We give a formal concept of refinement suitable for this domain, which generalises conventional refinement in VDM-SL.

We also show how VDM⁺⁺ can be used in conjunction with classical discrete controller synthesis techniques.

Stephen Goldsack, Kevin Lano, Eugene Durr

High-level execution time analysis

Abstract

A compositional algebra, called mMCAN, for the execution time analysis of highlevel software processes is introduced. In mMCAN, processes can be concatenated, concurrently executed, and recursively invoked. We show that the set of execution times of an mMCAN is semilinear. We then propose and analyze an algorithm which calcuates the execution time sets of an mMCAN in semilinear forms. Finally, we consider several interesting variations of mMCAN whose execution time sets can be computed with algorithms.

Farn Wang

A sound and complete proof system for probabilistic processes

Abstract

In this paper we present a process algebra model of probabilistic communicating processes based on classical CSP. To define our model we have replaced internal non-determinism by generative probabilistic choices, and external non-determinism by reactive probabilistic choices, with the purpose of maintaining the meaning of the classical CSP operators, once generalized in a probabilistic way. Thus we try to keep valid, as far as possible, the laws of CSP. This combination of both internal and external choice makes strongly difficult the definition of a probabilistic version of CSP. In fact, we can find in the current literature quite a number of papers on probabilistic processes, but only in a few of them internal and external choices are combined, trying to preserve their original meaning.

Starting with a denotational semantics where the corresponding domain is a set of probabilistic trees with two kinds of nodes, representing the internal and external choices, we define a sound and complete proof system, with very similar laws to those of the corresponding CSP.

F. Cuartero Gómez, D. de Frutos Escrig, V. Valero Ruiz

Testing semantics for a probabilistic-timed process algebra

Abstract

In this paper we present a probabilistic-timed process algebra, which tries to unify the best solutions of previous probabilistic and timed algebras. We provide an operational semantics for the new language (PTPA), and from this operational semantics we define a testing semantics based on the probability with which processes pass tests. Afterwards the induced testing equivalence is operationally characterized by probabilistic timed traces.

Carlos Gregorio-Rodríguez, Luis Llana-Díaz, Manuel Núñez, Pedro Palao-Gostanza

Denotational semantics for timed testing

Abstract

In this paper we present a denotational semantics for a timed process algebra, which is fully abstract with respect to the must testing semantics previously developed [Lla96,LdFN96]. The domain of semantic processes is made up of consistent sets of barbs, which generalize the notion of acceptance sets, in such a way that the actions that are offered but not taken in each state are also recorded. the main difficulty when defining this denotational semantics has been that the natural ordering between semantic processes cannot be proved to be complete. So an alternative stronger complete ordering has to be considered, which is proved to be consistent with the original one, in the sense that lubs of chains with respect to the new ordering are also lubs with respect to the original one.

Luis Fernando Llana Díaz, David de Frutos Escrig

Extending LOTOS with time: A true concurrency perspective

Abstract

An ongoing restandardisation activity is currently extending the OSI specification language LOTOS with quantitative time. We give an alternative perspective on this activity. We highlight a very simple but expressive timed LOTOS enhancement which is based on time intervals. The main point at which we depart from the standard approach to extending LOTOS with time, is that we employ a true concurrency semantics. We present a semantics based on a time extended bundle event structures. We give a full semantics for relating our timed LOTOS to timed bundle event structures. A fixed point theory is defined and finally, we describe how urgency can be supported in the language.

Howard Bowman, John Derrick

Introduction of a suspend/resume operator in ET-LOTOS

Abstract

We present in this paper a suspend/resume operator for ET-LOTOS (a timed extension of LOTOS). We focus on the way it can be defined and on its usefulness for the specification of real-time systems. We show that this operator is essential to specify typical real-time systems and we give a specification technique to describe this kind of system. We apply our operator and method to a small example.

Christian Hernalsteen, Arnaud Février

Specification and verification of a real-time field bus with formal description languages

Abstract

In this work the real-time field bus PROFIBUS for industrial communication networks, is specified with the formal specification language LOTOS and its associated tools. The paper introduces the general characteristics of LOTOS and its related tools, and the main features of PROFIBUS particularly the related with its data link layer. The methodology and data types implemented are explained, with an instance of developed performance tests for the specification. Results and new guidelines of this work are explained in last paragraph devoted to conclusions and future works. With LOTOS specification of PROFIBUS protocol comes up the possibility and benefit of using formal descriptions techniques for designs in the field of industrial communications.

Mariño P., Poza F., Domínguez M., Nogueira J.

Backmatter