Translating bach programs for better verification of shared data
Modelling Shared-Space Coordination in mCRL2: a Bach-to-mCRL2 Translation Framework
Logic in Computer ScienceProgramming Languages
Summary
Making sure complex computer systems work right is hard, especially when many parts share and change data. The paper shows how Bach programs, which coordinate data sharing, can be translated into another language called mCRL2. This helps check not just if states can happen, but also if important ongoing rules are followed, like responses always matching requests. The authors also provide a way to write and check these detailed rules directly about the shared data, improving how system correctness is verified.
What this means in practice
- •For distributed systems developers: Verify complex properties of data sharing and communication protocols automatically by translating coordination code into mCRL2 for model checking.
- •For software verification engineers: Check ongoing behavioral rules like ensuring messages are always responded to within coordinated programs using the enhanced verification approach.
Authors
Corentin Reuther, Jean-Marie Jacquet
Abstract
Although significant research has focused on the theory and implementation of data-based coordination languages, the critical aspect of their automated verification using model-checking techniques remains underexplored, which is essential for ensuring reliability and correctness in distributed systems. Existing tools, such as Anemone, provide a solid foundation for reachability-based verification of Bach programs. While they effectively analyze properties expressed in terms of state attainability, extending support to more expressive temporal specifications-such as liveness properties or invariants over shared space contents-remains an open opportunity. Such extensions are important to capture comprehensive system behaviors, for instance, ensuring that "a request is always matched by a response" or that "no message is silently lost". Addressing this limitation, we propose an automated translation from Bach to mCRL2, which explicitly represents the shared space, thereby enabling the use of mCRL2's mu-calculus model checker to verify complex properties beyond simple reachability. Complementing this translation, we introduce a systematic method to analyze the shared space in mCRL2 concerning data reachability, by directly expressing properties over the shared space's contents in the mu-calculus, thus providing a clearer framework for verification. This approach enables a novel verification process that combines action-based properties with state-based properties over the shared space contents, a largely unexplored area in current coordination-language verification approaches, offering a new dimension of analysis