Boosting Embedded Systems Design / PERSYVAL-Minalogic Breakfasts

This context makes it essential to be able to rigorously model the hardware/software system from the earliest stages of the design flow and to verify proper design throughout this flow. Two major families of methods contribute to this challenge: execution verification via simulation and symbolic reasoning using formal methods. These two constantly evolving fields offer a rich and complementary range of solutions.

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

Program and presentations

• 08:15-08:30: Welcome
• 08:30-08:45: Introductory presentation
  Simulation/Formal Methods positioning in brief
  Laurence Pierre, Université Grenoble Alpes, TIMA laboratory and UFR IM2AG
  Download presentation
• 08:45-09:45: Specialized talks
  • Virtual platforms: efficient hardware/software simulation and new virtualization techniques
    Frédéric Pétrot, Grenoble INP, TIMA Laboratory
    Download presentation
    Virtual prototyping aims 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 these processors. This approach relies on specific modeling techniques and can be carried out at different levels of abstraction so that trade-offs between speed and accuracy can be made. This presentation details the challenges faced by virtual prototyping methods and introduces commonly accepted abstraction levels. We will focus in particular on techniques utilizing dynamic binary translation and its integration within SystemC, the current standard for digital component modeling.
  • Contribution of formal methods
    David Monniaux, CNRS, VERIMAG Laboratory
    Download presentation
    In addition to simulation analyses, numerous methods provide the capability to reason formally on a system model in order to verify various properties (functional correctness, absence of deadlocks, compliance with real-time constraints, rigor of memory accesses, etc.). These methods rely on diverse 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, along with the current state of associated methods and tools.
• 09:45-10:00: Conclusion
  Summary of collaboration methods, LabEx teams, and master's programs related to this topic
  Download presentation
• 10:00-10:30: Discussion session (can be extended until 11:00 AM for those who wish)