Abstract
We present a test case generation method which conciliates theorem proving and model checking. Test purposes are expressed by timed regular expressions and then translated into a corresponding automaton using a certified function. This automaton is composed with the system specification and an execution is computed from this sub-specification by an automatic tool. The result is finally re-injected into the theorem prover to be checked.
Research partially supported by the French government for the RNRT project Calife.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-0-387-35497-2_31
Chapter PDF
Similar content being viewed by others
References
R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138 (1): 3–34, 1995.
R. Alur, T. A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. In Proceedings of the 14th Annual Real-time Systems Symposium, pages 2–11. IEEE Computer Society Press, 1993.
Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, and Pei-Hsin Ho. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. Lecture Notes in Computer Science, 736: 209–229, 1993.
B. Baumgarten. Timed systems behaviour and conformance testing - a mathematical framework. In Proc. 8th PTS, 1995.
B.Bérard, P.Castéran, E.Fleury, JF.Monin L.Fribourg, C.Paulin, A.Petit, and D.Rouillard. Automates temporisés calife, 2000. http://www.loria.fr/projets/calife/.
B. Bérard, L. Fribourg, F. Klay, and J.-F. Monin. A compared study of two correctness proofs for the standardized algorithm of ABR conformance. Research Report LSV-99–7, LSV, ENS de Cachan, Cachan, France, August 1999. 27 pages.
P. Castéran and Davy Rouillard. Reasoning about parametrized automata. In Proceedings, 8 th International Conference on Real-Time System, volume 8, pages 107–119, 2000.
Pierre Castéran and Davy Rouillard. The eclair project, 1999. http://dept-info.labri.u-bordeaux.fr/Thasteran/CClair/.
E. Allen Emerson. Handbook of Theoretical Computer Science (volume B), chapter Temporal and Modal Logic, pages 995–1072. Elsevier, 1990.
A. Forum. Atm forum traffic management specification version, 1996.
T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HYTECH: A model checker for hybrid systems. Lecture Notes in Computer Science, 1254: 460–463, 1997.
T. Higashino, A. Nakata, K. Taniguchi, and A. Cavalli. Generating test cases for a timed i/o automaton model. In Proc. IFIP Int’l Work. Test Communicat. Syst. (IWTCS), pages 197–214. G. Csopaki, S. Dibuz, and K. Tarnay eds, 1999.
ISO. Information technology, open systems interconnection, conformance testing methodology and framework. International Standard IS-9646, CCITT X.290-X. 294, 1991.
Jean-François Monin and Francis Klay. Correctness proof of the standardized algorithm for ABR conformance. In FM’99, volume 1708 of Lecture Notes in Computer Science, pages 662–681. Springer, 1999.
Tobias Nipkow. Verified lexical analysis. In J. Grundy and M. Newey, editors, Proc. of the 11th International Conference on Theorem Proving in Higher Order Logics, pages 1–15. Springer-Verlag LNCS 1479, 1998.
Christine Paulin-Mohring. The coq project, 1999. http://coq.inria.fr.
Lawrence C. Paulson. The Isabelle reference manual. Technical Report 283, University of Cambridge, Computer Laboratory, 1993.
Lawrence C. Paulson. Mechanizing coinduction and corecursion in higher-order logic. J. Logic and Computation, 7: 175–204, 1997.
Davy Rouillard. Le modèle des p-automates dans CClair. Technical Report 1242–00, LaBRI, 2000.
N. Shankar, S. Owre, and J. Rushby. The pvs proof checker: A reference manual. Technical report, CSL, SRI International, Menlo Park CA, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Castanet, R., Rouillard, D. (2002). Generate Certified Test Cases by Combining Theorem Proving and Reachability Analysis. In: Schieferdecker, I., König, H., Wolisz, A. (eds) Testing of Communicating Systems XIV. IFIP — The International Federation for Information Processing, vol 82. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35497-2_19
Download citation
DOI: https://doi.org/10.1007/978-0-387-35497-2_19
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-6705-6
Online ISBN: 978-0-387-35497-2
eBook Packages: Springer Book Archive