Applied formal testing

这个研究项目的目标是调整一些正式测试的技术，以更好地处理一些现实生活中的需求。许多正式的测试技术都指向有时被称为“调试技术”的方向：目标是满足某些给定的标准（所有路径、所有代码、所有defuse和许多其他标准），或者在某些特定假设下发现每个错误（检查序列生成）。然而，在实践中，重要的应用程序并不期望是无故障的，因此实际测试活动的目的不可能是发现所有的故障。假设只有一些错误会被发现，那么只有质疑哪些错误会被测试方法发现才是有意义的。将检测指向“好”故障也是可取的。

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.