Constraint Oriented Specification with CSP and Real Time Temporal Logic

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.