A framework and tool support for the systematic testing of model-based specifications

Miller, T. and Strooper, P. (2003) A framework and tool support for the systematic testing of model-based specifications. Acm Transactions On Software Engineering And Methodology, 12 4: 409-439.


Author Miller, T.
Strooper, P.
Title A framework and tool support for the systematic testing of model-based specifications
Journal name Acm Transactions On Software Engineering And Methodology  (ERA 2012 Listed)    (ERA 2010 Rank A*)   Check publisher's open access policy
Publication date 2003
Sub-type Article
DOI 10.1145/990010.990012
Volume number 12
Issue number 4
ISSN 1049-331X
Start page 409
End page 439
Total pages 31
Editor Ghezzi, C.
Place of publication New York
Publisher ACM
Collection year 2003
Language eng
Subject C1
280302 Software Engineering
700199 Computer software and services not elsewhere classified
Abstract Formal specifications can precisely and unambiguously define the required behavior of a software system or component. However, formal specifications are complex artifacts that need to be verified to ensure that they are consistent, complete, and validated against the requirements. Specification testing or animation tools exist to assist with this by allowing the specifier to interpret or execute the specification. However, currently little is known about how to do this effectively. This article presents a framework and tool support for the systematic testing of formal, model-based specifications. Several important generic properties that should be satisfied by model-based specifications are first identified. Following the idea of mutation analysis, we then use variants or mutants of the specification to check that these properties are satisfied. The framework also allows the specifier to test application-specific properties. All properties are tested for a range of states that are defined by the tester in the form of a testgraph, which is a directed graph that partially models the states and transitions of the specification being tested. Tool support is provided for the generation of the mutants, for automatically traversing the testgraph and executing the test cases, and for reporting any errors. The framework is demonstrated on a small specification and its application to three larger specifications is discussed. Experience indicates that the framework can be used effectively to test small to medium-sized specifications and that it can reveal a significant number of problems in these specifications.
Keyword Computer Science, Software Engineering
Verification
Formal Verification
Specification Animation
Testgraphs
Testing
Programs
Q-Index Code C1

 
Versions
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 6 times in Thomson Reuters Web of Science Article | Citations
Scopus Citation Count Cited 7 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Access Statistics: 34 Abstract Views  -  Detailed Statistics
Created: Wed, 15 Aug 2007, 02:28:02 EST