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)
Download:
temporalLogic.tar
Related publications:
1. Gavin Lowe, Specification of communicating processes: temporal logic versus refusals-based refinement, Formal Aspects of Computing, 2008. (PDF)
Download:
temporalLogic.tar