IFIP Working Group 2.2 Meeting
28 June - 1 July 1999, Udine, Italy.

Abstracts of the talks announced

Javier Esparza
...

Davide Sangiorgi
Coinductive techniques based on bisimulation

The most popular method for establishing bisimilarities results is to exhibit bisimulation relations. I will discuss generalisations of the method aimed at reducing the size of the relations to exhibit and hence relieving the proof work needed to establish bisimilarity results. The core of the talk is based on the paper
"On the bisimulation proof method", D. Sangiorgi, Journal of MSCS, 8, 1998.

I will also discuss more recent developments, including: the applications of the new techniques to functional languages (especially the work of Soren Lassen) and to process calculi for cryptography (Boreale, De Nicola, and Pugliese), their implementation and their application in mechanical verification of infinite-state-space processes (Hirschkoff), their use in the prove of decidability results for bisimilarity on infinite graphs (Caucal).

Finally, I will mention some (in my opinion, very challenging) open problems such as: how to adapt the new techniques to higher-order languages; how to recast this theory in the framework of final coalgebras (an apparently ideal framework for understanding coinductive principles and techniques).

Egon Boerger (joint work with Wolfram Schulte)
Modular Design for the Java Virtual Machine Architecture

We provide concise abstract (ASM) code for running the Java Virtual Machine (JVM). First we define a fast JVM as platform for provably correct Java compilation, exhibiting a general compilation scheme of Java programs to JVM code. These definitions, together with the definition of an abstract interpreter of Java programs given in the previous lecture, allow us to prove that any compiler that satisfies some natural conditions compiles Java code correctly. As a by-product we provide a challenging realistic case study for mechanical verification of a compiler correctness proof. We have also validated our JVM and compiler specification through experimentation.

The modularity of our definitions for Java, the JVM and the compilation scheme exhibit orthogonal language, machine and compiler components, which fit together and provide the basis for a stepwise and provably correct design--for--reuse. We extend the above JVM to a defensive JVM which can be used safely as Java independent platform for executing arbitrary byte code. We then separate the bytecode verification machine part from the executing part and obtain in such a way a model for the bytecode verifier. As last step we integrate this bytecode verifier into a loading machine which together with the executing ASM provides a full JVM model.

Stephan Merz
A More Complete TLA

Lamport has proposed the Temporal Logic of Actions, a variant of linear-time temporal logic, whose formulas cannot distinguish between behaviors equivalent with respect to stuttering. Although TLA has turned out to be very successful, we identify two shortcomings: We argue that these two problems are related and define an extension of TLA that is still invariant under stuttering, but which has a more liberal syntax and admits a rather simple axiomatization.

Anders P. Ravn (joint work with Mauno Rönnkö and Kaisa Sere)
Evolution in Action Systems -- Hybrid Action Systems

Action Systems were introduced by Back and Kurki-Suonio in 1983 as a predicate transformer based formalism for modelling reactive systems. They have since then been thoroughly investigated and applied in many contexts. The associated refinement calculus is a central tool in the framework. Recently we have been investigating how to extend the framework such that it can be applied to hybrid and real-time systems. It turns out that a simple solution is to add a differential action. It has a weakest precondition semantics that characterize the initial states for an evolution to given post states [1]. It allows an interesting interpretation of parallel composition as addition of differentials [2]. It may also be transformed to a path equivalent evolution or abstracted to an assignment action within the framework [3].

The talk introduces these developments and discusses some alternatives that we are considering.

[1]
M. Rönnkö and A.P. Ravn. Action Systems with Continuous Behaviour. In Hybrid Systems V, LNCS 1567, pp. 304-323, 1999.
[2]
M. Rönnkö and A.P. Ravn. Switches and Jumps in Hybrid Action Systems. In Proc. Estonian Ac. of Sc., Engineering, 4, 2, pp. 106-118, 1998.
[3]
M. Rönnkö and K. Sere. Refinement and Continuous Behaviour. In Hybrid Systems: Computation and Control, LNCS 1569, pp. 223-237, 1999.

Wojciech Penczek
Partial order reductions preserving simulations

The "state explosion problem" can be alleviated by using partial order reduction techniques. These methods rely on expanding only a fragment of the full state space of a program, which is sufficient for verifying the formulas of temporal logics LTL-X or CTL*-X (i.e., LTL or CTL* without the next state operator). This is guaranteed by preserving either a stuttering maximal trace equivalence or a stuttering bisimulation between the full and the reduced state space. Since a stuttering bisimulation is much more restrictive than a stuttering maximal trace equivalence, resulting in less powerful reductions for CTL+-X, we study here partial order reductions that preserve equivalences "in-between", in particular a stuttering simulation which is induced by the universal fragment of CTL*-X, called ACTL*-X. The reductions generated by our method preserve also branching simulation and weak simulation, but surprisingly, they do not appear to be included into the reductions obtained by Peled's method for verifying LTL-X properties. Therefore, in addition to ACTL*-X reduction method we suggest also an improvement of the LTL-X reduction method. Moreover, we consider concurrency fair version of ACTL*-X and prove that reduction for fair ACTL*-X is much more efficient than for ACTL*-X. We present experimental results showing the efficiency of our method.

