J.UCS Special Issue on Tools for System Design and Verification
Rudolf Berghammer (University of Kiel, Germany)
rub@informatik.uni-kiel.de
Dominik Haneberg (University of Augsburg, Germany)
haneberg@informatik.uni-augsburg.de
Wolfgang Reif (University of Augsburg, Germany)
reif@informatik.uni-augsburg.de
Gerhard Schellhorn (University of Augsburg, Germany)
schellhorn@informatik.uni-augsburg.de
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"
(FMTOOLS 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.
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
Chairs:
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)
|
