Application name:

FlowBus Component

Organisation:

Bull Information Systems, EPSRC Rutherford-Appleton Laboratory and B-Core Ltd.

Method:

VDM-SL (for the initial specification) and the B-Method (for the development of the component).

Tools:

VDM Through Pictures and The B-Toolkit

Domain:

Hardware modelling.

Period:

January 1994 - November 1994.

Size:

Approximately 2 man-years. About 1000 lines of VDM specification and about 2000 lines of B were written.

Description:

The FlowBus component allows two different formatted machines to communicate with each other without writing a single line of code to try and interface the machines. FlowBus is written on a Unix platform.

The initial specification of the FlowBus component was developed in VDM. After the creation of this specification, a locally developed test case generator was used, forming the basis of the product's test specification. The VDM specification was then translated into B designs, because the B-Tool facilitates the automatic generation of C code.

Some of the proofs resulting from these B designs could not be analyzed at Bull and hence expertise from B-Core was hired in. Because of the proofs, numerous faults in the VDM specification were found. Next, C code was automatically created and incorporated into the B-Tool library so that various parts of FlowBus could be integrated in a bottom-up fashion.

Conclusions:

The B-Tool has significant potential in letting users test out abstract design specifications. Also, the facilities offered by the B-Tool to generate `abstract libraries' and C-code from a specification turn out to be very useful and powerful features. The exercise is considered to be very successful.

Publications:

None.

Contact:

Name:	Mr. Jeremy Dick
Organisation:	Bull Information Systems
Address:	Maxted Road Hemel Hampstead HP2 7DZ
Country:	UK

© copyright 2004 | Formal Methods Europe