Emil Sekerinski
On Class Refinement

Class invariants, as an extension of the idea of module or data type invariants, appear as a technique for documenting and specifying classes in object-oriented programs in general and are part of languages like Eiffel. The rules for class invariants state that (1) each method must preserve the invariant and the initialization must establish it and (2) for guaranteeing "safe substitutability", a subclass must not weaken the invariant (but can weaken the precondition and can strengthen the postcondition of each method). It turns out that in the case of Eiffel, these two rules fail to be sufficient for (at least) five different reasons. Some of those are specific to Eiffel but (at least) two are of general interest: the effect "super-calls" can have and the effect that certain inheritance structures can lead to interference of methods. We argue that there is a need for a formal analysis of the effects and present our results so far. Our model formalizes classes with private attributes, protected attributes, public methods, invariants, inheritance, and self- and super-calls. Statements are modelled by predicate transformers, thus allowing statements to be nondeterministic. The notion of class refinement is introduced. Classes are extended to allow action-based concurrency of objects. Class refinement is justified with respect to trace refinement. The whole formalization is expressed in the simple typed lambda calculus.

Gheorghe Stefanescu
Mixed network algebra: towards an algebraic calculi for software components.

The talks focuses on Network Algebra and the associated Calculus of Flownomials. It is a polynomial-like calculus for representing flow-graphs and their behaviors.

An `additive' interpretation AddNA of the calculus was intensively developed to study control flowcharts and finite automata. On the other hand, a `multiplicative' interpretation MultNA of the calculus was developed to study data-flow networks.

However, both interpretations are restrictive: flowcharts have not good parallelism, while data-flow networks have not good control. Actually, the key problem in understanding Multi-Agent Systems is just to find a theory which integrates the (multiplicative) reactive part and the (additive) control part of such systems.

The claim of our recent research is that the mixture of additive and multiplicative network algebras MixNA may be used to get an algebraic calculus for (concurrent, object-oriented) software systems.

The talk will contain an introduction to Network Algebra and some more advanced results related to the Mixed Network Algebra project. For more informations, papers, etc. see: http://hypatia.dcs.qmw.ac.uk/authors/StefanescuGH/ http://funinf.math.unibuc.ro/~ghstef/

Don Sannella (joint work with Furio Honsell)
Pre-logical relations

Logical relations are structure-preserving relations between models of typed lambda calculus. They are used extensively in the study of typed lambda calculus and have applications outside lambda calculus, for example to abstract interpretation and data refinement.

We propose a weakening of the notion of logical relations, called pre-logical relations, that has many of the features that make logical relations so useful but having further algebraic properties including composability. The basic idea is simply to require the reverse implication in the definition of logical relations to hold only for lambda-expressible functions. Pre-logical relations are the minimal weakening of logical relations that gives composability for extensional structures and simultaneously the most liberal definition that gives the Basic Lemma of logical relations.

The use of pre-logical relations in place of logical relations gives an improved version of Mitchell's representation independence theorem which characterizes observational equivalence for all signatures rather than just for first-order signatures. Pre-logical relations can be used in place of logical relations to give an account of data refinement where the fact that pre-logical relations compose explains why stepwise refinement is sound.

F.S. de Boer
Reasoning about the correctness of object-oriented programs

Francesca Rossi
Recent results on soft constraint solving and programming

Soft constraints generalize classical constraints in that they have various levels of satisfaction, not only two (satisfied or not). Our formalization of soft constraints is general enough to have, as instances, many useful classes of soft constraints, like fuzzy constraints, optimization problems, problems with uncertainties, and others. This means that many real-life problems can be naturally represented by using soft constraints.

In this talk, I will first give the main motivations for soft constraints, their formalism and properties, some solution algorithms, and a formal way to use them within logic programming and to define the semantics of the resulting programming formalism. Then, I will describe some promising directions for research, like the use of abstraction to solve soft constraints more efficiently, the use of learning to ease the modelling task, and the definition of domain and propagation approximations for existing programming languages based on soft constraints.

Masami Hagiya (joint work with Koichi Takahashi and Mitsuharu Yamamoto)
Abstact Model Checking --- Algorithms and Applications

We first give a framework for abstract model checking with incremental generalization using a heuristic generalization procedure, where abstraction is incrementally performed while reachable states are being explored. We present the algorithm for reachability analysis as well as its variations and extensions including the shortest path algorithm.

As a concrete example of the framework, we describe verification of the alternating bit protocol by arithmetic generalization, where states with different integer parameters are generalized to a state with arithmetic variables. We proved safety and liveness of the alternating bit protocol by this approach.

As another example of abstract model checking, we also report our previous work on verifying algorithms for concurrent garbage collection. By abstract model checking, we verified several algorithms for concurrent garbage collection with a single abstraction mapping. An abstract heap was defined as a set of abstract cells. In order to define abstract transitions on abstract heaps, procedures called filters were introduced, which delete inconsistent abstract cells from an abstract heap. We also did an experiment of finding new algorithms by model checking, whose results were used as inputs to abstract model checking and successfully verified. Verified algorithms are: on-the-fly, a variant of on-the-fly, snapshot, and a variant of snapshot. VCGC is now under investigation.

