A Framework for the Hazard Analysis of Chemical Plants

Peter Herrmann, Heiko Krumm

Universität Dortmund, FB Informatik, LS IV, D-44221 Dortmund, Germany
E-Mail: {herrmann| krumm}@ls4.cs.tu-dortmund.de

Abstract

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.

Published in

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 obtain it, please call us.