IFIP Working Group 2.2 Meeting
22 - 26 September 1997 in Graz, Austria.

Abstracts of the talks announced

A. Arnold
An experience with MEC in a real industrial project

How and why some formal methods have been applied to develop the embedded software of an household electricity meter.

Literature references:

Andre Arnold, Didier Begay, Jean-Pierre Radoux. The embedded software of an electricity meter: An experience in using formal methods in an industrial project. Science of Computer Programming, 28:93--110, 1997.

E. Boerger
A Programmer Friendly Modular Definition of the Semantics of Java

Extended abstract

R. Cleaveland
Building Better Buechi Automata: An Operational Semantics of Temporal Logic

This talk presents an operational semantics of Propositional Linear-Time Temporal Logic in the SOS style due to Plotkin. The semantics relies on the definition of a transition relation and an "accepting" predicate on states. Using the semantics as a basis, we show how one may build Buechi automata from from formulas that accept precisely the infinite sequences that are models of the formulas. This procedure improves on the one defined by Vardi and Wolper in their seminal 1986 LICS paper in several respects that will be described.

Ph. Darondeau (joint work with Eric Badouel)
Types of Petri Nets

We suggest a uniform presentation of all the classical families of Petri nets, based on a suitable concept of types. This presentation provides means for connecting and crossing families of nets. It allows also to construct a duality between automata and nets parametric on the type of nets. Some other potential applications are reviewed.

Literature references:

On the Synthesis of General Petri Nets, Inria-RR-3025 (Nov.1996)

H. Ehrig
Synchronization of Views and Loose Semantics of Typed Graph Productions

The concepts of views is used on two levels. First, so-called design views are developed for structuring specifications, that is, a system is modeled according to different views (e.g., representing the needs of different kinds of users) which have to be synchronized afterwards in order to build the whole system. Views can be specified by means of tkyped graph transformation systems, where the type graph determines the visible types and the productions describe the known operations of that view. The synchronization of views is done by the construction of cooperative parallel composition of graph transformation systems, developed by Leila Ribeiro in her PhD thesis.

If the specification is complete, a view may describe an observation of the system in operation. In this case we speak of a user view. It turns out that the semantics of such a view cannot be described by computations (i.e., graph transformations), but just by observations of computations of the global system. Such observations of computations cannot be represented by graph transformations in th usual sense because a local view may lack operations (productions) of the global system, so that state changes may be observed that do not have a cause in the local view.

Therefore, the notion of graph transition is introduced as loose semantics for productions, where the production specifies only a lower bound to the activities that are to happen during application. Contrastingly, in the classical double-pushout approach to graph rewriting, productions are interpreted as complete descriptions of the transformations to be performed.

For typed graph transformation systems a transition sequence semantics is developed, comprising all finite and infinite sequences of transition in a system. Moreover, this semantics is shown to be compositional w.r.t. the synchronization of views.

J. Esparza
Model-Checking Pushdown Automata

Pushdown automata (PDA) can be seen not only as language acceptors, but also as processes. As a process, the semantic of a PDA is no longer a language, but a Kripke structure. Temporal logics can be used as query languages to describe properties of this structure. The model-checking problem consists of deciding whether the Kripke structure of a given PDA is model of a given temporal formula or not. Since the Kripke structure associated to a PDA can be infinite, the many existing model-checking techniques for finite structures cannot be applied. In the talk I present algorithms for linear and branching-time logics, which I claim are easier to understand than the existing ones. They rely on a simple result of automata theory which is part of my undergraduate lecture on formal languages.

Literature references:

Bouajjani, Esparza, Maler: Reachability Analysis of Pushdown Automata: Application to Model-Checking. Proceedings of CONCUR '97.

R. Gorrieri (joint work with Nadia Busi and Gianluigi Zavattaro)
Is Linda Turing-powerful?

