Using Refinement Checking as System Testing

Abstract. 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 port; 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. Key words: System Testing, Ref...

• Type: Conference
• Year: 2008
• Where: CIBSE
• Authors: Cristiano Bertolini, Alexandre Mota
• Keywords: Automatic Verification Approach, CIBSE 2008, Refinement Checker Fdr, Software Engineering, Specification Language Csp