Logistics
Where: Prato, Italy
When: 610 September 2004
Host: Bertrand Meyer
Here is an overview of Prato and the
Monash center. Here are many more
pictures, courtesy of Carroll Morgan and Gary Leavens.
Topics of discussion

Cliff Jones, Beyond "Verifying Compiler".
One conclusion: The "Verifying Compiler" should not be concerned with
verifying the absence of bugs, but help with the design of software.
Recommended reading:
 Donald MacKenzie's 1995 work that analyzes the failures that led to some
1100+ deaths
 Jones, Hoare, and Randell: "Extending the horizons of DSE [Grand Challenge GC6 on "Dependable Systems Evolution", accepted by UKCRC]"
Discussion of the Grand Challenge of a Verifying Compiler (or, a Verifying
Development Environment)
 Gary Leavens, AliasFree Formal Parameters
Aliasing among formal parameters, and among formals and globals,
causes problems for both optimization and reasoning; such aliases are
a source of subtle errors in programs. Wholeprogram static analysis
could provide knowledge about such aliasing, but it is nonmodular,
expensive, and conservative. All of these characteristics are
undesirable for reasoning.
I will describe a small extension to Java and JML that leads to
significantly better optimization opportunities for a compiler and
allows modular reasoning. The extension allows aliasing among
arguments and globals at the call site, but guarantees there will be
no overlap among arguments and globals inside method bodies, and also
allows methods to have specifications that "work" for overlapping
arguments. This is done by having multiple bodies for each procedure,
up to one for each aliasing pattern. Procedure calls are
automatically dispatched to the body that matches the runtime
aliasing pattern among the actual parameters and the globals.
This talk is based on joint work with Medhat Assaad and Olga
Antropova. Thanks to Jim Horning, Murali Sitaraman, Greg Kulczycki,
William Ogden, and Bruce Weide for discussions of related topics.
This work is supported in part by the US National Science Foundation
under grants CCR9803843, CCR0097907, CCR0113181, CCF0428078, and
CCF0429567.
 Peter Müller, Modular verification of object and module invariants
(joint work with Rustan Leino)
The talk describes a methodology for specifying and verifying
objectoriented programs, using object invariants to specify the consistency
of data and using ownership to organize objects into dynamic contexts.
Object invariants can describe a large variety of properties, including
properties of cyclic data structures. The methodology is designed to
allow modular reasoning, even in the presence of subclasses and callbacks.
Module invariants describe properties of variables that are shared by
several objects. I would like to discuss how the presented methodology for
object invariants can be adapted to cover module invariants.
 Bertrand Meyer, The Dependent Delegate Dilemma
.
 Pamela Zave, A formal model of addressing for interoperating networks.
 Annabelle McIver, Optimal strategies for twoplayer parity games
In this talk I will discuss the problem of finding optimal strategies
for twoplayer games.
Game models of programs can be useful in the specification and analysis of
temporalstyle properties. In such models players compete to optimise
some specified reward function. Of particular interest are the
strategies they employ for winning the game and, amongst those, "memoriless"
strategies  those which only depend on the current game configuration 
are arguably the most useful of all.
It has recently been proved that in the stochastic paritygame setting
optimal memoriless strategies exist for each player  and in fact they can
be assumed to be "pure", ie. they do not need to be randomised.
Unfortunately determining those optimal memoriless strategies can be
problematic.
I will show how optimal memoriless strategies can be computed reasonably
simply, provided that nonpure strategies are an acceptable solution.
 Michael Jackson, The problem of the banker with 52 cards.
A “banker” has an ordinary 52card deck of cards. You have some
positive amount of money. The banker decides on the order of the
cards. Before the banker turns each card over, you place a bet.
You put some proportion of you money on “red” and the rest on “black”.
After the banker turns over the card, you lose the money you bet on the
losing color, and double the money you put on the winning color.
Design a strategy that maximizes your guaranteed gain, and prove this
strategy correct.
 Ian Hayes, Finding Faults
Examining systematic methods for detecting faults in components, including
timing faults.
 Michael Butler, Semantics and atomicity for longrunning transactions
