BEACON - Box Algebra with Asynchronous Communications

Project Dates: From March 2001 to July 2003

Project Leader: Prof. Maciej Koutny

Sponsors: EPSRC

The aim of this project is to develop a conservative extension of the existing Box Algebra to support asynchronous communic action primitives both at the low-level and high-level net level. The first objective is to develop an algebraic treatment of asynchronous link extension of the Box Algebra, including the syntax, operational semantic rules, and proofs of behavioural consistency. This will be achieved by adopting key ideas which proved to be effective for the existing Box Algebra. We will re-consider the notion of equivalence used in the present framework, and for the chosen equivalence attempt to prove that the operational and compositional net semantics coincide. The second objective of the project - extending the results to a model based on high-level Petri nets - is crucial from the point of view of applying the results of the planned work to the modelling and verification of concurrent programs employing timing constraints and pre-emption. Using a suitable model of high-level nets, we will introduce a simple typing scheme on the basis of the formalism developed in the first stage of the project. As a result, we will be able to handle (in a compositional way) the semantics of a non-trivial procedural concurrent programming language.