FME on Wednesday

Detailed program
Wednesday July 24th, 2002
See also the unified by-slot program

All sessions take place in auditorium 2.

All-day activities

Session 9: Invited speaker

Chair: Peter Lindsay

09:00-10:00  David Basin, U Freiburg, Germany
Invited talk: The next 700 synthesis calculi
Over the last decade I have worked with colleagues on different projects to develop, implement, and automate the use of calculi for program synthesis and transformation. These projects had different motivations and goals and differed too in the kinds of programs synthesized (e.g., functional programs, logic programs, and even circuit descriptions). However, despite their differences they were all based on three simple ideas. First, calculi can be formally derived in a rich enough logic (e.g., higher-order logic). Second, higher-order resolution is the central mechanism used to synthesize programs during proofs of their correctness. And third, synthesis proofs have a predictable form and can be partially or completely automated. In this talk I explain these ideas and illustrate the general methodology employed.

10:00-10:30  Michael Whalen, U Minnesota, USA
Johann Schumann, NASA Ames, USA
Bernd Fischer, NASA Ames, USA
Synthesizing certified code
Code certification is a lightweight approach for formally demonstrating software quality. Its basic idea is to require code producers to provide formal proofs that their code satisfies certain quality properties. These proofs serve as certificates that can be checked independently. Since code certification uses the same underlying technology as program verification, it requires detailed annotations (e.g., loop invariants) to make the proofs possible. However, manually adding annotations to the code is time-consuming and error-prone. We address this problem by combining code certification with automatic program synthesis. Given a high-level specification, our approach simultaneously generates code and all annotations required to certify the generated code. We describe a certification extension of AutoBayes, a synthesis tool for automatically generating data analysis programs. Based on built-in domain knowledge, proof annotations are added and used to generate proof obligations that are discharged by the automated theorem prover E-SETHEO. We demonstrate our approach by certifying operator- and memory-safety on a data-classification program. For this program, our approach was faster and more precise than PolySpace, a commercial static analysis tool.

Session 10: Refinement and program verification

Chair: Juan Bicarregui

11:00-11:30  Augusto Sampaio, Federal U of Pernambuco, Brazil
Jim Woodcock, U Kent-Canterbury, UK
Ana Cavalcanti, Federal U of Pernambuco, Brazil
Refinement in Circus
We describe refinement in Circus, a concurrent specification language that integrates imperative CSP, Z, and the refinement calculus. Each Circus process has a state and accompanying actions that define both the internal state transitions and the changes in control flow that occur during execution. We define the meaning of refinement of processes and their actions, and propose a sound data refinement technique for process refinement. Refinement laws for CSP and Z are directly relevant and applicable to Circus, but our focus here is on new laws for processes that integrate state and control. We give some new results about the distribution of data refinement through the combinators of CSP. We illustrate our ideas with the development of a distributed system of co-operating processes from a centralised specification.

11:30-12:00  Ana Cavalcanti, Federal U of Pernambuco, Brazil
David A. Naumann, Stevens Inst. of Techn., USA
Forward simulation for data refinement of classes
Simulation is the most widely used technique to prove data refinement. We define forward simulation for a language with recursive classes, inheritance, type casts and tests, dynamic binding, class based visibility, mutable state (without aliasing), and specification constructs from refinement calculi. It is a language based on sequential Java, but it also includes specification and design mechanisms appropriate for the construction of programs based on refinement. We show simulation to be sound for data refinement of classes in this language.

12:00-12:30  Luke Wildman, U Queensland, Australia
A formal basis for a program compilation proof tools
This paper presents a case study in verified program compilation from high-level language programs to assembler code using the Cogito formal development system. A form of window-inference based on the Z schema is used to perform the compilation. Data-refinement is used to change the representation of integer variables to assembler word locations.

Session 11: Model checking theory

Chair: Lars-Henrik Eriksson

14:00-14:30  Thomas Firley, Techn. U of Braunschweig, Germany
Ursula Goltz, Techn. U of Braunschweig, Germany
Property dependent abstraction of control structure for software verification
In this paper we present a technique to compute abstract models for formal system verification. The method reduces the state space by eliminating those parts of a system model which are not required to check a property. The abstract model depends on the property, which is a formula of the next-less fragment of CTL*. The algorithm reads a system description, annotates it with abstract sub-models for the statements, which are finally composed as abstract model for the system. In the paper we introduce the core algorithm and illustrate it by an example.

