Recent Work

(and some not so recent any more...)

I've been working together with Lydie du Bousquet, Duncan Clarke, Thierry Jéron, and Elena Zinovieva on symbolic test generation. This paper presented at the Integrated Formal Methods 2000 conference describes the theory of symbolic test generation. A prototype tool called STG implements the approach. We've used STG to generate and execute symbolic test cases for a simple smart-card application: the Common Electronic Purse System (CEPS). We have presented this paper at the e-Smart 2001 conference. This short one (in TACAS'02) presents the tool.

I've also been doing some work on deductive verification (a simple example: the sliding-window protocol with PVS, FORTE'01) and how to to it more automatically, cf. same protocol using PVS and supplementary decision procedures (TPHOLs'01), and a larger example : the CEPS (VCL'02).

This paper (initially in Formal Methods Europe (FME'02), extended version to appear in Journal of Software Testing, Verification, and Reliability 13(3) : Sept. 2003) is about integrating symbolic test generation with STG and deductive verification with PVS. This one (to appear in Formal Methods (FM'03)) presents a methodology based on compositionality, abstraction, and theorem-proving (PVS), which was successfully applied to verify a quite large specification of an ATM protocol (details here).

In the Vertecs project we are studying the interactions between verification, control synthesis, and test generation . This paper (in French, to appear in Modélisation des systèmes réactifs, MSR'03) presents our initial results, while this one (in English, to appear in 42nd IEEE Conference on Decision and Control (CDC'03)) takes a more general approach.

An upcoming paper (to appear in TestCom'04) shows how to generate conformance test cases directly from a specification and the safety properties that it satisfies. This allows for an automatic, seamless, and sound validation process between safety requirements, operational specifications, and black-box implementations of finite-state systems.

A collaboration with members of the Lande project of Irisa has resulted in generating a correct-by-construction dataflow analyser for a relevant subset of JavaCard, using the Coq proof assistant (paper to appear at ESOP'04).

Vlad Rusu