Posts

Dec 20, 2017
Automated Test Generation of MC/DC (part 2)
In the previous post (part 1) we have introduced the concept of MC/DC which finds application in the verification of avionics and automotive applications. In this post we show how to generate MC/DC tests starting from a Simulink or a Lustre specification, using Intrepyd. Highlights QA for avionics critical software (DO-178C) The MC/DC coverage metric...

Nov 20, 2017
Automated Test Generation of MC/DC (part 1)
In this post (and its companion part 2) we show how to automatically generate tests from a Simulink or Lustre specification using Intrepyd. The tests will provide full coverage using the Modified Condition/Decision Coverage (MD/DC from now on), which is of paramount importance in the avionics domain. The focus of this post is on the...

Oct 20, 2017
Machine-precise Verification of Simulink Models
In this post we show how to use Intrepyd (repo) to translate and verify MathWorks Simulink models. The translation is such that the semantic is machine-precise, i.e., we verify properties by taking into account finite integers and floating-point representations for integers and single or double precision variables, which is something that, at the time of...

Sep 20, 2017
Machine-precise Verification of Lustre Specifications
In this post we show how to use Intrepyd (repo) to translate and verify Lustre specifications. The translation is such that the semantic is machine-precise, i.e., we verify properties by taking into account finite integers and floating-point representations for integers and real variables respectively, which is something that, to the best of our knowledge, is...