Formal Methods Europe Symposium 1997

Tool Demonstrations

During the Symposium there will be various tool demonstrations and demo sessions. The tool demonstrations listed in this Call for Participation have been fixed until the deadline for printing. The list will be updated as further tool demonstrators suggest to attend FME'97 and printed in the final program.

• Thierry Servat, Clement Roches, Steria Mediterranee, France:
  AtelierB demonstration
  AtelierB is a set of tools to help the designer formalize his application. It enables him to concentrate entirely on writing his software specifications and their refinements by releaving him of all automatable tasks. AtelierB is an industrial tool, used in important operational projects. It was developed and validated using industrial facilities to reach the high level of confidence necessary.

• E. Trichina, J. Oinonen, Advanced Computing Research Center, University of South Australia, Australia:
  3D Visual Tool Supporting Derivation of Operational Specification for Parallel Programs
  Parallel program design and analysis is a complex activity, where many difficulties stem from the principle inadequacy of pure textual formalism to specify parallelism in an understandable fashion. In this tooldemonstration there will be reported on a visual system, which uses a three-dimensional model to describe the data dependencies in the computational domain and to visualize transformations of this domain relevant to the main steps in parallel program design.

• Christoph Lueth, Bremen Institute for Safe Systems, University of Bremen, Germany:
  TAS and IsaWin: Generic Interfaces for Transformational Program Development and Theorem Proving
  There will be a presentation of two tools, TAS and IsaWin, for transformational program development and theorem proving respectively, based on the theorem prover Isabelle. Their distinguishing feature is a generic, open system design which allows the development of a family of tools for different formal methods on a sound logical basis with a uniform appearance. The context of this work is the UniForM project, the aim of which is to develop a framework integrating different formal methods in a logically consistent way. Consistency is achieved by encoding formal methods such as CSP and Z in the theorem prover Isabelle, which is used to perform the program development as well as to prove the correctness of the transformation rules.

• Jan Storbank Pedersen, Computer Resources International A/S, Denmark:
  RAISE Tool Demonstration
  The RAISE tools are a fully integrated tool set supporting rigorous development of large software systems. Based on the interactive structure editing of RSL modules, theories, development relations and justifications (proofs), with additional tools for pretty-printing and translation to Ada and C++.

• Peter Gorm Larson, Institute for Applied Computer Science (IFAD), Denmark:
  VDM Technology
  The services and tools supporting the ISO VDM-SL standard and the object oriented VDM++ notation are commonly known as the VDM Technology. For both notations consultancy, training and industrially applicable tools are supplied by IFAD. Users of this technology often report about their applications in the Toolbox Newsletter which is issued on a regular basis. This demonstration provides an introduction to these tools: The IFAD VDM-SL Toolbox, the VDM-SL to C++ Code Generator, the Dynamic Link facility, The IFAD VDM++ Toolbox, the VDM++ to C++ Code Generator and the VENUS environment.

• Helen Lowe, Departement of Computing, Napier University, United Kingdom:
  XBarnacle: A Semi-automated Proof Tool
  The work of the team is in semi-automated inductive proof, with application to proving properties of recursive functions etc, nearer the "automated" end of the interactive-automated continuum. XBarnacle is a Prolog/Tcl interface to the automated proof planning system CLAM, which can prove many theorems unaided but which may need help, for example in the provision of lemmas or to correct some wrong choices, typically a wrong induction schema, or a mis-use of generalization. The aim is to facilitate interaction with the proof tool where necessary.

• Hans Martin Hörcher, Vossloh-Systemtechnik GmbH, Germany:
  To be announced.

• Magnus Herner:
  SDT and ITEX
  The tools SDT and ITEX are developed by the Swedish company. SDT and ITEX support the standardised, formally defined languages SDL, MSC, ASN.1 and TTCN for the integrated development and test of real-time communicating systems. An OM editor also supports the use of informal object-oriented analysis according to either Rumbaugh's OMT method or the newer Unified Method Language (UML) jointly developed by Rumbaugh, Booch and Jacobson.

• Andre Arnold:
  The model-checker MEC
  MEC is a tool aiming at helping the designer of a complex system to analyze its behaviour. The components of the system are modeled as labeled transition systems. The interaction between these components are described as the set of authorized or possible global actions of the system. Given these data, MEC computes the transition system modeling the whole system. Then, in an interactive way, the user can use MEC to compute sets of states and sets of transitions that satisfy properties expressible in some CTL-like temporal logic.

• Steven Bradley:
  The AORTA Tool Set
  AORTA (Application Oriented Real-Time Algebra) attempts to address some of the problems faced by designers of real-time systems by providing a formal language for system design and verification, which deals with quantitative time, and relates directly to implemented systems. In order to ensure implementability of designs, the language is more restrictive than many other timed formalisms, which can be used to model a wide range of possible behaviours, many of them unimplementable. The basic language is a timed process algebra, related to the timed variants of process algebras like CCS, LOTOS and CSP.