·Home
·Table of Contents
·Reliability and Validation 1

Preparing Testing by Proving Critical Systems

D. Rouillard, R. Castanet, P.Castéran, P. Félix
Labri, UMR 5800, Université Bordeaux 1,
33405 Talence Cedex, France
Contact

Abstract

1 Introduction

2 A proof assistant as entry point

3 The CClair environment

Fig 2: a simple transition system:the Digicode

4 The verification activity

5 Conclusion

References

  1. Berard Béatrice and Laurent Fribourg. Automated verification of a parametric real-time program: The ABR conformance protocol.Lecture Notes in Computer Science, 1633:96-107, 1999.
  2. Pierre Cast ran and Davy Rouillard. Introduction to CClair (draft). Rapport technique, LaBRI, December 1999. www.dept-info.labri.u-bordeaux.fr/~casteran/CClair/Tutorial.ps.
  3. A. Cavalli and All. Engendrer des tests pour un vrai protocole, grâce à des techniques éprouvées de vérification. CFIP'96, 1996.
  4. M. Clatin, R. Groz, M. Phalippou, and R. Thummel. Two approaches linking a test generation tool with verification techniques. Protocol Test systems, VIII, 1995.
  5. M. Dubuc, G. Bochmann, and R. Dssouli. TESTL : An environment for incremental test suite design based on fsm. 4 th IWPTS,Leidschendam, 1991.
  6. J.C. Fernandez, C. Jard, T. Jéron, and G. Viho. Using on-the-fly verification techniques for the generation of test suites. CAV'96, July 1996.
  7. J. Grabowski. Test case generation and test case specification with MSC. PhD thesis, University of Bern, 1994.
  8. Christine Paulin-Mohring. The coq project, 1999. http://coq.inria.fr.
  9. Lawrence C. Paulson. The Isabelle reference manual. Technical Report 283, University of Cambridge, Computer Laboratory, 1993.
  10. Lawrence C. Paulson. Isabelle's object-logics. Technical Report 286, University of Cambridge, Computer Laboratory, 1993.
  11. R.Castanet, C.Chevrier, O.Koné , and B. Le Saec. An adaptative test sequence generation method for the users needs.Protocol Test Systems VIII, 1995.
  12. Philippe Schnoebelen et al. Vérification de logiciels, Techniques et outils du model-checking. Vuibert (France), 1999.
  13. Daryl Stewart. The hol system, 1998.http://www.cl.cam.ac.uk/Research/HVG/HOL.

© AIPnD , created by NDT.net |Home|    |Top|