Towards MC/DC coverage of properties specification patterns

Abstract

Model based testing is used to validate the actual system against its requirements described as formal specification,while formal verification proves that a requirement is not violated in the overall system. Verifying properties,in certain cases,becomes very expensive (or unpractical),mainly when the application of test techniques is enough for the users purposes. The Modified Condition/Decision Coverage (MC/DC),used in the avionics software industry,is recognised as a good technique to find out the possible mistakes on programs logics because it covers how each condition can affect the programs’ decisions outcomes. It has also been adapted to provide the coverage of specifications in the requirements-based approach. This paper proposes a technique to decompose properties (specifications),defined as regular expressions,into subexpressions representing test cases to cover the MD/DC for specifications (Unique First Word Recognition). Then,instead of proving an entire property,we can use a model checker to observe and select program executions that cover all the test cases given as the subexpressions. To support this approach,we give a syntactic characterisation of the properties decomposition,inductively defined over the syntax of regular expressions,and show how to use the technique to decompose Specification Patterns (SPS) and monitor their satisfiability using the Java PathFinder (JPF).