Verification of Formal Requirements through Tracing

Abstract: Software development in the railway application is governed by strict standards which aim to ensure safety. It is for example highly recommended to use formal methods when specifying requirements. Moreover, it is mandatory to have certain roles be fulfilled by different people. A common technique is developing software tests for the requirements. Making sure that software requirements are properly described, interpreted and implemented by different people is a major challenge. Tests fully depend on the tester to cover all scenarios. Having more methods that simplify requirement tracing and that depends less on thoroughness of the tester would provide many benefits. This thesis investigates whether and how software tracing can be used to validate formal requirements of software. The goal is to perform trace validation such that it can be used to complement more traditional verification techniques. By verifying formal requirements on traces, the detection of errors depends on the events in the traces. As a consequence, more traces provide a higher chance of detecting errors. Thereby eliminating risk of the tester missing important cases. The presented verification approach firstly specifies requirements in linear temporal logic and converts this specification to a non-deterministic Büchi automaton, or a finite state machine which is also evaluated. Secondly, the approach describes several alternatives for collecting traces and how to link those to the formal specification. Lastly, the verification approach proposes an algorithm which takes the Büchi automaton and a trace to detect violations of the requirement. The validation approach is implemented in form of multiple tools and its operation shown by means of a toy example. This example models a railway application such that its requirements can be verified using the tools. The results are then used to show how these tools can be used in an actual railway application. Using these research outcomes, and the stand-alone tool, an implementation in Trace Compass is created. This can, just like the stand-alone tool, decide for each pair of trace and requirement whether the trace violates the requirement.