J.UCS Special Issue on Tools for System Design and
Verification - Part 1
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 two special issues presented here are a selection of
articles presented at the "Workshop on Tools for System Design
and Verification" (FM-TOOLs 2000).
The workshop was the fourth in a series of biennial events devoted
to this topic. The first three workshops were held in in Kiel (1994),
Bremen (1996) and Malente (1998), Germany. The workshop took place at
the beautiful 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.
29 talks based on abstracts of 5 pages were presented at the
workshop. After the workshop, authors were invited to submit full
papers. 22 submissions were reviewed by the program committee. 12 were
selected to be published in the two special issues.
In the first of the two special issues the reader will find papers,
which give full system descriptions of a variety of tools. The second
special issue contains papers, which describe extensions of approaches
to tool support, new theory and applications.
The first three papers focus on support for specification
languages. Deduction capabilities are implemented by connecting
interactive and automatic verification tools. "DisCo Toolset - The New
Generation" (by Aaltonen, Katara and Pitkaenen) implements a
method to specify reactive and distributed systems. "The Korrigan
Environment" (by Choppy, Poizat and Royer) allows
specification of systems with both static and dynamic aspects, and
"An Open
Software Architecture for the Verification of Industrial
Controllers" (by Treseler, Stursberg, Chung and Yang)
describes VERDICT.
The systems of the other three papers of the first special issue
focus on deduction: In "Program Generation via Declarative Term
Graph Attribution", Derichsweiler and Kahl explain the program
transformation system HOPS.
Crossley and Poernomo describe "Fred: An Approach to
generating Real, Correct, Reusable Programs from Proofs", and
in "RAVEN: Real-Time
Analyzing and Verification Environment", Ruf gives a model
checking system based on timed automata.
The first two papers of the second special issue describe advances
to existing approaches using formal methods. In "Modelling
Sequences within the REL VIEW System" Berghammer and Hoffmann
extend a system based on relational algebra, and "A Practical
Extension Mechanism for Decision Procedures: the Case Study of
Universal Presbuger Arithmetic" is discussed by Armando and
Ranise.
Both "Verification of Parameterized Protocols" (by
Baukus, Lakhnech and Stahl) and "Refining Predicate Diagrams for
Designing Reactive Systems" (by Cansell, Mery, and Merz) give
approaches that reduce classes of infinite systems to finite systems,
which can be automatically verified by model checking.
A new, powerful specification language is given by Rothe, Tews and
Jacobs in "The Coalgebraic Class Specification Language
CCSL", and finally, "Correctness of Efficient Real-Time
Model checking" (by Reif, Schellhorn, Vollmer and Ruf) discusses
an application of interactive theorem proving (KIV) to verify the
kernel algorithm of RAVEN (that was described in the first special
issue).
To conclude, 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, January 2001
Wolfgang Reif and Gerhard Schellhorn
Program committee
Chair:
Wolfgang Reif (U Augsburg, FRG)
Rudolf Berghammer (U Kiel, FRG)
Nikolaj Bjørner (Kestrel, USA)
John Harrison (Intel, USA)
Jozef Hoomann (U Nijmegen, NL)
Hélène Kirchner (LORIA, Fr)
Tobias Nipkow (TU München, FRG)
Jan Peleska (U Bremen, FRG)
Joseph Sifakis (Verimag, Fr)
Martin Wirsing (U München, FRG)
|