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

Baillie, J. (1994) Using testing semantics to show safety and liveness in the development of CCS specifications. UH Computer Science Technical Report . University of Hertfordshire.
Copy

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.)


picture_as_pdf
CSTR+199.pdf

View Download

Atom BibTeX OpenURL ContextObject in Span OpenURL ContextObject Dublin Core MPEG-21 DIDL Data Cite XML EndNote HTML Citation METS MODS RIOXX2 XML Reference Manager Refer ASCII Citation
Export

Downloads