Date: Mon, 18 Mar 1991 11:58:29 PST
From: JON@edu.WASHINGTON.RAD.GAFFER (Jon Jacky)
Message-Id: <910318115829.29d0@GAFFER.RAD.WASHINGTON.EDU>
Subject: HOL and control systems?
To: info-hol@edu.ucdavis.clover
Sender: JON@edu.WASHINGTON.RAD.GAFFER

I am seeking additional information about a project described in a brief
article:

	S. Tran, J. Cullyer, E. Hines, and K. Marks.  "On the development 
	of formal methods-based software design methodology for automotive 
	applications", 	Microprocessors and Microsystems 14(5) June 1990, 
	320 - 323.

The paper describes the development of a microprocessor-controlled automobile
throttle.  Some excerpts:

	"The ... system is basically a three-term [proportional-integral-
	-differential, or PID]  controller which performs
	calculations on a set of filtered inputs (sucha as driver demand,
	engine temperature, etc.) and produces a pulse-width-modulation 
	(PWM) output which then controls the butterfly angle in the valve
	actuator. ... the design has been classified safety-critical.  An
	example of a catastrophic failure is the throttle either fully opened
	or fully closed as the vehicle is being driven. ...
	
	... The Viper design process was used.  The top-level specification
	is written in Gordon's High Order Logic and has been verified
	using the HOL theorem prover.  It is then animated by a `prototype'
	implementation using a subset of Pascal ... The project is complete
	and being installed in a full system.    It is thus possible to
	examine the effectiveness of the methods used in this project."

The article also shows (but does not really explain) a fragment of HOL text
that apparently specifies the PID controller.

The claims in that second paragraph are quite impressive.  In particular, I am
not aware of any other instance where a formally developed process control
system was actually placed into operation, so that experience in the field
could be observed and reported.  Can anyone provide me with additional
information or references about this project?   

The brief bibliography with the article cites two technical reports (not about
this project) from co-author S. C. Tran at "T&N Technology Ltd." but the
address of this firm is not given.   This project was not mentioned in the "HOL
Around the World" memo that Sara Kalvala circulated to this list a while ago.

This project is relevant to my interest in the safety of medical devices that
contain or use computers.  Currently, I am investigating formal approaches to
specifying and developing software for the control system of a medical
cyclotron that we use for neutron radiation therapy and isotope production. 

Jonathan Jacky				jon@gaffer.rad.washington.edu
Radiation Oncology RC-08		voice:	(206)-548-4117
University of Washington		FAX:	(206)-548-6218	
Seattle, Washington  98195
USA