|Final Report of the COST-247 Action|
Focus Points and Convergent Process Operators
Jan Friso Groote
|Centrum voor Wiskunde en Informatica|
|Specification and Analysis of Embedded Systems|
|P.O. Box 94079|
|1090 GB Amsterdam|
We are searching for improved ways to prove the correctness of distributed systems and protocols. Our investigation has led to a method that we baptise the Cones and Foci method. A parallel process is first transformed in a linear process by expanding the parallellism. By using convergent process operators, the description remains relatively small and the state space explosion is circumvented. Then, in order to prove a specification equal to an implementation, six sets of requirements need to be checked. Using this method we have proven a number of rather intricate distributed systems correct.
This presentation has been given during the COST-247 6th Management Committee Meeting (Budapest, Hungary, October 26-27, 1995).
COST-247 Working Group(s): 1
Web link: http://www.cwi.nl/~jfg
This Page was prepared by Mark Jorgensen.