Formalization of Software Testing Criteria using the strongZstrong.pdfVIP

Formalization of Software Testing Criteria using the Z Notation Sergiy A. Vilkomir Jonathan P. Bowen South Bank University, Centre for Applied Formal Methods School of Computing, Information Systems and Mathematics 103 Borough Road, London SE1 0AA, UK {vilkoms, bowenjp}@sbu.ac.uk http://www.cafm.sbu.ac.uk/ Abstract criteria, although the combination of the two has been con- sidered [24, 31]. Data-flow criteria are based on the investi- This paper describes an approach to formalization of crite- gation of the ways in which values are associated with vari- ria of computer systems software testing. A brief review of ables and how these associations can affect the execution of control-flow criteria is introduced. As a formal language for the program [36]. This group contains so-called all-uses, describing the criteria, the Z notation is selected. Z schemas all-defs, all-p -uses and other criteria [14, 27]. Control-flow are presented for definitions of the following criteria: state- criteria examine logical expressions, which determine the ment coverage, decision coverage, condition coverage, de- branch and loop structure of the program. This group of cision/condition coverage, full predicate coverage, modified criteria is considered in this paper. condition/decision coverage, and multiple condition cover- The paper is structured as follows. Section 2 presents age. This characterization could help in the correct under-