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

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


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

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 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.

Page 1

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

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)

Page 2