Catálogo de publicaciones - libros

An application is modelled as an open system if the environment is not expressed explicitly in the model. Open systems are the paradigmatic case of reactive systems.

Consider the following scenario: A flip-flop is wired up so that with every rising edge of the clock, it changes its state.

As another example for the NTASM approach, let us describe and analyze Fischer’s real-time based synchronization protocol [Lam87]. It is meant to ensure mutual exclusion of access to commonly used resources via real-time properties of a shared variable. The idea is to use just one shared variable (which we call v) for coordinating the access to the critical section. The variable can contain a process id or some neutral value (which we call noProc). When a process wants to enter its critical section, it first has to wait until v=noProc; then it sets v to its process id, waits some time, and then reads v again. If v has kept the old value, i.e., the id of the process considered, the process may enter its critical section; on leaving the critical section, v is set to noProc again. If v has not kept its old value, the attempt has failed and the process must go back and wait again till v=noProc.

This section will present several NTASM interpretations of timing enhanced Petri nets. Petri nets without timing [Pet62, Rei86] are a widely used model for discrete nondeterministic distributed systems.

Timed and hybrid automata are formalisms for the description of real-time systems which are designed primarily to make algorithmic analysis possible [ACD93, AD94, ACH95].

Lewerentz and Lindner [LL95] designed a case study inspired from an industrial application. This case study was often used for illustration of features of different modelling formalisms for reactive systems.

The main result of this work is that there exists a model of quantitative linear time which is both discrete and dense in the real numbers, and which can be used for the description and analysis of algorithms which make use of quantitative properties of a linear dense model of time with purely discrete means.