OSMOSE: automatic structural testing of executables. Verification is usually performed on a high-level view of the software, either specification or program source code. However, in certain circumstances verification is more relevant when performed at the machine-code level. This paper focuses on automatic test data generation from a stand-alone executable. Low-level analysis is much more difficult than high-level analysis since even the control-flow graph is not available and bit-level instructions have to be modelled faithfully. The paper shows how ‘path-based’ structural test data generation can be adapted from structured language to machine code, using both state-of-the-art technologies and innovative techniques. The results have been implemented in a tool named OSMOSE and encouraging experiments have been conducted.
Keywords for this software
References in zbMATH (referenced in 5 articles , 1 standard article )
Showing results 1 to 5 of 5.
- Chihani, Zakaria; Marre, Bruno; Bobot, François; Bardin, Sébastien: Sharpening constraint programming approaches for bit-vector theory (2017)
- Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015) ioport
- Brauer, Jörg; King, Andy: Transfer function synthesis without quantifier elimination (2012)
- Bardin, Sébastien; Herrmann, Philippe: OSMOSE: automatic structural testing of executables (2011) ioport
- Bardin, Sébastien; Herrmann, Philippe; Védrine, Franck: Refinement-based CFG reconstruction from unstructured programs (2011)