Tools' Abstracts

Efficient CSP-Z Data Abstraction. Adalberto Farias, Alexandre Mota, and Augusto Sampaio

In this work we present a Java tool which provides support for applying the strategy of data abstraction to CSP-Z specifications. According to the strategy, finite processes can be derived from infinite ones by replacing infinite data types with finite ones and rewriting operations, while still preserving almost all original properties. The technique is based on the stable and infinite behaviour of a CSP-Z process. The tool can interact with theorem provers and model checkers in order to determine the stability of a CSP-Z process. The tool also allows the user to provide plugins to interact with different theorem provers (and model checkers). Additionally, the tool also provides for translating CSP-Z into CSP-M, the machine-readable version of CSP accepted by the FDR tool.

UML to B: Formal Verification of Object-oriented Models. Colin Snook

U2B is a tool for translating UML-B models into the formal notation, B. The UML-B is a profile of the UML that defines a subset and specialisation of UML that has a mapping to, and is therefore suitable for translation into B. The UML-B profile consists of class diagrams with attached statecharts, and an integrated constraint and action language that is based on the B notation. The UML-B profile uses stereotypes to specialise the meaning of UML entities, thus enriching the standard UML notation and increasing its correspondence with B concepts. The UML-B profile also defines tagged values (UML-B clauses) that may be attached to UML entities. UML-B clauses are used to attach details that are not part of the standard UML. Several styles of modelling are available within UML-B including an event systems mode, which corresponds with the Event B modelling paradigm. UML-B provides a diagramatic, formal modelling notation. It has a well defined semantics as a direct result of its mapping to B. As with most formal notations, there is often a strong reluctance to use B in industrial settings. The popularity of the UML enables UML-B to overcome this reluctance. Its familiar diagramatic notations make specifications accessible to domain experts who may not be familiar with formal notations such as B. UML-B hides B's infrastructure and packages mathematical constraints and action specifications into small sections each being presented in the context of its owning UML entity. The demonstration will illustrate the use of UML-B for abstract modelling of systems, and the use of U2B and the animator/model checker, ProB, for efficient and effective validation and verification. U2B is available for download here: http://www.ecs.soton.ac.uk/~cfs/U2Bdownloads/U2Bdownloads.htm

Software Verification with Integrated Data Type Refinement for Integer Arithmetic. Bernhard Beckert and Steffen Schlager

The KeY system enhances the commercial UML CASE tool Borland Together ControlCenter with functionality for formal specification and deductive verification.
It is developed in the context of the ongoing KeY project, which aims to integrate formal methods into real-world software development processes. The main features of KeY are:

User continues to work in familiar modelling environment

Support for parsing and pattern-based generation of OCL constraints

Dynamic Logic as logical basis for reasoning about models and implementations

Target language: Java Card

Integrated automated and interactive proof tools

The ultimate goal of the KeY project is to facilitate and promote the use of formal verification as an integral part of the development process of Java Card applications in an industrial context.
More information on KeY as well as the current version of the KeY system are available for download at http://www.key-project.org.

Perfect Developer: a tool for Object-Oriented Formal Specification and Refinement. David Crocker

Perfect Developer is a high-productivity software development tool for devel-oping formal specifications and refining them to code. The tool uses advanced automated reasoning to discharge almost all proof obligations without user inter-vention. Advanced mathematical knowledge is not a pre-requisite, which means that any developer uent in an object-oriented language such as Java or C++ should be able to learn the notation. A single notation is used to express functional requirements, specifications, and code. Specifications can be verified against the requirements. They can then be refined into code either manually (with verification) or, in many cases, auto-matically. The final code is automatically translated into ready-to-compile Java or C++. Perfect Developer is of commercial interest primarily for safety-critical or mission-critical applications, but its high productivity makes it suitable for non-critical applications too. It is also used by several universities for teaching formal methods to undergraduates and for research.
Further information at http://www.eschertech.com/papers/fme_2003_tools_paper.pdf.