Applied formal testing

该研究项目的目标是调整一些正式测试技术，以更好地处理一些现实生活的需求。许多形式化的测试技术都是针对所谓的“调试技术”：目标是满足一些给定的标准（所有路径，所有代码，所有def-use和许多其他标准），或者在一些特定的假设下发现每个错误（检查序列生成）。然而，在实践中，不平凡的应用程序只是不希望是无故障的，因此，一个现实的测试活动的目的不能发现所有的故障。鉴于只有一些错误会被发现，那么质疑哪些错误会被测试方法发现是有意义的。还期望将检测指向“良好”故障。

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.