Process Algebra Models

Process Algebra Models allow users to specify processes in PVL programs. PVL programs must then be annotated to indicate which locations in the program correspond to transitions in the process model. Properties specified in the process model may be assumed by VerCors at the locations in the program, provided that these properties of the process model are proven using an external tool, such as the model checker mCRL2.

Support for checking if a PVL program adheres to a process model is automatic, and implemented in VerCors 1.4.0. Checking if a process model adheres to the specified properties can be automated, but currently is not, and hence has to be done manually.

For the theoretical background on Process Algebra Models, we refer the reader to Wytse Oortwijn's PhD thesis: https://doi.org/10.3990/1.9789036548984.

For more practical sources, we refer the reader to the following urls:

1. https://github.com/wytseoortwijn/SupplementaryMaterialsThesis: The repository of supplementary materials of Wytse Oortwijn's PhD thesis
2. https://github.com/wytseoortwijn/csl-abstractions: Supplementary materials of "An Abstraction Technique for Verifying Shared-Memory Concurrency", which is a generalisation of chapter 5 of Wytse Oortwijn's PhD thesis
3. The VerCors example directory:
   • https://github.com/utwente-fmt/vercors/tree/dev/examples/futures
   • https://github.com/utwente-fmt/vercors/tree/dev/examples/known-problems/futures

For any aspects not covered by the above summary, please contact the VerCors team.