Fourth International Conference on Integrated Formal Methods
4-7 April 2004 in Canterbury, Kent, England
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.
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.
|Hosted by Computer Science @ Kent||
This page is maintained by