Gabriel@ANL-MCS@sri-unix.UUCP (09/28/83)
From: Gabriel@ANL-MCS (John Gabriel)
Copies of our reports ANL-83-70, and ANL-MCSD-TM-11 have been
sent to SU-Score for filing in the <Prolog> directory. Both
contain appendices listing experimental Prolog programs, both
are in the public domain.
ANL-83-70 deals with the automated diagnosis of faults in physical
plant. The actual problem solved is a "toy" piece of combinational
digital logic, but we have a proposal in to work on a sequential
relay logic system of about 1000 relays managing interlocks on
a real plant. I am not sure at this stage if we will be funded,
but I hope we will be and that we will be able to put the
proofs of principle, if not the production system in the public
domain.
Use of Prolog based systems in real plant, particularly very
expensive real plant having expected life in the fifty year
range for major components raises interesting questions about
software upgrades to track plant upgrades. In addition
requirements to certify reliability of systems important to
plant safety are severe by ordinary standards.
In the long term this may force us towards development efforts
on such things as Prolog compilers generating code running on
triply redundant processors, simply because that may be the
only way we establish traceability of decisions in software
development, together with required hardware reliability.
But those are some way away, and we expect to use the EDCAAD
CProlog for proofs of principle, and publish this work as
required by the EDCAAD licensing agreement.
ANL-MCSD-TM-11 deals with the following problem:- Suppose a
physical plant (or a software program) consists of components
(processes) linked by connections (data flows). Some aspects
of quality assurance for software or hardware "important to
safety" require certifications that the only paths into some
subsystem are those listed by the manufacturer.
The problem may be simply stated in graph theory; " Given a set
of arcs and two subgraphs of a given graph, prove the set of
arcs if removed separate the graph into a pair of disjoint
subgraphs, and that the two given subgraphs are one in each
of the subgraphs separated by removal of the given arcs".
If this theorem is denied, find the additional arcs to be
cut in order to make it true.
[ These reports can obtained through FTP as:
{SU-Score}PS:<Prolog>ANL-83-70.Txt
ANL-MCS-TM11.Txt
ANL-MCS-TM11.Figures -ed ]