We introduce a process algebra containing the coordination primitives of Linda (asynchronous communication via a shared data space, read operation, non-blocking test operators on the shared space). We compare two possible semantics for the output operation, following two different intuitions expressed in Linda reference manual (Scientifing Computing Associates, 95). The former, we call ordered, defines the output as an operation that returns when the message has reached the shared data space; the latter, we call unordered, returns just after sending the message to the tuple space. The process algebra under the ordered semantics is Turing powerful, and this is proved by presenting an encoding of a Random Access Machine, a Turing powerful formalism. The main result of the paper is that the process algebra under the unordered semantics is not Turing powerful. The proof of this result is rather elaborate and consists in showing that the problem of termination is decidable under the unordered semantics; it is composed of two steps:
Net semantics:
We define a net semantics for the unordered semantics in terms of contextual Petri nets, i.e., nets with inhibitor as well as read arcs. This semantics preserves the interleaving behavior, hence also the possibility of deadlock.
Deadlock-preserving simulation:
Given the contextual P/T net semantics, we present a mapping on finite (standard) P/T nets that preserves deadlock. As deadlock is decidable on finite P/T nets, we conclude that the termination problem is decidable under the unordered semantics.
Intuitively, the language is no more Turing powerful under the unordered semantics because there is no way for a process to know if a sent message has already been rendered.

O. Grumberg
Selective Quantitative Analysis and Interval Model Checking

In this work we propose a verification methodology consisting of selective quantitative timing analysis and interval model checking. Our methods can aid not only in determining if a system works correctly, but also in understanding how well the system works. The selective quantitative algorithms compute minimum and maximum delays over a selected subset of system executions. A linear-time temporal logic (LTL) formula is used to select either infinite paths or finite intervals over which the computation is performed. We show how tableau for LTL formulas can be used for selecting either paths or intervals. We also show how to use the tableau for model checking formulas interpreted over paths or intervals.

To demonstrate the usefulness of our methods we have verified a complex and realistic distributed real-time system. Our tool has been able to analyze the system and to compute the response time of the various components. Moreover, we have been able to identify inefficiencies that caused the response time to increase significantly (about 50%). After changing the design we not only verified that the response time was lower, but were also able to determine the causes for the poor performance of the original model using interval model checking.

Literature references:

