This theory generalizes the version 1999 theory. In version 1999, the theory restricts compositional reasoning to a system consisting of processes that synchronize by mutual exclusion. This restriction is now dropped. The new version 2002 maintains the same axiomatical style of version 1999, which we likes very much for its simplicity.
With respect to version 1999, the notation has been changed. There are also some minor changes to improve the definitions of the underlying concepts.
Keep in mind however that a more general theory has a broader application but it is also less powerful. For this reason we also include the instantiation of the new version 2002 to the version 1999 setup (specialized, as said above, for mutual exclusion based synchronization).
This work is still on-going. The non-interference and interference parts are finished. Coming next: the composition part.
Code Download:
In progress: COMUNITY version 2002. HOL version: Taupo 6.Documentation:
I.S.W.B. Prasetya, T.E.J. Vos, S.D. Swierstra, B. Widjaja. A Theory for Composing Distributed Components Based on Mutual Exclusion . Draft, 2002. Submitted for publication.