Roadmap - Discussion

Two time slots are reserved for an interactive development of a so-called Roadmap for Formal Methods . Starting with an assessment of the current situtation we will try to identify intermediate goals (with respect to formal methodology, tool support, integration into software life cycle, etc.) in order to obtain industrial strength formal methods and a routine application in the software engineering process. As a concrete result of this discussion we strive for a roadmap that fixes the most important aims together with the technology necessary to achieve them on a time scale. Participants are encouraged to prepare and present their personal visions for the next ten years.

 

Goerigk/Hoffmann - Rigorous Compiler Implementation Correctness: How to Prove the Real Thing Correct

We give a comprehensive technical overview of our work on rigorous verification of compiling specification and compiler implementation of an initial correct binary compiler executable. We will concentrate on implementation verification. Machine program correctness is proved by a special bootstrapping technique with \`a posteriori code inspection. Our contribution is to perform this work for compilers and, hence, to relieve the application programmer's burden to prove implementation correctness again and again, as this is done today for safety and security critical applications. Once our work has been finished conscientiously and is accepted to reach sufficient mathematical certainty, compilers may be used for proved correct program implementation, safely in the sense that every result a target program execution returns is guaranteed to be correct with respect to the source program semantics.

 

Bertoli/Cimatti/Giunchiglia/Traverso - A Structured Approach to the Formal Certification of Safety for Computer

Safety-critical systems are often designed using development support tools which perform translations of high-level specifications into lower-level counterparts. The correctness of the translation is critical to the safety of the resulting systems. However, using non failure-safe components in the implementation of translators is desirable because of the extremely high cost of certified components. In order to ensure the correct behavior of development tools, we adopt a solution based on the idea of verifying each of their executions. In order to perform the verification in an automatic and efficient way, we follow an innovative approach, by distinguishing an off-line and an on-line verification phases. Each proof in the two phases is guaranteed correct by designing the certifying tools according to a logging-and-checking architecture. We describe in detail the off-line and on-line logging-and-checking methodology, its application in the frame of an industrial project, and the ongoing logging-and-checking redesign of a state-of-the-art prover which we intend to use in future applications.

 

Bogdanov/Holcombe/Singh - Automated Test Set Generation for Statecharts

In this paper we present the application of the formal testing method to the statechart notation. The method is proposed for deriving test sets for complex statecharts, i.e.\ containing hierarchy and concurrency, using a `divide and conquer' strategy. Initially, test cases are generated for simple statecharts and then these test cases are `merged' to derive test cases for complex statecharts. They are then populated with test data. Methods for generating test cases for simple statecharts and for `merging' of such test cases, are described using a simple example. The blackbox test method presented is easy to automate.

 

Buessow/Grieskamp/Heicking/Herrmann - An Open Environment for the Integration of Heterogeneous Modelling Techniques and Tools

Even though the development of formal methods makes steady progress with respect to techniques and tool support, their acceptance in industry is still relatively low. One reason for this probably stems from the fact that most formal approaches require users to forget about their conventional techniques and tools, and to relearn in a new environment. What makes this switch even harder to accept: due to their research character, tools for formal methods can usually not compete w.r.t. convenience, stability, and degree of integration to conventional, state-of-the-art commercial tools. Applying modern repository-based integration techniques to tools for formal methods can overcome some of these drawbacks. Yet, a full close of the gap of comfortability to commercial tools can naturally not be achieved in the research context in which tools for formal methods and their integration platforms are usually built. Moreover, an incremental migration, in which users can continue to apply their established conventional techniques and tools, adding formal support in degrees as desired, seems to be promising for bringing formal methods to practice. A framework based on the idea of combining established modeling techniques and tools with formal ones has been developed in the context of the project: among others, Statecharts {SC:Harel87}, a widely used graphical notation for reactive behavior, are combined with the formal notation Z {Z:Spiv92}, and with temporal logic {BG97,BGG+97}. The resulting combined notation is supported by a specification methodology {GHD98} and, last but not least, by an open and scalable tool integration environment -- the design principles of which will be sketched in this paper.

 

Geser/Kuechlin - Structured Formal Verification of a Fragement of the IBM/390 Clock Chip

We present a simple and powerful method for formal verification of hardware that exploits hardware symmetries. We illustrate the method at an industrial example: a fragment of the IBM S/390 Clock Chip.

 

Goldsmith/Zakiuddin - Critical Systems Validation and Verification with CSP and FDR

Formal Systems and DERA have enjoyed a number of fruitful collaborations in recent years, especially in projects exploiting the FDR tool to analyse CSP models of systems. This paper presents an overview of the approach and some of the diverse applications to which it has been applied.

 

Karlsen - The UniForM Work Bench - a Higher Order Tool Integration Framework

The UniForM WorkBench is an open ended tool integration framework for developing (formal) Software Development Environments (SDE) from the basis of pre-fabricated off-the-shelf development tools. The integration framework provides support for data, control and presentation integration as well as utilities for wrapping Haskell interfaces around existing development tools. Entire SDE's are then glued together on the basis of these encapsulations using Concurrent Haskell as the integration language, thus allowing integration to be done at a level of abstraction that is very close to the one offered by constructive formal specifications. So far, the integration framework has successfully been used to integrate tools for Haskell program development as well as specification and proof tools for Z specifications.

 

KIV

KIV 3.0 is an advanced tool for engineering high assurance systems. It provides an economically applicable verification technology, and supports the entire design process from formal specifications to executable verified code.

 

Krieg-Brueckner - UniForM Perspectives for Formal Methods

Trends for formal methods are reviewed and illustrated by several industrial applications: logical foundations of combination, testing, verification and transformation, and tool support. The UniForM Workbench is the background for highlighting experiences made over the past 20 years.Introduction This paper outlines some state of the art technology in Formal Methods and attempts to extrapolate towards the next century. The UniForM Workbench (Universal Formal Methods Workbench, cf. "BKBetal96" Krieg-Brückner et al. 1996) is developed by the Universities of Bremen and Oldenburg, and Elpro, Berlin, funded by the German Ministry for Education and Research, BMBF. In its present state, it provides a focal point to review experiences in the past decades developing languages, methods and tools, give an illustrative example of state of the art technology, evaluate preliminary experiences with industrial applications, and assess the industrial potential for the future and illuminate technological trends.

 

Kutter/Schweizer/Thiele - Integrating Formal Domain Specific Language Design in the Software Life Cycle

Domain Specific Languages help to split the software live cycle in different independent cycles. While the use of the newly created language is just an additional tool in the established cycle, the language live cycle is independent and opens the doors for the application of formal methods. We report on an industrial case study, where a driver specification language has been designed, formally specified, and finally an implementation has been generated from the specification. Using Abstract State Machines and Montages for the language specification, it was possible that the industrial partners learned how to maintain and extend the language specification. On the other hand the formal semantics of the method allows to apply different verification-oriented methods to the artifacts.

 

Margaria/Gruhn - Flexible and Reliable Process Model Properties An Integrated Approach

In this article we describe an integrated approach to process management based on the widely used LEU toolset for process modelling and workflow management and on the ABC tools for formal verification of process model properties. We show how process modelling and process model analysis benefit from this integration by gaining a fully automatic global property check capability. We illustrate the approach by means of a process model example taken from an industrial project.

 

Puitg/Dufourd - Formal Program Development in Geometric Modelling

An innovative attempt to integrate formal program development in geometric modeling is reported through the axiomatization of model of the combinatorial maps in the Calculus of Inductive Constructions. A hierarchical specification of ordered sorts is validated in the Coq prover by inductive proofs, and the automatic extraction of a prototype. Classical difficulties - like cohabitation of hierarchized objects, smooth handling of subtyping, and completion of partial relations - are addressed both from theorem proving and prototyping viewpoint.

 

Siegel

Translation validation is an alternative to the verification of translators (compilers, code generators). Rather than proving in advance that the compiler always produces a target code which correctly implements the source code (compiler verification), each individual translation (i.e. a run of the compiler) is followed by a validation phase which verifies that the target code produced on this run correctly implements the submitted source program. In order to be a practical alternative to compiler verification, a key feature of this validation is its full automation. In this paper we demonstrate the feasibility of translation validation for industrial code generators from \dcplus\ - a widely used intermediate format for synchronous languages - to C. We explain the compilation pattern from \dcplus\ to C and advocate new abstraction techniques for a fragment of first order logic as part of the automation of our approach.

 

Woodcock

A theorem-proving system derived from Higher Order Logic (HOL) is described. The system is designed to support the verification of code written in its own implementation language (SML/NJ), and to allow code which is proven to preserve equality of hol\_terms to be used to extend the system. The extension is shown to be theoretically conservative, and the implementation to be reliable. It is hoped that significant efficiency gains can be realized employing this technique (Computational Reflection).

 

Yamane - A Practical Hierarchical Design by Timed Simulation Relations for Real-Time Systems

As many processes concurrently behave and timing constraints are strict in real-time systems, it is difficult to design real-time systems. For this reason, a hierarchical design method is useful. In the hierarchical design method, it is important to verify whether the low level specification satisfies the high level specification or not. In general, the language inclusion verification method is useful for verifying it. But, as nondeterministic timed automata are not closed under complementation, it is impossible to use the language inclusion verification method. In this paper, we propose the hierarchical design method based on timed simulation method. Especially, we generalize existing timed simulation methods and propose a $safety$ timed simulation relation and a $\exists$-liveness timed simulation relation, a $\forall$-liveness timed simulation relation. Finally, we show our proposed method effective by some example.

 

Agerholm/Larsen - A Lightweight Approach to Formal Methods

The main current trend in applied formal methods can be characterized by the term "lightweight". Historically, formal methods have been viewed as pure alternatives to traditional development methodologies, demanding a revolutionary change in industry to adopt them. With a pragmatic, lightweight approach, the use of formal methods is complementing and improving existing development practices ina company in an evolutionary way, demonstrating more clearly the cost-effictiveness of formal methods. This paper presents our view on lightweight formal methods as a strategy for successful formal methods technology transfer to indusrty.

 

Agerholm - Tools

IFAD is the world-leading formal methods technology provider for high-quality software. With distinguishing features for system modeling and early validation, our professional software development environment, called VDMTools(r), assist developers in clarifying requirements and obtaining early confidence in system designs. Our quality products support object-oriented formal specification in VDM++ and provide links to leading third-party tools for graphical modeling in UML, including Rational Rose.

 

Broy - Enriching the Software Develpoment Process by Formal Methods

We discribe a software develpoment process designed for an integration and usage of formal methods into practical software process models in a scalable way. Our process model is an extension of the V-model, and allows the specification of critical components and the verification of crucial development steps. For different development stages we suggest user-oriented description techniques, based on common formal semantic. Furthermore we outline methods for the verification of critical development steps. We illustrate our process by developing a small example with some critical aspects.

 

Fujita - Two real formal verification experiences: ATM switch chip and parallel cache protocol

In this paper, we report two of our recent efforts in applying formal verification methods to our real hardware designs. The first one is to try to verify ATM switch LSI chips through the combined ues of a theorem prover and model checking programs, and the second one is to try to formally verify the correctness of a cache coherency protocol used in one of our parallel PC servers by model checking programs. In both cases, the verifications themselves were successfull (we could really verify the "abstracted/simplifed" designs). We could not, however, get much benefits from formal methods, since the verification process was not automatic but interactive. We had to spend significant amount of human time and human efforts in applying formal verification techniques, which made it very difficult to verify designs "in time", that is, before the design process finishes. We review our experiences and describe problems that we typically encounter in application of formal verification techniques to real life designs.

 

Fantechi/Gnesi/Mazzanti/Pugliese/Tronci - A Symbolic Model Checker for ACTL

We present SAM, a symbolic model checker for ACTL, the action-based version of CTL. SAM relies on implicit representations of Labeled Transition Systems (LTSs), the semantic domain for ACTL formulas, and uses symbolic manipulation algorithms. SAM has been realized by translating (networks of) LTSs and, prossibly recursive, ACTL formulas into BSP (Boolean Symbolic Programming), a programming language aiming at defining computations of boolean funcions, and by using BSP interpreter to carry out computations (i.e. verifications).

 

Souza et al.

Design of Distributed Multimedia Applications (DAMD) is a multi-institutional cooperative project aiming the development of a methodology, based on the Formal Descrition Technique (FDT) Enhancements to Language of Temporal Ordering Specification (E-LOTOTS) and supported by a set of appropriate tools, for the specification, validation, implementation, and testing of distributed multimedia applications. This paper presents the main result of this project.

 

van der Meulen/Bloomfield/Clement - The application of formal methods in the specification of the emergency closing system of the storm surge barrier in the Eastern Scheldt.

 

Boerger The Abstract State Machines Method for the Design and Analysis of Complex Computing Systems

The huge gap between much of academic theory and the prevailing software and hardware practice is still with us, as is a wide-spread scepticism about the industrial benefit of formal methods. In this talk I will present the ASM approach to software and hardware design and analysis which contributes to bridging this gap. I will explain that it offers a mathematically well founded and rigorous but nevertheless simple discipline practical and scalable to industrial applications. I will present the salient features of this method and illustrate them through several examples from my work on specification and verification of programming languages, compilers, protocols and architectures. In particular I will show that by building appropriate ASMs for Java and the Java Virtual Machine, one can prove the correctness of a general compilation scheme of Java programs to JVM code. I will also point out the realistic potential of the ASM method for large-scale industrial applications.

 

Büttner - Proving instead of Hoping - Why you cannot Afford to Ignore Formal Verification

 

ClarkeModel Checking and the Verification of Finite State Reactive Systems

Logical errors in finite state reactive systems are an important problem for designers. They can delay getting a new product on the market or cause the failure of some critical device that is already in use. My research group has developed a verification method called temporal logic model checking for this class of systems. In this approach specifications are expressed in a propositional temporal logic, and reactive systems are modeled as state-transition graphs. An efficient search procedure is used to determine automatically if the specifications are satisfied by the state-transition graph. The technique has been used in the past to find subtle errors in a number of non-trivial circuit and protocol designs. During the last few years, the size of the reactive systems that can be verified by model checking techniques has increased dramatically. By representing sets of states and transition relations implicitly using Binary Decision Diagrams (BDDs), we are now able to check examples that are many orders of magnitude larger than was previously the case. In this lecture we describe how the BDD-based model checking techniques work and illustrate their power with a number of complex examples. the shuttle has to abort its flight during take-off.

 

Ullman,Meister - title to be announced

Content: formal modeling of the application of digital signatures based on smartcards

 

Wilikens - title to be announced

Content: European Dependability Initiative  
as part of the Information Society Technologies Programme within the EC's RTD Framework 5 (1998 - 2002)