Application name:

Architecture for a Family of Oscilloscopes

Organisation:

Tektronix, Inc. Computer Research Labs and several product development divisions.

Method:

Z

Tools:

Fuzz and ZEE (our homegrown Z editor)

Domain:

Hardware modelling

Period:

1987 - 1990

Size:

Major oscilloscope product family. 50 Software engineers working on various aspects of development. Formal specification part was done by a small subset of these; most of the specifications ran under 50 pages, including descriptive prose.

Description:

We developed several formal architectural models for a family of oscilloscopes. The formal models served to identify common product infrastructure that could be shared by implementations for a number of related products. The formal models were developed by a small number of researchers working with product engineers. Emphasis was on reasoning about properties of the models rather than proofs of correctness. The project combined prototyping with formal specification: the former tied the the models to reality, and the latter kept the implementation clean.

Conclusions:

Formal methods can be applied in a cost-effective way in industry if they are used to specify product family architectures.

Publications:

"Formal Specification of an Architecture for a Family of Instrumentation Systems." David Garlan and Norman Delisle. In: Applications of Formal Methods, Michael G. Hinchey and Jonathan P. Bowen (editors). Prentice Hall International Series in Computer Science. To appear, mid 1995.

"Applying Formal Specification to Industrial Problems: A Specification of an Oscilloscope". Norman Delisle and David Garlan. IEEE Software, 7(5): 29-36. September 1990.

"The Role of Formal Reusable Frameworks". David Garlan. In: Proceedings of the First ACM/SIGSOFT Workshop on Formal Methods in Software Development (Napa, California, May 1990).

"Formal Specifications as Reusable Frameworks". David Garlan and Norman Delisle. In: VDM'90; VDM and Z -- Formal Methods in Software Development. D. Bjoerner, H. Langmaack and C.A.R. Hoare (editors). Springer-Verlag, LNCS 428. Pages 135-149. 1990.

"The Role of Formalized Domain-Specific Frameworks". David Garlan. In: Proceedings of the Fifth International Software Process Workshop (October 1989).

"Formally Specifying Electronic Instruments". Norman Delisle and David Garlan. In: Proceedings of the Fifth International Workshop on Software Specification and Design (May 1989).

Contact:

Name:	David Garlan
Organisation:	Department of Computer Science, Carnegie Mellon University
Address:	5000 Forbes Avenue Pittsburgh PA 15213-3891
Country:	USA
Phone number:	+1 (412) 2685056
Fax:	+1 (412) 2685576
E-mail:	garlan@cs.cmu.edu
Personal website:	-

URL:

-

Remarks:

-

© copyright 2004 | Formal Methods Europe