This Lecture
An Industrial Case Study
	A Formal Specification of an Oscilloscope
	Delisle and Garlan, IEEE Software (Sept 1990)

New concepts
•	Bridging the gap between theory and practice
•	Axiomatic specifications
•	Higher-order functional specifications
But First ...
Two Useful Identities
1.  " x: T | P(x) ∑ Q(x) 
∫ 
  " x: T ∑ P(x) ﬁ Q(x)

2.  $ x: T | P(x) ∑ Q(x) 
∫ 
  $ x: T ∑ P(x) Ÿ Q(x)

Context
The Problem
At Tektronix
•	Many divisions building similar product
•	No reuse among product efforts
•	Long time-to-market (5 years)
•	Each product typically built from scratch
•	User interface increasingly important
•	Software effort increasingly larger proportion of development costs

Goals
•	Build next generation instrumentation systems
•	Allow reuse between product divisions
• 	Support better interactive response to user changes
• 	Multiple hardware platforms for same user interface
• 	Multiple user interfaces for same platform 
	(vertical markets)
First Attempt
First attempt was an Object-Oriented Architecture
Layered View
Second  attempt was Layered Architecture
Functional View
Traces = Oscilloscope (Signals)
Signals, Waveforms, Traces
Basic Types
AbsTime 	==  N
RelTime	==  N
Volts	==  Z
Horiz	==  Z
Vert	==  Z
Signals, Waveforms, Traces
Channel Subsystem
Coupling
Acquisition
Clip
Channel Parameters
Channel Configuration
Trigger Subsystem
Channel Selection
Trigger Detection
Trigger Parameters
Trigger Configuration
The Whole System
Oscilloscope
Role of Formalism
• What was formalized
	- User level model (higher-order P/F)
	- Connection framework (colored P/F)
	- User interface architecture 
• Benefits of formalism
	- Motivated and constrained architectures
	- Conceptual prototyping
	- Communication medium
• Non-benefits
	- Correctness
	- Completeness
	- Adoption of formal methods within Tektronix
Some Morals
• Success requires
	- Domain experts and system builders
	- Expertise in abstraction
	- Skill in manipulating formal models
	- Willingness to abandon old implementation patterns
	- Willingness to reject inappropriate models
• Tools
	- Not needed during conceptualization
	- Essential during development
• Management
	- Must keep hands off the process initially
	- Must help inforce standards later
Last Slide
The Whole System