[an error occurred while processing this directive]<title>Department of Computer Science: Concurrency</title>
<meta name="keywords"
      content="Department of Computer Science Research Activities Concurrency"></meta>
<meta property="og:site_name" content="Department of Computer Science"></meta>
<meta property="og:title" content="Concurrency"></meta>
<meta property="og:image"
      content="http://www.cs.ox.ac.uk/images/CompSci_logo_landscapeL_rgb_corrected.jpg"></meta>
<meta property="og:url" content="http://www.cs.ox.ac.uk/activities/concurrency/"></meta>
<meta name="Author" content="Tom Newcomb, Tomasz Mazur"/>
[an error occurred while processing this directive]
<div id="breadcrumb">
   <span id="breadcrumb-label">You are here:</span>
   <ul>
      <li>
         <a href="/">Home</a>
      </li>
      <li>
         <a href="/research/">Research</a>
      </li>
      <li>
         <a href="/research/activities.html">Activities</a>
      </li>
      <li>
         <a href="/activities/concurrency">Concurrency</a>
      </li>
       <li>
         <a href="/activities/concurrency/tools">Tools</a>
      </li>
      <li>
         <span class="youarehere">BPTL to CSP compiler</span>
      </li>
   </ul>
</div>
<div id="content">


<h1>BPTL to CSP compiler<br>
</h1>
<div class="personalContent">
<span class="il">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 <a href="../fdr">FDR</a> 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.<br>
</span><br>
<br>
Related publications:<br>
1. Gavin Lowe, Specification of communicating processes: temporal logic
versus refusals-based refinement, <span style="font-style: italic;">Formal
Aspects of Computing</span>, 2008. (<a
 href="http://www.cs.ox.ac.uk/files/368/tl.pdf">PDF</a>)<br>
<br>
<br>
Download:<a
 href="http://www.cs.ox.ac.uk/people/gavin.lowe/Papers/temporalLogic.tar"><br>
<big><span style="font-family: monospace;">temporalLogic.tar</span></big></a><br>
<br>
</div>


</div>
[an error occurred while processing this directive]
[an error occurred while processing this directive]
[an error occurred while processing this directive]