Test Cases Generation from CTL. A Methodology
YANG ; GHAZEL ; EL-KOURSI
Type de document
COMMUNICATION AVEC ACTES INTERNATIONAL (ACTI)
Langue
anglais
Auteur
YANG ; GHAZEL ; EL-KOURSI
Résumé / Abstract
A formal test design technique has strict rules on how the test cases must be derived. Generally, a formal specification, which is precise, complete, consistent and unambiguous, is needed as a basis for formal testing. Various formal methods in testing have been developed in the last 50 years. Most of these methods are based on formal notations such as FSM, LTS, etc. which are graphical and easy to understand by developers and users for performing a black box testing process. However, temporal logics are rarely used as a formal specification basis to generate test cases for black box testing, as their semantics are relatively abstract. This paper discusses a methodology on how to generate test cases from specifications expressed in temporal logic CTL. Firstly, user requirements concerning the safety aspects are refined then formalized into CTL safety properties. CTL formulas are then encoded as µ-calculus formulas. These µ-calculus formulas are then transformed into automata by using control synthesis techniques. In the last step, transitions based coverage are defined to generate testing cases from automata.
