Application name:

BMW Rolls-Royce System Test Facility (STF)

Organisation:

DST Deutsche System-Technik GmbH, GSE Gesellschaft fuer Software Engineering.

Method:

Z

Tools:

DST-Fuzz

Domain:

Miscellaneous

Period:

1993 - 1994

Size:

Size of the specifications developed: 50 pages of Z.

Description:

The System Test Facility (STF) developed for BMW Rolls-Royce (BRR) Aero Engines is a system used for certification testing of the Electronic Engine Control (EEC) of a new family of aero engines currently under development by BRR. Only a small, but central part of the system, which is handling evaluation of test control language commands used to control test execution, was developed formally Here, mainly an abstract machine for evaluating these commands was defined in parallel with the final definition of the test control language. The result of this process was

• The formal specification of the language interpreter, which defined the precise language semantics and was reviewed internally,
• The language manual, which was reviewed by the customer,
• The structure of a simple compiler transforming the source language for the interpreter input language.

The specification was implemented directly. The specifications were embedded into the structured specification for the remaining system.

Conclusions:

The use of Z for this application domain could be seen positive, because: developing the test control language in parallel with its formal semantics directly lead to a clean structure of language and its implementation. After the extensive specification process including reviews (taking about six weeks), implementation of the subsystem was relatively straightforward, taking eight days and resulted in a running system after half a day of debugging. Only one error was detected during later acceptance test/operation. Missing experience in using formal methods together with tight time scales and geographical separation of the development teams prevented us from further extending the use of formal methods within this project.

Publications:

None.

Contact:

Name:	Hans-Martin Hoercher
Organisation:	DST Deutsche System-Technik GmbH
Address:	Edisonstrasse 3 D-24145 Kiel
Country:	Germany
Phone number:	+49 (431) 710
Fax:	+49 (431) 7109503
E-mail:	hoercher@dst.de
Personal website:	-

URL:

-

Remarks:

-

© copyright 2004 | Formal Methods Europe