During the period leading from M01 to M18, the project has achieved significant work that can be described in different research streams:

  • Three use-cases are running in parallel and performed the following tasks:
    • Definition of the precise perimeter for analysis and of high-level security and safety properties.
    • Set up of the project analysis tools and training.
    • First round of analyses (on-going).
  • Research and development to solve the technical problems in the analysis tools. This includes the following tasks that are under way:
    • Connections between modelling and formal verification tools.
    • Improvements of the core tools Frama-C, VeriFast, Diversity, Contiki, and FlowArmor.
    • Improvements of related plug-ins, such as E-ACSL and Frama-clang.
    • Connections between the formal analysis tool Frama-C and testing tool AFL and between Frama-C and modelling tool Diversity.
    • Development of new GUI and a client-server proof architecture for Frama-C.
    • Improvements of the ACSL++ specification language for C++.
  • Research on methodologies by integrating the end-user’s concrete needs, the economic concerns and the quality measurements.
  • In parallel dissemination activities.

In terms of progress beyond the state of the art, we expect to advance in the following areas:

  • Improved formal methods usability and stability: Frama-C has been experimented since 2005 on numerous applications from different domains improve the tool and its methodology. In VESSEDIA we tackle the field of IoT through three IoT use-cases. The same experimental approach holds for the VeriFast, Diversity, Contiki, and FlowArmor tools that have evolved along experiments and applications.
  • Improved scalability: VESSEDIA expects to scale up source code analysis tools by improving the efficiency of the tools and demonstrate it on the project’s use-cases.
  • Standardisation: In the ISO JTC1 VESSEDIA will produce in three years a normative ISO standard for V&V tools.
  • Improved modularity and abstraction: programming languages have improved significantly with abstraction means at the language level allowing more efficient programming and less error prone programs. In VESSEDIA, the connections between design and formal methods will help in the same manner by 1) more abstract descriptions of systems, 2) system-level security properties and their refinements, and 3) integration of detailed specifications at design level.
  • Methodology: a proper methodology will be proposed for using the tools, taking into account the environment and the economic and certification constraints.