The Circal Process Algebra

Circal (for CIRcuit CALculus) is a formalism for specifying communicating concurrent finite state systems. Circal's distinguishing characteristics in the space of process calculii are:

• Processes are guarded by sets of actions that occur simultaneously, and and arbitrary number of processes can synchronize on the same action.
• There is no special action to describe a process that is evolving due to an internal (invisible) cause. That role is played by evolution on an empty action set, and is expressed by an internal choice operator.
• The concurrent composition operator allows (and requires) the synchronisation of actions with the same name and prevents actions belonging to both of the components from occurring independantly.

Tools

The Circal System embeds Circal in a C - like modelling language and provides an automatic verification engine for comparing Circal processes.

Publications and Reports

(list at the University of South Australia)