Advertisement
Published in:
2016 | OriginalPaper | Chapter
Towards MC/DC Coverage of Properties Specification Patterns
Authors : Ana C. V. de Melo, Corina S. Păsăreanu, Simone Hanazumi
Published in: Theoretical Aspects of Computing – ICTAC 2016
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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).