A Framework for the Hazard Analysis of Chemical Plants
Universität Dortmund, FB Informatik, LS IV, D-44221 Dortmund, Germany
Transposing the notion of software frameworks to the
abstraction level of formal specifications and verifications, we
developed a framework supporting the formal hazard analysis of chemical
plants. It provides generic specification modules for the description of
safety properties, specification modules for the description of plant
models, and theorems stating that certain subsystem structures of the
plant model imply certain safety properties. Using the framework for
hazard analysis, one firstly describes the plant and its control
equipment as a composition of framework module instances. Secondly, one
expresses the different safety properties of interest by parameterized
framework modules. Finally, a safety property is proven when an
appropriate theorem instance of the framework can be found. Thus, the
framework facilitates the formal modeling. Moreover, the efforts for
formal verifications are reduced drastically since framework theorem
instances can replace explicit proofs.
The framework utilizes modular temporal logic specifications supported
by the specification language cTLA which is a variant of Lamport's
temporal logic of actions TLA and in particular is devoted to the
compositional description of process systems.
Proceedings of the 11th IEEE International Symposium on
Computer-Aided Control System Design
(CACSD2000), pages 35-41, Anchorage, Sep. 2000. IEEE CSS, Omnipress.
Obtaining the paper
Due to the copyright agreement between the publisher and the authors we are
not allowed to make the paper available online. If you have problems to
please call us.
Peter Herrmann, November 7, 2000
-- digital media copyright