Introduction

FSP stands for Finite State Process. It is the notation used to specify the behaviour of concurrent systems to LTSA. FSP specifications generate finite Labelled Transition Systems (see). The syntax and semantics owe much to both Hoare's CSP and Milner's CCS. FSP behaviour specifications contain (see semantics) two sorts of process definitions: primitive processes and composite processes. Safety properties are specified using property automata and liveness properties using Buchi automata.

Primitive Processes

Primitive processes are defined using action prefix, choice and recursion. Both action labels and local process names may be indexed which greatly increases the descriptive power of FSP.

Composite Processes

Composite processes are defined using parallel composition, relabelling and hiding.

Properties

LTSA provides different techniques for checking safety and properties. Correspondingly, FSP provides a way of specifying safety properties (using image automata) and a way of specifying liveness properties (using Buchi automata).

FSP Syntax reference

FSP Semantics