Longrunning transactions lack the atomicity of ACID transactions.
Instead of rollbacks and checkpoints, compensation is used to recover from
error. The development of a trace semantics has lead to a structured
design for a language of longrunning transactions and also to a rational
basis for the use of compensation in which a degree of atomicty can be
recovered.
Links:

Cliff Jones, Towards a development method, "Splitting atoms safely".
Some notes:
Wanted: a method that provides the fiction of atomicity. Can
atomicity be used in program design? Wants atomicity refinement,
especially in combination with data refinement.
Related items:
 New (and clear!) database book by Gerhard Weikum
 "Atomicity in system design and execution", Dagstuhl seminar, April 2004
 Mark Utting, ModelBased Testing
In this talk, I will describe the problems of generating good test suites
from formal specifications (pre/post style). The goal is to build a
practical tool (the LTG  Leirios Test Generator) that engineers can use to
semiautomatically generate tests from B, Z, JML, UML or Statechart
specifications.
 Bertrand Meyer, The mathematics of object computation.
 JeanRaymond Abrial, Developing discrete transition systems.
(1) Refinement of Stuttering steps: skip or keep (or both).
Stuttering steps are usually considered to be refinement of skip. In
certain cases, it is interesting however to think of them as being a
refinement of (a sort of) keep (the action that maintain the invariant).
Presentation, problems, discussion.
(2) Temporal Statements and Refinements. Is it claimed that it
is possible to completely avoid certain temporal logic statements and
replace them by refinements of stuttering steps. This raises the
problem of characterizing systems which run forever. Generalization of
"pre, post" pairs.
 Carroll Morgan, Compositionality and "pCSP".
Compositional semantics for probabilistic process algebras have been studied
for decades: one of the major problems is the interaction of the various
forms of choice: probabilistic, internal, external (to use CSP terminology).
What's the new angle?
Work with Annabelle on sequential semantics for probability and demonic
choice has given a logic which is discriminating enough in its observations
to reconstruct the operational (but sequential) program that led to the
observations. The proof of that is not trivial, and (therefore?) the
technique is not much used by other researchers. Yet.
(It is expected values, not new for IFIP2.3...)
Thus we hope it might give us some leverage on this problem. Related
issues turn out to be information hiding and (of course) simulation.
 Werner Dietl, Object Ownership  Overview and Issues
Abstract: I will motivate object ownership and show three concrete systems
that enforce it  two type systems and one dynamic solution. There
should be multiple possible discussion topics, from the basic motivation and
possible applications down to technical problems.
 Alexander Petrenko, Specification Based Testing (SBT): A Practical
Concern.
The talk will discuss different issues related to SBT technology development
and application. I will involve our case studies for KVEST, UniTesK
and OTK technologies developed and applied in several projects for Nortel
Networks, Microsoft, Intel and other customers. Main points of the
talk are as follows:
 KVEST and UniTesK technologies for test generation from contract
specifications
 Roles of models in test suite generation and multiparadigm specifications
in real life applications
 models of: requirements, faults, test coverage,
implementation architecture/structure, behavior (history, trace)
 paradigm combinations: contract specification and FSM/LTS,
 paradigm alternatives in compiler unit testing: contract
specification vs. language specification
 Highest priorities of SBT introduction in practice
 specification without specification language
 how to use formal methods without mathematic background
 SBT vs. conformance testing
 detail vs. simple models and test scenarios
 Rustan Leino, On bounded model checking, induction, and interpolants.
Many interesting statebased computer systemsboth software programs and
hardware circuitscan be represented as transition systems. An
execution of a transition system begins in some initial state and then
repeatedly applies a transition relation to obtain the next state. An
important question for such a system is whether or not it is possible for
the system to reach some given set of ``bad'' states. In this
discussion, I consider ways to determine such reachability, trying to
uniformly present previous attempts.
Slides: [PowerPoint]
[PDF]

Bertrand Meyer,
"Test Studio" from Eiffel Software / ETH.

Also present:
 Karine Arnout
 Eric Hehner
 Doug McIlroy
 Michel Sintzoff
IFIP WG 2.3 home
page