A Case Study in Safety-Critical Design
Glenn BrunsAbstract: We have modelled the design of a safety-critical railway system in the process calculus CCS, described important properties of the design in temporal logic, and verified with the Concurrency Workbench that some of the properties hold of the model. Verifying properties of a design, rather than an implementation, presented special problems, particularly in capturing in the formal model the kinds of abstraction found in the design, and in showing that the verified properties would also hold in all implementations of the design.
A revised version of this report appeared in the Proceedings of CAV '92. Springer Verlag, 1992. Lecture Notes in Computer Science, 354.
Previous | Index | Next