CCS-recent applications, experience with tools, current and planned research

The Mathematically Proven Safety Systems (MPSS) project in the Laboratory for Foundations of Computer Science of Edinburgh University is applying state-of the-art formal reasoning techniques and tools to the design of safety critical system. During the first year of the project the author has concentrated on process calculi and model-based approaches. One major case study concerned with reactor protection has been completed. This is the primary subject of this paper. On-going work includes investigations into the hazard analysis process and how formal descriptions of safety properties can be generated from this process. These properties would then be carried forward as proof obligations in the actual system design stage. Further case study work in progress includes several examples in railway signalling. All of the case studies so far conducted have static safe states (e.g. signals set to red, control rods in)