FME on Tuesday

Detailed program
Tuesday July 23rd, 2002
See also the unified by-slot program

Sessions take place in auditorium 2 unless otherwise indicated.

All-day activities

Session 5: Invited speaker

Chair: Lars-Henrik Eriksson

09:00-10:00  Anthony Hall, Praxis Critical Systems, UK
Invited talk: Correctness by construction: Integrating formality into a commercial development process
This paper describes a successful project where we used formal methods as an integral part of the development process for a system intended to meet ITSEC E6 requirements. The system runs on commercially available hardware and uses common COTS software. We found that using formal methods in this way gave benefits in accuracy and testability of the software, reduced the number of errors in the delivered product and was a cost-effective way of developing high integrity software. Our experience contradicts the belief that formal methods are impractical, or that they should be treated as an overhead activity, outside the main stream of development. The paper explains how formal methods were used and what their benefits were. It shows how formality was integrated into the process. It discusses the use of different formal techniques appropriate for different aspects of the design and the integration of formal with non-formal methods.

10:00-10:30  Darko Marinov, Massachusetts Inst. of Techn., USA
Sarfraz Khurshid, Massachusetts Inst. of Techn., USA
VAlloy - virtual functions meet a relational language
We propose VAlloy, a veneer onto the first order, relational language Alloy. Alloy is suitable for modeling structural properties of object-oriented software. However, Alloy lacks support for dynamic dispatch, i.e., function invocation based on actual parameter types. VAlloy introduces virtual functions in Alloy, which enables intuitive modeling of inheritance. Models in VAlloy are automatically translated into Alloy and can be automatically checked using the existing Alloy Analyzer. We illustrate the use of VAlloy by modeling object equality, such as in Java. We also give specifications for a part of the Java Collections Framework.

Session 6: Smart cards

Chair: Yves Ledru

11:00-11:30  Vlad Rusu, IRISA Rennes, France
Verification using test generation techniques
Applying formal methods to testing has recently become a popular research topic. In this paper we explore the opposite approach, namely, applying testing techniques to formal verification. The idea is to use symbolic test generation to extract subgraphs (called components) from a specification and to perform the verification on the components rather than on the whole system. This may considerably reduce the verification effort and, under reasonable sufficient conditions, a safety property verified on a component also holds on the whole specification. We demonstrate the approach by verifying an electronic purse system using our symbolic test generation tool STG and the PVS theorem prover.

11:30-12:00  Néstor Cataño, INRIA Sophia-Antipolis, France
Marieke Huisman, INRIA Sophia-Antipolis, France
Formal specification and static checking of Gemplus' electronic purse using ESC/Java
This paper presents a case study in formal specification of smart card programs, using ESC/Java. It discusses an electronic purse application, provided by Gemplus, that we have annotated with functional specifications (i.e., pre- and post-conditions, modifies clauses and class invariants) that are as detailed as possible. The specification is based on the informal documentation of the application. Using ESC/Java, the implementation has been checked with respect to the specification. This revealed several errors or possibilities for improvement in the source code (such as removing unnecessary tests). Our paper shows that a relatively lightweight use of formal specification techniques can already have a serious impact on the quality of a program and its documentation. Furthermore, we also present some ideas on how ESC/Java could be further improved, both with respect to specification and verification.

12:00-12:30  Ludovic Casset, Gemplus Research Laboratory, France
Development of an embedded verifier for Java Card byte code using formal methods
The Java security policy is implemented using security components such as a Java Virtual Machine (JVM), API, verifier, and a loader. It is of prime importance to ensure that these components are implemented in accordance with their specifications. Formal methods can be used to bring the mathematical proof that their implementation corresponds to their specification. In this paper, we introduce the formal development of a complete byte code verifier for Java Card and its on-card integration. In particular, we aim to focus on the model and the proof of the complete type verifier for the Java Card language. The global architecture of the verification process implemented in real industrial case study is described and the detailed specification of the type verifier is discusses as well as its proof. Moreover, this paper presents a comparison between formal and traditional development, summing up the pros and cons of using formal methods in industry.

Session 7: Refinement and proof

Chair: Tobias Nipkow

