Application name:

CICS development with B

Organisation:

IBM UK Laboratories Ltd., UK and B-Core UK Ltd., UK

Method:

B-Method / Abstract Machine Notation (AMN)

Tools:

B-Toolkit

Domain:

Transaction processing systems; Software Engineering

Period:

March 1993 - December 1994

Size:

(Approximate figures:) Specification: 750 lines AMN, implementation: 2500 lines AMN. 10,000 Lines of generated code. 2 Man-years.

Description:

B-Method was applied to development of a new component of a future release of CICS/ESA. Collaborative project with B-Toolkit vendors (B-Core UK Ltd.). Formal specification, initially in Z, was translated (by hand) into AMN. Some formal verification of the specification was attempted, but we did not attempt formal proof of refinements. Layered design, following B-Method, was conducted in AMN. Tools tailored for CICS used to generate code from low-level designs. Same personnel involved in specification and implementation. Consultancy from B-Toolkit vendors was important and useful.

Conclusions:

Tools support for the method was central to the work. Considerable effort was put into tailoring toolkit for CICS. Specification and animation in AMN were very helpful in checking the validity of the initial specification. Some problems encountered (but largely overcome) in integrating the B-Method with CICS architecture requirements. Project has demonstrated the possibility of automating mechanical aspects of the coding process, and the value of tools such as type-checkers and code generators in reducing coding errors.

Publications:

None.

Contact:

Name:	Ib Sorensen
Organisation:	B-Core UK Ltd.
Address:	Magdalen Centre Oxford Science Park Oxford OX4 4GA
Country:	Magdalen CentreOxford Science ParkUK
Phone number:	+44 (186) 5784520
Fax:	+44 (186) 5784518
E-mail:	Ib.Sorensen@comlab.ox.ac.uk

© copyright 2004 | Formal Methods Europe