© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Constraint oriented specification with CSP and real time temporal logic
Justin Pearson and Jeremy Bryans
Technical Report 3-98, University of Kent at Canterbury, July 1998.Abstract
A popular specification style, particularly for the initial specification of a system, is the {\em constraint-oriented style}, where the constraints are properties required to hold of the final system. One of the difficulties of using this style is that, for any particular notation, certain types of constraints are much harder to capture than others. In this paper we propose such a specification framework, which allows the specifier a choice of two languages: Communicating Sequential Processes (CSP) and a version of Propositional Temporal Logic (PTL). The components of a specification have to be checked for mutual consistency, to do this we present a common semantic framework for both PTL and CSP.
Download publication 100 kbytes
Bibtex Record
@techreport{598,
author = {Justin Pearson and Jeremy Bryans},
title = {Constraint Oriented Specification with {CSP} and Real Time Temporal Logic},
month = {July},
year = {1998},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1998/598},
institution = {University of Kent at Canterbury},
number = {3-98},
}