Using testing semantics to show safety and liveness in the development of CCS specifications

Abstract

Where formal methods are used in industrial software engineering, it is primarily as notation or language - an aid to the software engineer in thinking about and understanding the problem. What we address in this paper is the question of whether the laws of CCS can be used to prove important properties of a system, namely, safety and liveness. This begs questions about what precisely we mean by safety and liveness and how we model these properties within the constraints of the calculus. Ideally we should like to be able to prove an appropriate congruence between specification and design that would enable us to conclude that a property holding for the specification will also hold for the design. (We interpret 'design' to mean the refinement of a specification by decomposition.)