Presentation title

Simulation-Based Formal Verification of Onboard Software: a case study

Authors

Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti and Enrico Tronci

Institution(s)

Model Checking Lab, Sapienza University of Rome

Presentation type

Technical presentation

Abstract

System level verification of Cyber-Physical Systems (CPSs) has the goal of verifying that the whole (i.e., software + hardware) system meets the given specifications. Model checkers for hybrid systems cannot handle system level verification of actual systems. Thus, Hardware In the Loop Simulation (HILS) is currently the main workhorse for system level verification. By using model checking driven exhaustive HILS, System Level Formal Verification (SLFV) can be effectively carried out for actual systems.

In [1] we have presented a parallel random exhaustive HILS based model checker for hybrid systems (called SyLVer) that, by simulating all operational scenarios exactly once in a uniform random order, is able to provide, at any time during the verification process, an upper bound to the probability that the System Under Verification exhibits an error in a yet-to-be-simulated scenario (Omission Probability).

In this talk we show on-going research on the application of SyLVer technology to the MATLAB-Simulink model for the Apollo Lunar Module digital autopilot.

---

Additional material

• Presentation slides: [pdf]
• Full paper [1]:

  Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti, and Enrico Tronci
  Anytime system level verification via parallel random exhaustive hardware in the loop simulation.
  Microprocessors and Microsystems 41, pages 12–28, 2016.

For more details on this presentation please click the button below: