TRUFAL - Trust via Failed Falsification of Complex Dependable Systems Using Automated Test-Case Generation through Model Mutation

Todays dependable computer-based infrastructures rapidly grow in complexity due to a continuous evolution towards very large, heterogeneous, highly dynamic and ubiquitous computer systems. This trend of a growing complexity is a serious challenge to the task of engineering trustworthy systems: the more complex a system is, the more difficult is the verification of the fulfilment of its dependability requirements. It seems that despite the many advances in automated verification, the demand for new features and flexibility always creates systems that provide the next barrier for auto- mated verification. Where verification is not possible to establish trust, Sir Popper proposed falsification. TRUFAL will implement this idea by applying mutation analysis to the modelling level, leading to a new form of fault-oriented model-based testing. Mutation testing is strongly related to safety and security testing. Today, no commercial tools exist that combine mutation testing and model-based testing. One reason is the complexity of the algorithms behind mutation testing (equivalent mutant problem). The aim is to develop such a new test case generator that is able to handle models of industrial scale. We will exploit the newest results and techniques from formal methods: formal intermediate models, model decomposition and concolic (concrete and symbolic) execution. This tool, together with domain specific fault models, will be integrated in the quality assurance process of our industrial partners in the safety-critical transportation domain: automotive and railways, which in a mid-term range can lead to improvement of their development processes. The objective is to reduce their testing efforts by at least 10% while providing a measurable and scientifically defendable statement of trust in their systems in terms of fault coverage. All techniques will be well-founded in scientific theory.