SYRF Project
Task 4/5.4: "Verification of mixed A/S systems"
Abstract of deliverable 4/5.4.2
Achieved Results:
The work this year was mostly spent in the programming of a prototype tool
implementing the partitioning of transition for analysis of mixed A/S systems.
Theoretical foundations were described in the first year's deliverable.
We refined our proposed algorithms and the detailed method was presented
at the IWLS'98 workshop in Lake Tahoe this year.
The transition relation is
partititioned across two levels : an inner synchronous level where
partitioning follows ``classical'' division according to boolean control
registers; an outer level where partitioning is divided according to global
actions (or events), more in the lines of process algebras. Of course
here the behaviours of single components can be more complex than a simple
synchronisation offer, which accounts for the main issue in combining local
behaviours correctly into global ones.
Publications:
- A. Bouali, R. de Simone
A Symbolic Representation of Asynchronous Networks of Synchronous Processes
Proceedings of the Tenth International Workshop on Logic Synthesis (IWLS'98)
Lake Tahoe, CA, USA