Explanation of Counterexamples in the Context of Formal Verification

• Main Author: Ek, Alexander
• Format: Others
• Language: English
• Published: Uppsala universitet, Institutionen för informationsteknologi 2016
• Online Access: http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-301330

With the current rapid computerisation and automation of systems, which were previously controlled manually, a growing demand for measures to ensure correctness of systems is arising. This can be achieved with formal verification. With formal verification, systems can be proved to satisfy, or not satisfy, a set of given properties. In cases where a system does not satisfy the given properties, a counterexample is presented, but counterexamples are, more often than not, hard to interpret manually. Thus, automatic procedures for explaining counterexamples are needed but unfortunately few. This thesis will focus on the explanation of counterexamples from failed formal verifications of systems. An algorithm for doing such is presented in this thesis. This algorithm is shown to give desired explanations for some cases whilst just the bare minimum for the majority of cases. A number of procedures to obtain the latter are already known. However, a small problem, left unsolved, can bring desired explanations to the majority of cases if solved. The presented algorithm is, unfortunately, not free from flaws nor errors, but it is still unclear how severe these are.