Razvan Diaconescu
Behavioural methodlogies for algebraic specification and verification

Behavioural methodologies seem to be very promising for the design, prototyping and development of systems in the algebraic specification framework. In this talk we present several behavioural methodologies based on the new CafeOBJ algebraic specification language. However, these could be applied in the context of any other modern algebraic specification language supporting a behavioural formalism close enough to CafeOBJ hidden algebra. Most notably, this should be valid for CASL in the context Bidoit and Hennicker so-called "observational logic".

After some methodology rationale, the talk moves into a very brief presentation of CafeOBJ, including its language foundations and main features. The we discuss briefly the CafeOBJ hidden algebra formalism, extending the classical Goguen hidden algebra in several ways, most notably with operations having possibly several hidden sorts for the arguments, and introducing the crucial *behavioural coherence" property for operations.

The next part of the talk concentrates on the basic behavioural methodology for specification and verification emphasising an object-oriented style of specification with various advantages, one of them being a drastic simplification of the verification stage. Several *coherence* methodologies are also classified.

The final part of the talk presents a component-based behavioural specification and verification methodology based on the so-called *projection operations* and which constitutes the main CafeOBJ methodology for the object-oriented development of large systems.

Masahiko Sato
A simply typed context calculus

Marta Z Kwiatkowska
Issues in automatic verification of probabilistic systems

Francesco Parisi Presicce
Refinement (and modules) for graph transformation systems

Michel Bidoit (joint work with Rolf Hennicker)
Observational Logic

In this talk we propose a logical framework for specifying observational properties of software systems which is particularly suited for describing state-based systems like object-oriented programs. The basic assumption is that states are invisible "from the outside" and can only be observed via a distinguished set of observer operations which determine an "indistinguishability relation" between states. Thus it is possible to abstract from concrete state representations and to focus on the observable behaviour of a program. For the formalization of the above ideas we introduce the institution of "observational logic" which allows us to build specifications in a modular way. Moreover, we present a (sound and complete) proof system for verifying observational properties of components and system specifications.

K.V.S. Prasad
Can rendezvous implement broadcast?

Igor Walukiewicz
Is there a place for trace logics?

Gabriel Ciobanu (joint work with Mihai Rotaru)
Decomposing input guards in pi-calculus

He Jifeng
The least completion approach to automatically induce the enriched semantics

Ugo Montanari (joint work with Roberto Bruni)
Higher-order tiles

Mariangiola Dezani-Ciancaglini
Mutating Objects

Peter D. Mosses
Modular SOS

I'd like to draw the attention of (at least) the WG2.2 meeting participants to some recent papers that give examples of the use of the framework to be presented in my talk. Should I send messages myself to the various mailing-lists, or would you rather collect such information from all the participants and send it in a single message?

Rocco De Nicola
A kernel language for agents, interaction and mobility

Simone Martini
Some new results on the complexity of optimal reduction in the lambda-calculus

Philippe Darondeau
Perspectives of Petri Net Synthesis

Two usual examples of net synthesis problems are the realization of automata by Petri nets (up to isomorphism of automata), and the realization of regular languages by Petri nets (up to language equivalence). These problems amount to construct particular product decompositions of the objects to realize, using 1-place nets as components and extracting places from regions in automata or in languages. After a brief survey of the field, we show that computing regions w.r.t. general Petri nets can be done by computing the extremal rays of a polyhedral cone. Distribution constraints on the synthesized net can also be accomodated in this framework, providing an automated tool for the distributed implementation of automata. We indicate next the solution of extended forms of Petri net synthesis, such as constructing a Petri net with behaviour bounded by two regular expressions, or constructing a Petri net with reachability graph isomorphic to a context-free graph. We report on the difficulties to solve for extending the net synthesis techniques to languages of High Level Message Sequence Charts and to controllers of Discrete Event Systems.

J Strother Moore
Proving Theorems about Java Byte Code

We describe a formalization of an abstract machine very similar to the Java Virtual Machine but far simpler. We develop techniques for specifying the properties of classes and methods for this machine. We develop techniques for mechanically proving theorems about classes and methods. We discuss two such proofs, that of a static method implementing the factorial function and of an instance method that destructively manipulates objects in a way that takes advantage of inheritance. We conclude with a brief discussion of the advantages and disadvantages of this approach. The formalization and proofs are done with the ACL2 theorem proving system.

Amir Pnueli
Abstraction and composition: from infinite to finite-state systems

Andrzej Tarlecki
Architectural specifications in CASL

One of the most novel features of CASL, the Common Algebraic Specification Language, is the provision of so-called architectural specifications for describing the modular structure of software systems. A brief discussion of refinement of CASL specifications will provide the setting for a presentation of the rationale behind architectural specifications. This will be followed by some details of the features provided in CASL for architectural specifications, hints concerning their semantics, and simple results justifying their usefulness in the development process.


WG 2.2 (darondeau@irisa.fr)