Abstract
Applying formal methods to testing has recently become a popular research topic. In this paper we explore the opposite approach, namely, applying testing techniques to formal verification. The idea is to use symbolic test generation to extract subgraphs (called components) from a specification and to perform the verification on the components rather than on the whole system. This may considerably reduce the verification effort and, under reasonable sufficient conditions, a safety property verified on a component also holds on the whole specification. We demonstrate the approach by verifying an electronic purse system using our symbolic test generation tool STG and the PVS theorem prover.
This is a preview of subscription content, log in via an institution to check access.
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
P. Ammann and P. Black. Abstracting formal specifications to generate software tests via model checking. In Digital Avionics Systems Conference, DASC’99. Also a National Institute of Research and Technology research report, NIST-IR 6405.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill and J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, 1992.
T. Ball, R. Majumdar, T. Millstein, and S.K. Ramajani. Automatic predicate abstraction of C programs. ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI’01, pages 203–213.
A. Belinfante, J. Feenstra, R. de Vries, J. Tretmans, N. Goga, L. Feijs, and S. Mauw. Formal test automation: a simple experiment. Int. Workshop on the Testing of Communicating Systems, IWTCS’99, pages 179–196.
S. Bensalem, V. Ganesh, Y. Lakhnech, C. Munoz, S. Owre, H. Rueß, J. Rushby, V. Rusu, H. Saïdi, N. Shankar, E. Singerman, and A. Tiwari. An overview of SAL. LFM 2000: NASA Langley Formal Methods Workshop, LFM’00, pages 187–196.
S. Bensalem and Y. Lakhnech. Automatic generation of invariants. Formal Methods in System Design, 15(1):75–92, 1999.
CEPS: Common Electronic Purse System. http://www.cepsco.org.
D. Clarke, T. Jéron, V. Rusu, and E. Zinovieva. Automated test and oracle generation for smart-card applications. Conference on Research in Smart Cards, eSmart’01, pages 58–70. LNCS 2140.
D. Clarke, T. Jéron, V. Rusu, and E. Zinovieva. stg: a Symbolic Test Generation tool. Tools and Algorithms for the Construction and Analysis of Systems (TACAS’02), pages 470–475. LNCS 2280.
J-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu. CADP: A protocol validation and verification toolbox. Computer-Aided Verification, CAV’96. LNCS 1102.
C. Flanagan and S. Qadeer. Predicate Abstraction for Software Verification. To appear in Principles of Program Design, POPL’ 02.
S. Graf and H. Saïdi. Construction of abstract state graphs with PVS. Computer Aided Verification, CAV’97, pages 72–83. LNCS 1254.
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.
J. Hatcliff and M. Dwyer, Using the Bandera tool set to model-check properties of concurrent Java software. Concurrency Theory, CONCUR’01, pages 39–59. LNCS 2154.
K. Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. Formal Methods Europe, FME’96, pages 662–681. LNCS 1051.
T.A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy Abstraction. To appear in Principles of Program Design, POPL’ 02.
G.J. Holzmann. Design and validation of communication protocols. Prentice Hall, 1991.
ISO/IEC. International Standard 9646, OSI-Open Systems Interconnection, Information Technology-Conformance Testing Methodology and Framework, 1992.
R.S Lazić, T.C. Newcomb, and A.W. Roscoe. On model checking data-independent systems with arrays without reset. Oxford University Computing Laboratory, Research Report RR-02-02.
T. Jéron and P. Morel. Test generation derived from model-checking. Computer-Aided Verification, CAV’99, pages 108–122. LNCS 1633.
S. Owre, J. Rusby, N. Shankar, and F. von Henke. Formal verification of fault-tolerant architectures: Prolegomena to the design of pvs. IEEE Transactions on Software Engineering, 21(2): 107–125, 1995.
V. Rusu. Verifying a sliding-window protocol using PVS. In Formal Techniques for Networked and Distributed Systems, FORTE’01, pages 251–266. Kluwer Academic Publishers, 2001.
V. Rusu, L. du Bousquet, and T. Jéron. An approach to symbolic test generation. Conference on Integrating Formal Methods (IFM’00), pages 338–357. LNCS 1945.
H. Saïdi and N. Shankar. Abstract and model check while you prove. Computer-Aided Verification, CAV’99, pages 443–454. LNCS 1633.
F. Tip. A survey of program slicing techniques. Technical Report CS-R9438, Centrum voor Wiskunde en InformatIca, 1994.
J. Tretmans. Testing concurrent systems: A formal approach. Concurrency Theory, CONCUR’99, pages 46–65. LNCS 1664.
L. Van Aertryck, M. Benveniste, and D. Le Metayer. casting: a formally based software test generation method. In IEEE International Conference on Formal Engineering Methods (ICFEM’97), 1997.
M. Weiser. Program slicing. IEEE Transactions on Software Engineering, 10(4):352–357, 1984.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rusu, V. (2002). Verification Using Test Generation Techniques. In: Eriksson, LH., Lindsay, P.A. (eds) FME 2002:Formal Methods—Getting IT Right. FME 2002. Lecture Notes in Computer Science, vol 2391. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45614-7_15
Download citation
DOI: https://doi.org/10.1007/3-540-45614-7_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43928-8
Online ISBN: 978-3-540-45614-8
eBook Packages: Springer Book Archive