Applied formal testing

点击翻译按钮获取中文摘要

This research project goal is to adapt some of the techniques of formal testing to better handle some real-life requirements. Many formal testing techniques are directed towards what is sometimes called "debug techniques": the goal is to fulfill some given criteria (all paths, all code, all def-use and many others), or uncover every faults under some specific assumptions (checking sequence generation). However, in practice non trivial applications are simply not expected to be fault-free, thus the purpose of a realistic testing campaign cannot be to uncover all faults. Given that only some of the faults will be found, it only makes sense to question which ones will be uncovered by a testing method. It is also desirable to direct the detection towards the "good" faults.