S. Campos, E.M. Clarke, O. Grumberg: ``Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System'', the Conference on Computer-Aided Verification (CAV'96), Rutgers, NJ, July-August 1996

He Jifeng

G. Holzmann
Model based verification

The LTL model checker Spin is founded on the classic Vardi/Wolper framework for automata- theoretic verification. I'll briefly review how Spin implements this full framework in the context of an on-the-fly verification system. I'll also discuss a recent addition to Spin's algorithms that is reminiscent of BDDs: Puri's graph-based encoding method,.

Much of the work on Spin is aimed at making model checking more easily accessible to non-experts. I'll try to give a brief demo of the application of this style of model checking to some significant design problems.

F. Honsell
Final semantics for pi-calculus

The fundamental ideas and techniques of Final Semantics are briefly presented. These are exemplified by providing Final Semantics for various pi-calculi in a category of hypersets. Due to the particular rules that govern the binding operators of $\pi$-calculi, it is useful, as a preliminary step, to give a higher order-syntax presentations of the $\pi$-calculi using as metalanguage LF, a {\em logical framework} based on typed $\lambda$-calculus. At an abstract level, such a presentation elucidates the role of free and bound channels. At a practical level it serves as the basis for the development of a computer assisted editor for reasoning on pi-calculus terms, based within the system COQ.

L. Lamport
A TLA Reduction Theorem

A reduction theorem allows one to derive properties of a finer-grained specification by proving properties of a coarser-grained version obtained by combining multiple atomic actions into one. A TLA theorem that generalizes most of the existing reduction theorems is presented. The full theorem handles liveness properties, but only the safety part will be described.

Literature references:

Richard J. Lipton. Reduction: A Method of Proving Properties of Parallel Programs. CACM 18 (1975), 717--721.

K. Larsen
REAL MODEL CHECKING

This talk will be divided into three parts.

In the first two parts the real-time verification tool UPPAAL will be presented. The tool is the evolving result of a research collaboration between Department of Computer Systems, Uppsala, and BRICS@Aalborg University. We will review the theoretical basis underlying the modelling and specification languages of UPPAAL as well as the algoritmic techniques applied in the tool. In particular, some recently developed and implemented space-saving techniques (saving upto 90% of the original space consumption) will be given. Recently, UPPAAL has been applied in a number of industrial case studies (with companies such as Bang&Olufsen, SAAB and AB) and we will comment on the outcome and leasons learnt from these collaborations.

In the final part we will present a recently established project VVS, Verification and Validation of Systems, which is a collaboration between Danish Technical Univeristy, Lyngby, BRICS@Aalborg and a company BEOLOGIC. The research is focused on improvements of the commercial tool VISUALSTATE marketed by BEOLOGIC.

Literature references:

See http://www.docs.uu.se/docs/rtmv/uppaal/ for the UPPAAL homepage, where the references below can be obtained.

[LP97]
Henrik Lönn and Paul Pettersson. Formal Verification of a TDMA Protocol Start-Up Mechanism. Accepted for presentation at the 1997 Pacific Rim International Symposium on Fault-Tolerant Systems. Taipei, Taiwan, 15-16 December, 1997. (PDF-format).
[HSLL97]
Klaus Havelund, Arne Skou, Kim G. Larsen and Kristian Lund. Formal Modelling and Analysis of an Audio/Video Protocol: An Industrial Case Study Using UPPAAL. Accepted for presentation at the 18th IEEE Real-Time Systems Symposium. San Francisco, California, USA, 3-5 December 1997.
[LLPW97]
Kim G. Larsen, Fredrik Larsson, Paul Pettersson and Wang Yi. Efficient Verification of Real-Time Systems: Compact Data Structure and State-Space Reduction. Accepted for presentation at the 18th IEEE Real-Time Systems Symposium. San Francisco, California, USA, 3-5 December 1997.
[LPW97c]
Kim G. Larsen, Paul Pettersson and Wang Yi. UPPAAL in a Nutshell. To appear in Springer International Journal of Software Tools for Technology Transfer 1(1/2), September 1997. (PDF-format).
[LPW97b]
Magnus Lindahl, Paul Pettersson and Wang Yi. Formal Design and Analysis of a Gear Controller: an Industrial Case Study Using UPPAAL. Technical Report ASTEC 97/09, Advanced Software Technology, Uppsala University, 1 August, 1997. (PDF-format).
[LPW97a]
Kim G. Larsen, Paul Pettersson and Wang Yi. UPPAAL: Status & Developments. In Proceedings of the 9th International Conference on Computer-Aided Verification. Haifa, Israel, 22-25 June 1997.
[KLLPW97]
Kåre J. Kristoffersen, Francois Larroussinie, Kim G. Larsen, Paul Pettersson and Wang Yi. A Compositional Proof of a Real-Time Mutual Exclusion Protocol. In Proceedings of the 7th International Joint Conference on the Theory and Practice of Software Development. Lille, France, 14-18 April, 1997.
[DKRT97]
P.R. D'Argenio, J.-P. Katoen, T.C. Ruys, and J. Tretmans. The bounded retransmission protocol must be on time!. In Proceedings of the 3rd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems. Enschede, The Netherlands, April 1997. LNCS 1217, pages 416-431.
[JLS96]
Henrik Ejersbo Jensen, Kim G. Larsen, and Arne Skou. Modelling and Analysis of a Collision Avoidance Protocol using SPIN and UPPAAL. In Proceedings of the 2nd SPIN Workshop. Rutgers University, New Jersey, USA, 5 August 1996.
[DKRT96]
P.R. D'Argenio, J.-P. Katoen, T. Ruys, and J. Tretmans. Modeling and Verifying a Bounded Retransmission Protocol. In Proceedings of COST 247, International Workshop on Applied Formal Methods in System Design. Maribor, Slovenia, June, 1996. Also appeared as Technical Report CTIT 96-22, University of Twente, July 1996.
[BGKLLPW96]
Johan Bengtsson, W. O. David Griffioen, Kåre J. Kristoffersen, Kim G. Larsen, Fredrik Larsson, Paul Pettersson and Wang Yi. Verification of an Audio Protocol with Bus Collision Using UPPAAL. In Proceedings of the 8th International Conference on Computer-Aided Verification. New Brunswick, New Jersey, USA, 31 July 31-3 August, 1996. LNCS 1102, pages 244-256, R. Alur and T. A. Henzinger (Eds.).
[BLLPW96]
Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, Wang Yi. UPPAAL in 1995. In Proceedings of Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Passau, Germany, 27-29 March, 1996. LNCS 1055, pages 431-434, T. Margaria and B. Steffen (Eds.).
[LPW95c]
Kim G. Larsen, Paul Pettersson and Wang Yi. Compositional and Symbolic Model-Checking of Real-Time Systems. In Proceedings of the 16th IEEE Real-Time Systems Symposium, Pisa, Italy, 5-7 December, 1995.
[BLLPW95]
Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson and Wang Yi. UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems. In Proceedings of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, New Brunswick, New Jersey, 22-24 October, 1995.
[LPW95b]
Kim G. Larsen, Paul Pettersson and Wang Yi. Diagnostic Model-Checking for Real-Time Systems. In Proceedings of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, New Brunswick, New Jersey, 22-24 October, 1995. (Abstract.)
[LPW95a]
Kim G. Larsen, Paul Pettersson and Wang Yi. Model-Checking for Real-Time Systems. In Proceedings of the 10th International Conference on Fundamentals of Computation Theory, Dresden, Germany, 22-25 August, 1995. LNCS 965, pages 62-88, Horst Reichel (Ed.).
[WPD94]
Wang Yi, Paul Pettersson and Mats Daniels. Automatic Verification of Real-Time Communicating Systems by Constraint Solving. In Proceedings of the 7th International Conference on Formal Description Techniques, Berne, Switzerland, 4-7 October, 1994.

J S. Moore
Mechanically Proved Theorems about A Non-Blocking No-Wait Counter

The ACL2 theorem prover is a theorem prover for applicative Common Lisp. In this talk I show one way it can be used to prove theorems about concurrent programs. The approach is quite direct: define an interleaved execution model as an interpreter in Common Lisp. Non-determinacy is handled via an ``oracle.'' To illustrate this approach I implement concurrent programs to increment a globally shared counter in a non-blocking, no-wait style. I prove that the counter never decreases (safety) and that it is incremented in during runs in which the total number of steps exceeds 5 times the number of processors. The proof involves the definition of a ``uniprocessor'' view of the system, i.e., an interpreter that executes a single process with a globally shared memory that ``chaotically'' changes. This uniprocessor view is related in a general way to the multiprocessor semantics. Length of the run in question assures us that at least one processor takes at least six steps. We then take the uniprocessor view from such a processor. It is easy to show that in six steps the processor increments the counter, unless the memory chaotically changes during that uniprocessor run. But the safety property of the multiprocessing system, and the general relation between the multiprocessing and uniprocessing views, establish that if the memory changes chaotically for the uniprocessor then the counter increases.

E.-R. Olderog
Correct Real-Time Software for PLCs

Programmable Logic Controllers (PLCs) are a simple type of processor that is widespread in industrial implementations of real-time controllers. Characteristic for PLCs are their cyclic behaviour consisting of reading sensor values, updating the local state, and outputing the updated values to actuators. The state transformation can depend on timers.

At Oldenburg we are currrently developing a tool-supported method for correct real-time software for PLCs. Our work takes place in the context of the project "UniForM" (Universal Formal Methods Workbench) [KPOBB96] that is performed in collaboration with the University of Bremen and an industrial partner from Berlin.

The central concept in our approach is that of a PLC-automaton [Die97a]. PLC automata can be seen as a special class of timed automata that can be easily complied into programs PLCs. Zhou Chaochen's Duration Calculus (DC for short) [ZHR91] is used both for stating real-time requirements and for providing a formal semantics to PLC-automata. Using this common semantic basis an algorithm for synthesizing PLC-automata from a subset of Duration Calculus called DC implementables [Rav95] has been developed [Die97b].

We illustrate our approach using the case study of the industrial partner for the control of a single track railway.

Literature references:

[KPOBB96]
B. Krieg-Brueckner, J. Peleska, E.-R. Olderog, D. Balzer, A. Baer, UniForM -- Universal Formal Methods Workbench. In: U. Grote, G. Wolf, Softwaretechnologie -- Statusseminar des BMBF, DLR, Berlin 1996.
[Die97a]
H. Dierks, PLC-Automata: A New Class of Implementable Real-Time Automata. In: M. Bertran and T. Rus (Eds.), Transformation-Based Reactive Systems Development (ARTS'97), LNCS 1231, (Springer-Verlag, 1997) pp. 111--125.
[Die97b]
H. Dierks, Synthesising Controllers from Real-Time Specifications. In: Proceedings of ISSS'97. IEEE, Antwerp, 1997.
[Rav95]
A.P. Ravn. Design of Embedded Real-Time Computing Systems. Thesis for the Doctor of Technics. Technical Report ID-TR: 1995-170, Technical University of Denmark, 1995.
[ZHR91]
Zhou Chaochen, C.A.R. Hoare, A.P. Ravn. A Calculus of Durations. Information Processing Letters 40/5 1991, 269--276.

A. Ravn (joint work with Zhiming Liu, Leicester University, UK)
A link between Duration Calculus and Timed Transition Systems

Duration calculus is a real-time interval logic which has shown some promise in specifying and reasoning about high level properties of embedded systems, see e.g. [1,2]. In these experiments, a design for a program in the form of state machines has been specified and verified in the same formalism. However, it may be easier to specify designs in a state machine notation and then link the properties of the design to the requirements. Such exercises have been undertaken a number of times, and are becoming increasingly important when we apply mechanical proof support, where tedious details may be automated using model checking tools. In this talk I report on a syntactic link between the proof system for TTS [3] and duration calculus.

Literature references:

[1]
E-R. Olderog, A.P. Ravn, and J.U. Skakkebæk. Refining system requirements to program specifications. In C. Heitmeyer and D. Mandrioli, editors, Formal Methods in Real-Time Systems, Trends in Software-Engineering, Chapter 5, pages 107--134. Wiley, 1996.
[2]
A.P. Ravn, H. Rischel, and K. M. Hansen. Specifying and verifying requirements of real-time systems. IEEE Trans. Softw. Eng., 19(1):41--55, 1993.
[3]
T. Henzinger, Z. Manna, and A. Pnueli. Temporal proof methodologies for timed transition systems. Information and Computation, 112(2):273--337, 1994.

W.-P. de Roever (joint work with Lars Kuehne and Jozef Hooman)
Towards Mechanical Verification of Parts of the IEEE P1394 Serial Bus

The IEEE P1394 Serial Bus standard provides high performance connections for data transfer between hardware components and is especially well suited for connecting multimedia devices. To achieve its mechanical verification, a high level specification is developed for the asynchronous part of the P1394 Link layer, using the verification tool PVS. We derive a formal framework which closely resembles the state machine approach used in the standard document. In this framework, a new parallel combinator characterizes synchronous message passing between transitions for which a set of messages is exchanged atomically. The combinator is mechanically checked for being commutative and associative. As expected, unclarities, ambiguities and unforseen properties need to be resolved in the specification of the Link layer. To date, important Link Layer properties have been handproved using linear time temporal logic; the next aim of the authors is the mechanization of these proofs in PVS.

D. Sangiorgi
Reasoning about processes usig (static) types

Type systems are widely-used in sequential programming languages. A type system may include, for instance, constructs for union, product, subtyping, polymorphism. These systems can easily be ``transplanted'' from sequential languages to message-passing process languages (for instance, those based on the pi-calculus). As in sequential languages, so in concurrent languages types are useful for static detection of programming errors, for improving the efficiency of the code generated by the compiler, and for enhancing the readability of programs. In the talk, I will show that types also have an important impact on behavioural properties of processes. Types act as a contract between a process and its environment and therefore reduce the number of legal contexts in which processes may conceivably be placed. This gives rise to notions of behavioural equivalences which are usefully coarser than those of the untyped language. I will also give examples of (static) type systems that are specific to the world of concurrent processes (i.e., not transplanted from sequential languages) and that allow us to prevent certain interferences among processes.

Literature references:

B.Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. Proc. LICS '93. A revised and extended version in journal of MSCS 6(5), 409--454, 1996.
B. Pierce and D. Sangiorgi. Behavioral Equivalence in the Polymorphic Pi-Calculus. Proc. 23th POPL, 1997.
D. Sangiorgi. The name discipline of uniform receptiveness. Proc. ICALP'97.

A. Tarlecki (joint work with Till Mossakowski and Wiesiek Pawlowski)
Combining and Representing Logical Systems

This work addresses important problems of building complex logical systems and their representations in universal logics in a systematic way. Following Goguen and Burstall, we adopt the model-theoretic view of logic as captured in the notions of institution and of parchment (a certain algebraic way of presenting institutions).

We propose a new, modified notion of parchment together with a notion of parchment morphism and representation, respectively. We lift formal properties of the categories of institutions and their representations to this level: the category of parchments is complete, and their representations may be put together using categorical limits as well. However, parchments provide a more adequate framework for systematic combination of logical systems than institutions. We indicate how the necessary invention for proper combination of various logical features may be introduced either on an ad hoc basis (when putting parchments together using limits in their category and then further modifying the result) or via representations in a universal logic (when parchment combination is driven by their representations).

Literature references:

T. Mossakowski, A. Tarlecki, W. Pawlowski. Combining and Representing Logical Systems. Proc CTCS'97, Santa Margherita Ligure, September 1997, LNCS.

F. Vaandrager
Testing Timed Automata

We present a generalization of the classical theory of testing for Mealy machines to a setting of dense real-time systems. A model of timed I/O automata is introduced, inspired by the timed automaton model of Alur and Dill, together with a notion of test sequence for this model. Our first result is a test generation algorithm for black-box conformance testing of timed I/O automata. Although it is highly exponential and cannot be claimed to be of practical value, it is the first algorithm that yields a finite and complete set of tests for dense real-time systems. Our second result is the identification of a subclass of timed I/O automata, called bounded response automata, for which a more efficient algorithm can be given.

Literature references:

J.G. Springintveld, F.W. Vaandrager and P.R. D'Argenio. Testing Timed Automata. Technical Report CSI-R9712, Computing Science Institute, University of Nijmegen, August 1997. Available through the URL http://www.cs.kun.nl/~fvaan/.

M. Wirsing (joint work with P. Cenciarelli, A. Knapp, B. Reus)
From sequential to multi-threaded Java: An event-based operational semantics

A structural operational semantics of a non trivial sublanguage of Java is presented. This language includes dynamic creation of objects, method calls and synchronisation of threads. First we introduce a simple operational description of the sequential part of the language, where the memory is treated as an algebra with suitably axiomatised operations. Then, the interaction between threads via a shared memory is described in terms of structures, called ``event spaces,'' whose well-formedness conditions formalise directly the rules given in the Java language specification. Event spaces are included in the operational judgements to develop the semantics of the full language, which is shown to extend the one for sequential Java conservatively. By changing the well-formedness conditions, while leaving the operational rules untouched, one can enforce different language implementations. An example is developed where this flexibility is used to capture optimising Java compilers.

J. Zwiers
Partial orders in linear time temporal logic.

Partial orders have been used in the past to formulate various transformations and proof rules for distributed systems. In this talk I will show how most of these results carry over to a framework based on (linear-time) temporal logic for actions. The theory is based on three types of action ordering, all three expressible in T.L. The aim of it is to have transformational design in combination with assertional and temporal logic reasoning. This combination has two aspects: If time permits I will discuss also the repercussions of including real-time into the framework.


WG 2.2 (darondeau@irisa.fr)