Skip to Main content Skip to Navigation
Journal articles

Combining formal verification and conformance testing for validating reactive systems

Vlad Rusu 1
1 DART - Contributions of the Data parallelism to real time
LIFL - Laboratoire d'Informatique Fondamentale de Lille, Inria Lille - Nord Europe
Abstract : This paper presents a combination of verification and conformance testing techniques to support the formal validation of reactive systems. The idea is to use symbolic test selection techniques to extract subgraphs (components) from a specification, and to perform the verification on the components rather than on the whole specification. Under reasonable sufficient conditions, this constitutes a sound compositional verification technique, in the sense that a property verified on the components also holds on the whole specification. This may considerably reduce the global verification effort. Moreover, once verified, a component forms the basis of an adequate test case, i.e. when executed on an implementation, it will not issue false positive or negative verdicts with respect to the verified properties. The approach has been implemented using the STG test selection tool and the PVS theorem prover. It is demonstrated here on a smart‐card application: the Common Electronic Purse System.
Document type :
Journal articles
Complete list of metadata

https://hal.inria.fr/inria-00527591
Contributor : Mister Dart <>
Submitted on : Tuesday, October 19, 2010 - 4:21:33 PM
Last modification on : Wednesday, June 30, 2021 - 9:58:04 AM

Links full text

Identifiers

Collections

Citation

Vlad Rusu. Combining formal verification and conformance testing for validating reactive systems. Journal of : Software Testing, Verification and Reliability, Wiley, 2003, 13 (3), pp.157-180. ⟨10.1002/stvr.274⟩. ⟨inria-00527591⟩

Share

Metrics