Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: Wed, 15 Apr 1992 9:49:30 -0700 (PDT)
From: JON@edu.washington.radonc.gaffer (Jon Jacky)
Message-Id: <920415094930.21e001e2@gaffer.radonc.washington.edu>
Subject: Re: formal treatment of PLCs
To: info-hol@edu.uidaho.cs.ted

Roger Jones asks ---

> Does anyone know of any work that has been done on the use of
> HOL or Z in the development of applications for Programmable
> Logic Controllers?

I've thought about this, and have a half-baked unpublished manuscript that I've
abandoned indefinitely.

Our cyclotron control system uses PLC's extensively for some of the "easier"
on-off controls and sequencing: vacuum, cooling, some beamline components, some
equipment protection, some backup for the hardwired people protection.

I've always thought that PLC's would be an ideal application for formal
methods, particularly the kinds of things that are already very mature in the
digital electronics world: BDD's, model checking, etc.   The PLC people are
completely ignorant of this work - have never heard of it - while the hardware
verification people are just as oblivious to the existence of the PLC world and
its considerable economic significance.  It is likely that more factories and
process control systems use PLC's than general purpose computers programmed in
some language that computer science people know about.

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