Bridging the B-Method and ACSL: Towards Verified C Code

• Fagner M. Dias Universidade Federal do Rio Grande do Norte https://orcid.org/0009-0002-1385-3558
• Marcel V. M. Oliveira Universidade Federal do Rio Grande do Norte https://orcid.org/0000-0002-3023-2748
• Thierry Lecomte CLEARSY https://orcid.org/0000-0001-8977-4827

Resumo

The B-Method is a formal specification and development methodology that ensures system correctness with a design-by-contract approach. However, translating these high-level specifications into C code introduces challenges, particularly in verifying that the generated code respects the specified properties. To address this, we propose a systematic translation process from the B-Method to ACSL, which enables the formal verification of the C code using Frama-C, a static analysis tool. The proposed method provides a set of ACSL specifications that correspond to B-Method abstractions, allowing for deductive verification of the C code to ensure compliance with safety and correctness requirements. A case study demonstrates the practical application of this translation strategy, showing its effectiveness in verifying a simple runner-counting system.

Palavras-chave: Formal Verification, C Code Verification, Software Safety