Skip to Main content Skip to Navigation
Conference papers

Methodology for Specification and Verification of High-Level Requirements with MetAcsl

Abstract : Specification and formal verification of high-level properties (such as security properties, like data integrity or confidentiality) over a large software product remains an important challenge for the industrial practice. Recent work introduced METACSL, a plugin of the FRAMA-C verification platform, that allows the user to specify high-level properties, called HIgh-Level ACSL REquirements or HILARE, for C programs and transform them into assertions that can then be verified by classic deductive verification. This paper presents a methodology of specification and verification of a wide range of high-level properties with METACSL and illustrates it on several examples. The goal is to provide verification practitioners with detailed methodological guidelines for common patterns of properties in order to facilitate their everyday work and to avoid some frequent pitfalls. The illustrating examples are inspired by very usual kinds of properties and illustrated on two use cases. One of them-on the real-life code of the bootloader module of the secure storage device Wookey-was fully verified using the described approach, demonstrating its capacity to scale to real-life code. The other one-on a microkernel of an OS-was added to illustrate other common properties, where the description of the system was intentionally left very generic.
Document type :
Conference papers
Complete list of metadata

https://hal-cea.archives-ouvertes.fr/cea-03179670
Contributor : Virgile Robles <>
Submitted on : Wednesday, March 24, 2021 - 12:47:14 PM
Last modification on : Tuesday, April 6, 2021 - 1:07:49 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : cea-03179670, version 1

Citation

Virgile Robles, Nikolai Kosmatov, Virgile Prévosto, Louis Rilling, Pascale Le Gall. Methodology for Specification and Verification of High-Level Requirements with MetAcsl. FormaliSE 2021 - 9th International Conference on Formal Methods in Software Engineering, IEEE TCSE; SIGSOFT, May 2021, Online conference, France. ⟨cea-03179670⟩

Share

Metrics

Record views

24

Files downloads

8