Promoting the Design of Embedded Systems / PERSYVAL-Minalogic Breakfast Meetings

In this context, it is essential to be able to rigorously model the hardware/software system from the earliest stages of the design flow and to perform design verification throughout that flow. Two main categories of methods address this challenge: runtime verification via simulation and symbolic reasoning using formal methods. These two rapidly evolving fields offer a wide range of rich and complementary solutions.

The purpose of this meeting is to provide an overview of their respective contributions: on the one hand, the latest advances in the efficiency of processor-based system simulation using virtualization techniques; and on the other hand, the variety of verifications and analyses that can be performed using tools based on formal reasoning.

Program and presentations

• 8:15–8:30 a.m.: Welcome
• 8:30–8:45 a.m.: Introductory presentation:
  Overview of Simulation and Formal Methods:
  Laurence Pierre, Université Grenoble Alpes, TIMA Laboratory and IM2AG Department:
  Download the presentation
• 8:45–9:45 a.m.: Specialized presentations
  • Virtual Platforms: Efficient Hardware/Software Simulation and New Virtualization Techniques
    Frédéric Pétrot, Grenoble INP, TIMA Laboratory
    Download the presentation
    The goal of virtual prototyping is to simulate the behavior of a complete digital system consisting of a virtual model of the hardware platform—including processors—and the software running on those processors. This approach relies on specific modeling techniques and can be implemented at different levels of abstraction, allowing for trade-offs between speed and accuracy. This presentation details the challenges faced by virtual prototyping methods and introduces commonly accepted levels of abstraction. We will focus in particular on techniques utilizing dynamic binary translation and its integration within SystemC, the current standard for modeling digital components.
  • Contribution of Formal Methods
    David Monniaux, CNRS, VERIMAG Laboratory
    Download the presentation
    In addition to simulation-based analyses, numerous methods allow for formal reasoning on a system model in order to verify various properties (functional correctness, absence of deadlocks, compliance with real-time constraints, correctness of memory accesses, etc.). These methods rely on various techniques (model checking, static analysis, proof assistants, etc.). The goal of this presentation is to provide an overview of the verifications that can be performed and the current state of the associated methods and tools.
• 9:45–10:00 a.m.: Conclusion
  Summary of collaboration opportunities, LabEx teams, and master’s programs related to this topic
  Download the presentation
• 10:00–10:30 a.m.: Discussion time (may continue until 11:00 a.m. for those who wish to stay)