Posts
-
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...
Read more → -
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...
Read more → -
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...
Read more → -
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...
Read more →
Subscribe via RSS.