Abstract
Test generation is a program-synthesis problem: starting from the formal specification of a system under test, and from a test purpose describing a set of behaviours to be tested, compute a reactive program that observes an implementation of the system to detect non- conformant behaviour, while trying to control it towards satisfying the test purpose. In this paper we describe an approach for generating sym- bolic test cases, in the form of input-output automata with variables and parameters.
The specifications and proofs for the example treated in the paper can be found at http://www.irisa.fr/pampa/perso/rusu/IFM00/.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
A. Belinfante, J. Feenstra, R. de Vries, J. Tretmans, N. Goga, L. Feijs, and S. Mauw. Formal test automation: a simple experiment. In International Workshop on the Testing of Communicating Systems (IWTCS’99), pp 179–196, 1999.
S. Bensalem, Y. Lakhnech, and S. Owre. Computing abstractions of infinite state systems sompositionally and automatically. In Computer-Aided Verification (CAV’98), LNCS 1427, pp 319–331, 1998.
G. Bernot, M. C. Gaudel, and B. Marre. Software testing based on formal specifications: a theory and a tool. Software Engineering Journal 6(6), pp 387–405, 1991.
M. Bozga, J-C. Fernandez, and L. Ghirvu. Using static analysis to improve automatic test generation. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS’00), LNCS 1785, pp 235–250, 2000.
E. Brinskma. A theory for the derivation of tests. In Protocol Specification, Testing, and Verification (FORTE/PSTV’98), pp 63–74, 1998.
J.-C. Fernandez, C. Jard, T. Jéron, and C. Viho. An experiment in automatic generation of test suites for protocols with verification technology. Science of Computer Programming, 29 (1-2): 123–146, 1997.
N. Halbwachs, Y. E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2): 157–185, 1997.
L. Helmink, M. P. A. Sellink, and F. Vaandrager. Proof-checking a data link protocol. In Types for Proofs and Programs, International Workshop (TYPES’94), LNCS 806, pp 127–165, 1994.
T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: A Model Checker for Hybrid Systems. Software Tools for Technology Transfer 1:110–122, 1997.
C. A. R. Hoare. Communicating sequential processes. Prentice Hall International Series in Computer Science, 1985.
ISO/IEC. International Standard 9646-1/2/3, OSI-Open Systems Interconnection, Information Technology-Open Systems Interconnection Conformance Testing Methodology and Framework, 1992.
C. Jard, T. Jéron and P. Morel. Verification of test suites. To appear in International Conference on the Testing of Communicating Systems (TestCom’00), 2000.
T. Jéron and P. Morel. Test generation derived from model-checking. In Computer-Aided Verification (CAV’99), LNCS 1633, pp 108–122, 1999.
N. Klarlund and M. Schwartzbach. A Domain-Specific Language for Regular Sets of Strings and Trees. IEEE Transactions On Software Engineering 25(3):378–386, 1999.
N. Lynch and M. Tuttle. An introduction to input/output automata. CWI Quarterly, 3(2), 1999.
J. Tretmans. Test generation with inputs, outputs and quiescence. Software-Concepts and Tools, 17(3):103–120, 1996.
S. Owre, J. Rusby, N. Shankar, and F. von Henke. Formal verification of faulttolerant architectures: Prolegomena to the design of pvs. IEEE Transactions on Software Engineering, 21(2): 107–125, 1995.
P. J. Ramadge, and W. M. Wonham. Supervisory Control of a Class of Discrete-Event Processes. SIAM Journal of Control and Optimization, 25(1):206–230, 1987.
S. Rapps and E. Weyuker. Selecting software test data using data flow information. IEEE Transactions on Software Engineering, 11(4):367–375, 1985.
R. Shostak. A practical decision procedure for arithmetic with function symbols. Journal of the ACM, 26(2): 351–360, 1979.
International Telecommunications Union. B-ISDN SAAL Service-Specific Connection-Oriented Protocol. ITU-T Recommendation Q.2110, 1994.
F. Tip. A survey of program slicing techniques. Technical Report CS-R9438, Centrum voor Wiskunde en InformatIca, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rusu, V., du Bousquet, L., Jéron, T. (2000). An Approach to Symbolic Test Generation. In: Grieskamp, W., Santen, T., Stoddart, B. (eds) Integrated Formal Methods. IFM 2000. Lecture Notes in Computer Science, vol 1945. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-40911-4_20
Download citation
DOI: https://doi.org/10.1007/3-540-40911-4_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41196-3
Online ISBN: 978-3-540-40911-3
eBook Packages: Springer Book Archive