Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 9 / Issue 2

available in:   PDF (37 kB) PS (45 kB)
Similar Docs BibTeX   Write a comment
Links into Future


J.UCS Special Issue on Tools for System Design and Verification

Rudolf Berghammer (University of Kiel, Germany)

Dominik Haneberg (University of Augsburg, Germany)

Wolfgang Reif (University of Augsburg, Germany)

Gerhard Schellhorn (University of Augsburg, Germany)

Abstract: There is a growing awareness that tool support is needed to develop high-assurance industry-size software/hardware systems. The work contained in this special issue is a selection of articles presented at the "Workshop on Tools for System Design and Verification" (FM­TOOLS 2002).

The workshop was the fifth in a series of biennial events devoted to this topic. The first four workshops were held in Kiel (1994), Bremen (1996), Malente (1998) and Reisensburg (2000). This year's workshop was held again at Reisensburg castle located between Ulm and Munich in Southern Germany.

The aim of the workshop was to provide a forum for researchers interested in the use and development of tools which support the use of mathematical techniques for the specification, development, analysis and verification of systems. The focus was on papers which deal with all topics relevant for developers or users of tools that support formal modeling and verification of hardware/software systems. In particular, papers on support for specification languages, interactive and automated verification, system analysis and validation, comparison of tools, combinations of tools and techniques, customizing tools for particular applications, and applications of formal methods were invited.

16 talks based on abstracts of 5 pages were presented at the workshop. After the workshop, authors were invited to submit full papers. 12 submissions were reviewed by the program committee. 6 were selected to be published in this special issue. Here is an overview of the 6 selected contributions:

"Moby/RT: A Tool for Specification and Verification of Real-Time Systems", written by Ernst-Rüdiger Olderog and Henning Dierks, describes the specification of requirements by constraint diagrams over duration calculus, system design with PLC-automata and the theoretical basis that allows to use model checkers for proving correctness.

In "Checking Object System Designs Incrementally", Hans-Dieter Ehrich, Maik Kollmann and Ralf Pinger give a method that allows to apply model checking to distributed object systems.

Page 86

Given suitable restrictions on the communication of the objects the method allows to break down global conditions to local ones, avoiding the state explosion problem.

The paper "Optimized Temporal Logic Compilation" by Andreas Krebs and Jürgen Ruf presents a technique to verify temporal properties during simulation. The technique can be used in the design of software as well as hardware systems.

In their work "A Case Study in Verification of UML Statecharts: the PROFI-safe Protocol" Robi Malik and Reinhard Mühlfeld illustrate a case study that applies model checking to check important features of the PROFIsafe bus protocol.

"HOLZ 2.0: A Proof Environment for Z-Specifications", written by Achim D. Brucker, Frank Rittinger and Burkhart Wolff, describes an embedding of the Z specification language in the higher-order logic of the interactive theorem prover Isabelle.

The paper "Tool Support for the Interactive Derivation of Formally Correct Functional Programs" outlines the ULTRA system, a tool that supports the transformational derivation of correct functional programs from specifications. It is written by Walter Guttmann, Helmuth Partsch, Wolfram Schulte and Ton Vullinghs.

The editors would like to thank the members of the program committee and all the referees for their care and time in reviewing and selecting the submitted papers.

Augsburg, February 2003

Rudolf Berghammer
Dominik Haneberg
Wolfgang Reif
Gerhard Schellhorn

Program committee

Rudolf Berghammer (Univ. Kiel, FRG)
Wolfgang Reif (Univ. Augsburg, FRG)

David Basin (Univ. Freiburg, FRG)
Jozef Hooman (Univ. Nijmegen, NL)
Yassine Lakhnech (VERIMAG, Grenoble, FR)
Rym Mili (Univ. Texas, Dallas, USA)
Tobias Nipkow (TU München, FRG)
Martin Wirsing (Univ. München, FRG)

Page 87