Formal mutation testing for Circus

详细信息    查看全文

• 作者：Alex Alberto ; ^a ; ^{alexdba@gmail.com" class="auth_mail" title="E-mail the corresponding author} ; Ana Cavalcanti^b ; Marie-Claude Gaudel^c ; Adenilso Simã ; o^a
• 关键词：Circus ; Mutation ; Testing ; Formal specification
• 刊名：Information and Software Technology
• 出版年：2017
• 出版时间：January 2017
• 年：2017
• 卷：81
• 期：Complete
• 页码：131-153
• 全文大小：2414 K

文摘

class="boldFont">Context: The demand from industry for more dependable and scalable test-development mechanisms has fostered the use of formal models to guide the generation of tests. Despite many advancements having been obtained with state-based models, such as Finite State Machines (FSMs) and Input/Output Transition Systems (IOTSs), more advanced formalisms are required to specify large, state-rich, concurrent systems. class="sansserif">Circus, a state-rich process algebra combining Z, CSP and a refinement calculus, is suitable for this; however, deriving tests from such models is accordingly more challenging. Recently, a testing theory has been stated for class="sansserif">Circus, allowing the verification of process refinement based on exhaustive test sets.

class="boldFont">Objective: We investigate fault-based testing for refinement from class="sansserif">Circus specifications using mutation. We seek the benefits of such techniques in test-set quality assertion and fault-based test-case selection. We target results relevant not only for class="sansserif">Circus, but to any process algebra for refinement that combines CSP with a data language.

class="boldFont">Method: We present a formal definition for fault-based test sets, extending the class="sansserif">Circus testing theory, and an extensive study of mutation operators for class="sansserif">Circus. Using these results, we propose an approach to generate tests to kill mutants. Finally, we explain how prototype tool support can be obtained with the implementation of a mutant generator, a translator from class="sansserif">Circus to CSP, and a refinement checker for CSP, and with a more sophisticated chain of tools that support the use of symbolic tests.

class="boldFont">Results: We formally characterise mutation testing for class="sansserif">Circus, defining the exhaustive test sets that can kill a given mutant. We also provide a technique to select tests from these sets based on specification traces of the mutants. Finally, we present mutation operators that consider faults related to both reactive and data manipulation behaviour. Altogether, we define a new fault-based test-generation technique for class="sansserif">Circus.

class="boldFont">Conclusion: We conclude that mutation testing for class="sansserif">Circus can truly aid making test generation from state-rich model more tractable, by focussing on particular faults.