14:30-15:00  Natalia Ioustinova, CWI Amsterdam, The Netherlands
Natalia Sidorova, Eindhoven U of Techn., The Netherlands
Martin Steffen, U Kiel, Germany
Closing open SDL-systems for model checking with DTSpin
Model checkers like Spin can handle closed reactive systems, only. Thus to handle open systems, in particular when using assume-guarantee reasoning, we need to be able to close (sub-)systems, which is commonly done by adding an environment process. For models with asynchronous message-passing communication, however, modelling the environment as separate process will lead to a combinatorial explosion caused by all combinations of messages in the input queues. In this paper we describe the implementation of a tool which automatically closes DTPromela translations of SDL-specifications by embedding the timed chaotic environment into the system. To corroborate the usefulness of our approach, we compare the state space of models closed by embedding chaos with the state space of the same models closed with chaos as external environment process on some simple models and on a case study from a wireless ATM medium-access protocol.

15:00-15:30  Lars Michael Kristensen, U South Australia, Australia
Thomas Mailund, U Aarhus, Denmark
A generalised sweep-line method for safety properties
The recently developed sweep-line method exploits progress present in many concurrent systems to explore the full state space of the system while storing only small fragments of the state space in memory at a time. A disadvantage of the sweep-line method is that it relies on a strict and global notion of progress. This prevents the method from being used for many reactive systems. In this paper we generalise the sweep-line method such that it can be used for verifying safety properties of reactive systems exhibiting local progress. The basic idea is to relax the strict notion of progress and to recognise the situations where this could cause the state space exploration not to terminate. The generalised sweep-line method explores all reachable states of the system, but may explore a state several times. We demonstrate the practical application of the generalised sweep-line method on two case studies demonstrating a reduction in peak memory usage to typically 10 % compared to the use of ordinary full state spaces.

Session 12: Combining methods

Chair: Jim Woodcock

16:00-16:30  Helen Treharne, Royal Holloway, U London, UK
Supplementing a UML development process with B
This paper discusses our experiences of using UML and B together through an illustrative case study. Our approach to using UML and B centers around stereotyping UML classes in order to identify which classes should be modelled in B. We discuss the tensions between the notations, and the compromises that need to be reached in order for B to supplement a UML development. The case study begins from the initial conception of a library system and its use case view in order to demonstrate how the classes were identified.

16:30-17:00  Jin Song Dong, National U of Singapore
Jing Sun, National U of Singapore
Hai Wang, National U of Singapore
Semantic web for extending and linking formalisms
The diversity of various formal specification techniques and the need for their effective combinations requires an extensible and integrated supporting environment. The Web provides infrastructure for such an environment for formal specification and design because it allows sharing of various design models and provides hyper textual links among the models. Recently the Semantic Web Activity proposed the idea of having data on the web defined and linked in a way that it can be used for automation, extension and integration. The success of the Semantic Web may have profound impact on the web environment for formal specifications, especially for extending and integrating different formalisms. This paper demonstrates how RDF and DAML can be used to build a Semantic Web environment for supporting, extending and integrating various formal specification languages. Furthermore, the paper illustrates how RDF query techniques can facilitate specification comprehension.

17:00-17:30  Takaaki Umedu, Osaka U, Japan
Yoshiki Terashima, Osaka U, Japan
Keiichi Yasumoto, Nara Inst. of Science and Techn., Japan
Akio Nakata, Osaka U, Japan
Teruo Higashino, Osaka U, Japan
Kenichi Taniguchi, Osaka U, Japan
A language for describing wireless mobile applications with dynamic establishment of multi-way synchronization channels
In this paper, we define a new language called LOTOS/M which enables dynamic establishment of multi-way synchronization channels among multiple agents (processes running on mobile hosts) on ad hoc networks, and show how it can be applied to designing wireless mobile applications. In LOTOS/M, a system specification is given by a set of independent agents. When a pair of agents is in a state capable of communicating with each other, a synchronization relation on a given gate (channel) list can dynamically be assigned to them by a new facility of LOTOS/M: (i) advertisement for a synchronization peer on a gate list and (ii) participation in the advertised synchronization. The synchronization relation on the same gate list can also be assigned to multiple agents to establish a multi-way synchronization channel incrementally so that the agents can exchange data through the channel. When an agent goes in a state incapable of communication, a synchronization relation assigned to the agent is canceled and it can run independently of the others. By describing some examples, we have confirmed that typical wireless mobile systems can easily be specified in LOTOS/M, and that they can be implemented efficiently with our LOTOS/M to Java compiler.

17:30-19:00  FME business meeting