A Strategy for Automatic Conformance Testing in Embedded Systems

Software testing is an expensive and time-consuming activity; it is also error-prone due to human factors. But, it still is the most common effort used in the software industry to achieve an acceptable level of quality for its products. An alternative is to use formal verification approaches, although they are not widespread in industry yet. This paper proposes an automatic verification approach to aid system testing based on refinement checking, where the underlying formalisms are hidden from the developers. Our approach consists in using a controlled natural language (a subset of English) to describe requirements (where it is automatically translated into the formal specification language CSP) and extracting a model directly from a mobile phone using a developed tool support; these artifacts are normalized in the same abstraction level and compared using the refinement checker FDR. This approach is being used at Motorola; the source of our case study.