14:00-14:30  Michael Backes, Saarland U, Germany
Christian Jacobi, Saarland U, Germany
Birgit Pfitzmann, IBM Zürich, Switzerland
Deriving cryptographically sound implementations using composition and formally verified bisimulation
We consider abstract specifications of cryptographic protocols which are both suitable for formal verification and maintain a sound cryptographic semantics. In this paper, we present the first abstract specification for ordered secure message transmission in reactive systems based on the recently published model of Pfitzmann and Waidner. We use their composition theorem to derive a possible implementation whose correctness additionally involves a classical bisimulation, which we formally verify using the theorem prover PVS. The example serves as the first important case study which shows that this approach is applicable in practice, and it is the first example that combines tool-supported formal proof techniques with the rigorous proofs of cryptography.

14:30-15:00  Claus Pahl, Dublin City U, Ireland
Interference analysis for dependable systems using refinement and abstraction
A common requirement for modern distributed and reactive systems is a high dependability guaranteeing reliability and security. The rigorous analysis of dependable systems specifications is of paramount importance for the reliability and security of these systems. A two-layered modal specification notation will allow the specification of services and protocols for distributed dependable systems and their properties. Refinement and its dual - abstraction - will play the key roles in an integrated development and analysis framework. Refinement and abstraction form the basis for an interference analysis method for security properties and for automated test case generation.

15:00-15:30  Neil Henderson, U Newcastle upon Tyne, UK
Stephen Paynter, MBDA Ltd, UK
The formal classification and verification of Simpson's 4-slot asynchronous communication mechanism
This paper critiques and extends Lamport's taxonomy of asynchronous registers. This extended taxonomy is used to characterise Simpson's 4-slot asynchronous communication mechanism (ACM). A formalisation of the Lamport atomic property and Simpson's original 4-slot implementation is given in the PVS logic. We prove that the 4-slot is atomic using Nipkow's retrieve relation proof rules. A description is given of the formal proofs, which have been discharged in the PVS theorem prover.

Session 8: Real-time and performance

Chair: Nico Plat

16:00-16:30  C. J. Fidge, U Queensland, Australia
Timing analysis of assembler code control-flow paths
Timing analysis of assembler code is essential to achieve the strongest possible guarantee of correctness for safety-critical, real-time software. Previous work has shown how timing constraints on control-flow paths through high-level language programs can be formalised using the semantics of the statements comprising the path. We extend these results to assembler-level code where it becomes possible to not only determine timing constraints, but also to verify them against the known execution times for each instruction. A minimal formal model is developed with both a weakest liberal precondition and a strongest postcondition semantics. However, despite the formalism's simplicity, it is shown that complex timing behaviour associated with instruction pipelining and iterative code can be modelled accurately.

16:30-17:00  María Victoria Cengarle, Techn. U of Munich, Germany
Alexander Knapp, U Munich, Germany
Towards OCL/RT
An extension of the "Object Constraint Language" (OCL) for modeling real-time and reactive systems in the "Unified Modeling Language" (UML) is proposed, called OCL/RT. A general notion of events that may carry time stamps is introduced providing means to describe the detailed dynamic and timing behaviour of UML software models. OCL is enriched by satisfaction operators @η for referring to the value in the history of an expression at the instant when an event η occurred, as well as the modalities always and sometime. The approach is illustrated by several examples. Finally, an operational semantics of OCL/RT is given.

17:00-17:30  Hubert Garavel, INRIA Rhône-Alpes, France
Holger Hermanns, U Twente, The Netherlands
On combining functional verification and performance evaluation using CADP
Considering functional correctness and performance evaluation in a common framework is desirable, both for scientific and economic reasons. In this paper, we describe how the CADP toolbox, originally designed for verifying the functional correctness of LOTOS specifications, can also be used for performance evaluation. We illustrate the proposed approach by the performance study of the SCSI-2 bus arbitration protocol.

Conference dinner

Joint with LICS, RTA
Room: Restaurant Luftkastellet

19:30-21:30  Banquet

21:30-22:30  Martin Davis, U California-Berkeley, USA
Plenary talk: Alan Turing & the advent of the computer