IFIP WG 2.3 meeting 43

Logistics

Where:  Prato, Italy
When:  6-10 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 GC-6 on "Dependable Systems Evolution", accepted by UKCRC]"
   
Discussion of the Grand Challenge of a Verifying Compiler (or, a Verifying Development Environment)
 
• Gary Leavens, Alias-Free 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.  Whole-program static analysis could provide knowledge about such aliasing, but it is non-modular, 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 run-time 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 CCR-9803843, CCR-0097907, CCR-0113181, CCF-0428078, and CCF-0429567.
   
• Peter Müller, Modular verification of object and module invariants
  (joint work with Rustan Leino)
  
  The talk describes a methodology for specifying and verifying object-oriented 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 two-player parity games
  
  In this talk I will discuss the problem of finding optimal strategies for two-player games.
  
  Game models of programs can be useful in the specification and analysis of temporal-style 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 parity-game 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 non-pure strategies are an acceptable solution.
   
• Michael Jackson, The problem of the banker with 52 cards.
  
  A “banker” has an ordinary 52-card 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 long-running transactions
  
  Long-running 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 long-running transactions and also to a rational basis for the use of compensation in which a degree of atomicty can be recovered.
  
  Links:
  • Free distribution of B system
  • The ProB Animator and Model Checker for the B Method
   
• 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, Model-Based 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 semi-automatically generate tests from B, Z, JML, UML or Statechart specifications.
   
• Bertrand Meyer, The mathematics of object computation.
   
• Jean-Raymond 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
      • learning and management
    • SBT vs. conformance testing
    • detail vs. simple models and test scenarios
   
• Rustan Leino, On bounded model checking, induction, and interpolants.
  
  Many interesting state-based computer systems--both software programs and hardware circuits--can 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