University of Oxford Logo University of OxfordDepartment of Computer Science - Home
Linked in
Linked in
Follow us on twitter
On Facebook

BPTL to CSP compiler

Specifications for model checking purposes can be expressed either as temporal logic formulae or as automata. Verification of models using the CSP process algebra has traditionally been based on the latter approach. Recently, Gavin Lowe studied the extent to which the FDR model checker can be used for testing whether a given CSP process satisfies a temporal logic specification. He also implemented a compiler for translating formulae expressed in the bounded, positive fragment BPTL of TL into standard CSP specifications, available below.

Related publications:
1. Gavin Lowe, Specification of communicating processes: temporal logic versus refusals-based refinement, Formal Aspects of Computing, 2008. (PDF)