Communicating Process Architectures 2009
Communicating Process
Architectures 2009 will start on the evening of Sunday 1st. November, through
to lunchtime on 4th. November at the Technische Universiteit Eindhoven
in Eindhoven, the Netherlands. The conference will run in its normal style
(a single stream of refereed papers during the day and fringe events
in the evenings). This year, however, we shall be part of
Formal Methods Week 2009
where registration for CPA also gives access to the sessions of other
conferences, tutorials and workshops running simultaenously –
follow their sidebar link to "Schedule" for the outline timetable.
Welcome!
WoTUG is a forum set up to support those applying the CSP
model of parallel processing. You will find on this site articles and information
that can help you design and build concurrent software and hardware systems that
really work, day in, day out, without any need to spend man-years of debugging
effort.
- Information on CSP, the mathematical basis of our work
- Our papers, the distilled results of our work
- The KRoC retargettable occam compiler
- A page about the group.
The Abstract below is from a paper in our database:
Working Towards the Agreement Problem Protocol Verification Environment
By James S. Pascoe, Roger J. Loader, V. S. Sunderam
This paper proposes the Agreement Problem Protocol Verification Environment (APPROVE) for the automated formal verification of novel solutions to agreement problems in group communication systems. Agreement problems are characterized by the need for a group of processes to agree on a proposed value and are exemplified by group membership, consensus and fault-tolerance scenarios. Due to their fundamental role, it is important that the correctness of new agreement algorithms be verified formally. In the past, the application of manual proof methods has been met with varying degrees of success, suggesting the need for a less error prone automated approach. An observation concerning previous proofs is that often a significant amount of effort is invested in modeling themes common to all such proofs, albeit using different formalisms. Thus, the APPROVE project aims to address these issues, its envisaged culmination being a usable software framework that exploits model re-use wherever possible.
Complete record...
|
