Correct‐by‐construction specification to verified code. Issue 10 (25th June 2018)

• Record Type: Journal Article
• Authors: Ge, Ning; Dieumegard, Arnaud; Jenn, Eric; Voisin, Laurent
• Is Part Of: Journal of software. Volume 30:Issue 10(2018)
• Page Start: n/a
• Page End: n/a
• Publication Date: 2018-06-25
• Subjects: C -- code generation -- equivalence proof -- Event‐B -- formal methods -- property proof; Software engineering -- Periodicals; Computer software -- Development -- Periodicals; Software maintenance -- Periodicals; 005.1
• DOI: 10.1002/smr.1959
• Languages: English
• ISSNs: 2047-7473

Abstract

Abstract: Event‐B is a formal notation and method for the systems development. The key feature of this method is to produce correct‐by‐construction system designs. Once the correct design is established, the remaining work is to generate or implement correct code from the design. Two main problems remain in the process from the correct‐by‐construction design to the correct software. First, the Event‐B design is "quasi‐correct" due to some technical limitations. For instance, it is still difficult to prove the liveness properties by the Rodin platform; it is not possible to construct the Event‐B design with floating‐point arithmetic, and sometimes, the Event‐B model is incomplete and must rely on the third‐party libraries. Therefore, a method is needed to complement these modeling and proof gaps. Secondly, proving the correctness of an automatic code generator is very difficult; therefore, a method is needed to guarantee the correctness of the produced code without proving the code generator. In this article, we address the above 2 problems by introducing an intermediate formal language called High‐Level Language (HLL) between the Event‐B models and the C code. The Event‐B model is translated to HLL with an additional schedule configuration, where Event‐B invariants and system invariants (here, deadlock‐freeness and liveness properties) are proved using a SAT‐based model checker called S3. This proof guarantees the correctness of the HLL model with respect to the Event‐B model. The C code is then automatically generated from the HLL model for most functions and is manually implemented for the third‐party ones according to the function contracts defined in Event‐B. The correctness of the generated C code is guaranteed using the equivalence proof, and the correctness of the implemented C code is guaranteed using the conformance proof. Through the article, we use a traffic light controller to illustrate the proposed method; then, we apply the method to an automatic protection function of a 3‐wheeled robot to evaluate its feasibility.