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

J. Baillie

Research output: Book/ReportOther report

50 Downloads (Pure)

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.)
Original languageEnglish
PublisherUniversity of Hertfordshire
Publication statusPublished - 1994

Publication series

NameUH Computer Science Technical Report
PublisherUniversity of Hertfordshire
Volume199

Fingerprint

Dive into the research topics of 'Using testing semantics to show safety and liveness in the development of CCS specifications'. Together they form a unique fingerprint.

Cite this