index.html

---
layout: default
title: HST
---

<h1>Overview</h1>

<p>
  HST is an open-source refinement checker for
  the <a href="https://en.wikipedia.org/wiki/Communicating_sequential_processes">CSP</a>
  process algebra.  It provides a library and set of command-line
  programs for processing CSP scripts.  The goal for the 1.0 release
  is to support refinement checking in the traces (T), stable failures
  (F), and failures-divergences (N) semantic models, all of which are
  described in [1].
</p>

<p>
  HST is divided into two major sections: the CSP₀ library, written in
  C++, and the CSPM libary, written in Haskell.  C++ was chosen for
  speed, since all LTS generation and refinement checking happens in
  the CSP₀ library.  Haskell was chosen since CSPM is a lazy,
  functional lanaguage — this us allows to use the same features of
  Haskell and not have to implement a lazy functional interpreter
  ourselves.
</p>

<p>
  For installation instructions, please see the INSTALL file.  There
  are currently two command-line programs — “cspm” and “csp0”.  The
  first allows you evaluate expressions in a CSPM script, and to
  compile CSPM process expressions into the corresponding CSP₀.  The
  second allows you to perform refinement checks on these compiled
  CSP₀ scripts.  Each program is self-documented; run “csp0 help” or
  “cspm help” for usage details.  The CSP₀ language is described in
  the csp0.html file, which should be installed as part of the
  standard installation process.  The most recent (and complete)
  description of the CSPM language can be found in the FDR2 reference
  manual [2].
</p>

<h1>Mailing list</h1>

<p>
  If you have questions about obtaining, installing, using, or
  developing HST, please join the
  HST <a href="https://groups.google.com/group/hst-project">mailing
  list</a>.
</p>

<h1>References</h1>

<div class="reference">
  <div class="citation_number">[1]</div>
  <div class="citation">
    A.W. Roscoe.  <em>The theory and practice of concurrency</em>.
    Prentice Hall, 1998.  ISBN
    0-13-6774409-5.  <a href="https://web.comlab.ox.ac.uk/oucl/publications/books/concurrency/">https://web.comlab.ox.ac.uk/oucl/publications/books/concurrency/</a>
  </div>
</div>

<div class="reference">
  <div class="citation_number">[2]</div>
  <div class="citation">
    Formal Systems (Europe) Ltd.  <em>Failures-Divergence Refinement:
    FDR2 Manual</em>.
    2005.  <a href="https://www.fsel.com/">https://www.fsel.com/</a>
  </div>
</div>