Anzeige
Erschienen in:
2016 | OriginalPaper | Buchkapitel
Towards MC/DC Coverage of Properties Specification Patterns
verfasst von : Ana C. V. de Melo, Corina S. Păsăreanu, Simone Hanazumi
Erschienen in: Theoretical Aspects of Computing – ICTAC 2016
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. 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).