Catálogo de publicaciones - libros

This work introduces a novel approach to modelling timed systems. The main idea consists of a new model of time which is both discrete and dense in the real numbers. This allows to use a discrete base formalism for the description of timed algorithms where system behaviors can be interpreted very straightforwardly in a timed manner without sacrificing that much precision.

Before we go into the details of the formalisms which we propose for modelling some classes of real-time and hybrid systems, we describe the role we give to formal methods in software engineering and some relevant features of formal methods which seem especially useful to us. This partly is an elaboration of ideas first developed by the author in [Rus94]. This discussion will present the context for the results described later, and it will be used to derive some desiderata for the formalism to be used according to our understanding of formal methods.

In computer science, system behaviors are often represented as a function from some time domain to some state domain . We will also use this approach.

Infinitesimals, i.e., numbers which are in some respect like zero and in some other respect unlike zero, have been used in mathematics since the beginning of the calculus. Robinson [Rob96] gives an overview of the use of infinitesimals in the history of the calculus: Leibniz uses infinitely small numbers in the development of the calculus without admitting their existence; he considers them to be useful fictions. De l’Hospital seemed to believe in the existence of infinitesimals, and he formulated Leibniz’ principles in a way which made the main inconsistency stand out – that infinitesimal quantities are sometimes treated as being equal to zero, and sometimes as being not equal to zero.

Different approaches exist for the description of discrete concurrent and reactive systems. Often used examples are automata models (including hierarchical and parallel automata like Harel’s StateCharts [Har87]), formalisms for the description of concurrent and reactive systems (including Lamport’s Temporal Logic of Actions [Lam94a, Lam94b] or Manna and Pnueli’s Fair Transition Systems [MP92, MP95]), different versions of Petri nets [Rei86], or even models used in theoretical computer science like Turing machines [Tur37].

We will define hybrid systems using the most important ideas from ASMs. First we define a classical approach to modelling hybrid systems, and then we define a novel, non-standard approach of modelling hybrid systems.

If Gurevich’s thesis is valid, ASMs can be used to model any sequential algorithm on any abstraction level. But algorithms are defined in an operational way, and they operate step by step. Often, a higher abstraction level than this is wanted for describing properties of systems. Temporal logics of different kinds are proposed for this in computer science (see [Pnu77] for the introduction of the concept into computer science, and [MP92, Lam94b] for several well-developed approaches).

A system is called concurrent if it is considered at an abstraction level where during its run-time, there are moments when several subsystems are active. For real-time systems, this is a typical case. For non-quantitative linear time, the interleaving approach and the synchronous approach are the most important modelling strategies. Since real-time models build on non-quantitative models and since we investigate a linear-time model, we will investigate how these two strategies are expressed in the ASM formalism and, more specifically, as NTASMs.

Synchronous systems are concurrent systems in which the components proceed in a lockstep fashion. An early investigated model of synchronous systems are cellular automata [vN66, Vol79], where the synchronously working components, which are called “cells” in this context, communicate according to some regular interconnection scheme, so that each cell only communicates with its neighbors. This abstraction is appropriate in applications in which the signal travel time in the system is not negligible. A more general model of synchronously working systems assumes a broadcasting communication, i.e., it assumes that an output of a component is instantaneously visible to each other component. In this section, we will investigate such a model of synchronous systems.

A concept which is often used in models of real-time systems is the deadline. A deadline is a point in time associated with an event so that the event must take place in a system run, and it must not take place after the deadline. This section will discuss how deadlines might be modelled in NTASMs.