A Typical Testing Problem: Validating WML Cellphones

Abstract

I will present in my talk a problem typical for the activity of telecommunications operators where formal methods should bring some help: validating equipment (for example, cellphones) which is supposed to act as an interpreter for an XML-like language (in that case, WML, a script language for the WAP protocol). Testing interpreters suppose that test scripts have to be separated in two parts: a data part which is a program in the interpreted language, and a script part which describes what the interpreted program is supposed to do if it is correctly interpreted. The data part is very often reduced to very simple programs exercising only one feature of the language, and the script part is then informal, in general a description in natural language. This does not enable to exercise combinations of features of the interpreted language. To change this situation, it would be necessary to encode in some way the semantics of the interpreted language. From that encoding, and from a significant program in the interpreted language, automatic test generation tools derived from model-checking technology will provide test suites of hopefully better quality.