More Web Proxy on the site http://driver.im/

Article

Generation of Functional Test Sequences from B Formal Specifications-Presentation and Industrial Case Study

Authors:

Fabien PeureuxAuthors Info & Claims

ASE '01: Proceedings of the 16th IEEE international conference on Automated software engineering

Page 377

Published: 26 November 2001 Publication History

Abstract

This paper presents an original method to generate testsequences. From formal specifications of the system to betested, an equivalent system of constraints is derived, andthen, the domain of each state variable of this system is partitionedinto subdomains. Using this partition, limit statesare computed with a specific solver that uses ConstraintLogic Programming with sets. This specific solver is thenused to build test sequences by traversing the constrainedreachability graph of the specifications. Finally, the formalspecifications is used as an oracle by using them to determinethe expected output for a given input. The results of anindustrial case-study of the Smart Card GSM 11-11 standardare presented and discussed.

References

[1]

G. Bernot, M-C. Gaudel, and B. Marre. Software testing based on formal specifications: a theory and a tool. Software Engineering Journal, 6(6):387-405, November 1991.

Digital Library

[2]

D.A. Carrington and P.A. Stocks. A tale of two paradigms: formal methods and software testing. In Proceedings of the Z user workshop (8th Z User Meeting), pages 51-68, Cambridge, UK, June 1994.

[3]

J-R Abrial. The B-BOOK: Assigning Programs to Meaning. Cambridge University Press, 1996.

Digital Library

[4]

J. Jaffar and J-L. Lassez. Constraint Logic Programming. In Proceedings POPL'87, pages 111-119, Munich, Germany, January 1987. ACM Press.

Digital Library

[5]

A. Gotlieb, B. Botella, and M. Rueher. A CLP framework for computing structural test data. In Springer-Verlag, editor, Proceedings of the First International Conference on Computational Logic (CL'2000), pages 399-413, London, UK, July 2000.

Digital Library

[6]

C. Meudec. ATGen: automatic test data generation using constraint logic programming and symbolic execution. The Journal of Software Testing, Verification and Reliability, 11:81-96, 2001.

[7]

H. Lotzbeyer and A. Pretschner. AutoFocus on constraint logic programming. In CL'2000 Workshop on (Constraint) Logic Programming and Software Engineering LPSE'2000, London, UK, July 2000.

[8]

B. Marre and A. Arnould. Test Sequence generation from Lustre descriptions: GATEL. In Proceedings of the 15th IEEE Int. Conf. on Automated Software Engineering (ASE'00), Grenoble, France, 2000.

Digital Library

[9]

E. Sekerinski and K. Sere. Program development by refinement - Case studies using the B method. Springer-Verlag, 1999. ISBN 1 85233 0538.

Digital Library

[10]

F. Ambert, B. Legeard, and E. Legros. Constraint Logic Programming on Sets and Multisets. In Proceedings of ICLP'94 - Workshop on Constraint Languages and their use in Problem Modeling, pages 151-165, Ithaca, New York, November 1994.

[11]

F. Bouquet, B. Legeard, and F. Peureux. Constraint Logic Programming with sets for animation of B formal specifications. In CL'2000 Workshop on (Constraint) Logic Programming and Software Engineering LPSE'2000, London, July 2000.

[12]

European Telecommunications Standards Institute, F- 06921 Sophia Antipolis cedex - France. GSM 11-11 V7.2.0 Technical Specifications, 1999.

[13]

A. Pretschner. Classical search strategies for test case generation with Constraint Logic Programming. In BRICS, editor, Proceedings of the Workshop on Formal Approaches to Testing of Software (FATES'01), pages 47-60, Aalborg, Denmark, August 2001.

[14]

J. Dick and A. Faivre. Automating the generation and sequencing of test cases from model-based specifications. FME'93: Industrial Strength Formal Methods Europe, LNCS 670:268-284, 1993.

Digital Library

[15]

P.A. Stocks and D.A. Carrington. A framework for specification-based testing. IEEE Transaction in Software Engineering, 22(11):777-793, November 1996.

Digital Library

[16]

E. Bernard, B. Legeard, X. Luck, and F. Peureux. Generation of functional test sequences from B formal specifications using Constraint logic programming with sets - industrial case-study. Technical Report TFC01-01, LIFC - University of Franche-Comté, 2001.

Cited By

Bernard ELegeard BLuck XPeureux F(2019)Generation of test sequences from formal specificationsSoftware—Practice & Experience10.1002/spe.59734:10(915-948)Online publication date: 4-Jan-2019
https://dl.acm.org/doi/10.1002/spe.597
Bouquet FLegeard BPeureux F(2018)CLPS---B --- A constraint solver to animate a B specificationInternational Journal on Software Tools for Technology Transfer (STTT)10.5555/2944225.29443706:2(143-157)Online publication date: 28-Dec-2018
https://dl.acm.org/doi/10.5555/2944225.2944370
Balck KGrinchtein OPearson JFettweis GNebel W(2014)Model-based protocol log generation for testing a telecommunication test harness using CLPProceedings of the conference on Design, Automation & Test in Europe10.5555/2616606.2616839(1-4)Online publication date: 24-Mar-2014
https://dl.acm.org/doi/10.5555/2616606.2616839
Show More Cited By

Recommendations

Generation of test sequences from formal specifications: GSM 11-11 standard case study

This paper presents the results of a case study on generating test cases for a fragment of the smart card GSM 11-11 standard. The generation method is based on an original approach using the B notation and techniques of constraint logic programming with ...
Selecting and mapping test sequences from formal specifications of concurrent programs
HASE '96: Proceedings of the 1996 High-Assurance Systems Engineering Workshop

Specification-based testing of concurrent programs requires that test sequences be selected from the specification and mapped to the implementation. Test sequences can be selected incrementally. During incremental testing, the specification is ...
Automated test case generation from IFAD VDM++ specifications
SEPADS'05: Proceedings of the 4th WSEAS International Conference on Software Engineering, Parallel & Distributed Systems

Most of the current research on automatic generation of test cases from formal specifications has been directed towards non object-oriented formal specifications. While object-oriented paradigm is the most widely accepted methodology for software ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ASE '01: Proceedings of the 16th IEEE international conference on Automated software engineering

November 2001

Copyright © Copyright (c) 2001 Institute of Electrical and Electronics Engineers, Inc. All rights reserved.

Publisher

IEEE Computer Society

United States

Publication History

Published: 26 November 2001

Author Tags

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 82 of 337 submissions, 24%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 17 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Bernard ELegeard BLuck XPeureux F(2019)Generation of test sequences from formal specificationsSoftware—Practice & Experience10.1002/spe.59734:10(915-948)Online publication date: 4-Jan-2019
https://dl.acm.org/doi/10.1002/spe.597
Bouquet FLegeard BPeureux F(2018)CLPS---B --- A constraint solver to animate a B specificationInternational Journal on Software Tools for Technology Transfer (STTT)10.5555/2944225.29443706:2(143-157)Online publication date: 28-Dec-2018
https://dl.acm.org/doi/10.5555/2944225.2944370
Balck KGrinchtein OPearson JFettweis GNebel W(2014)Model-based protocol log generation for testing a telecommunication test harness using CLPProceedings of the conference on Design, Automation & Test in Europe10.5555/2616606.2616839(1-4)Online publication date: 24-Mar-2014
https://dl.acm.org/doi/10.5555/2616606.2616839
Buchs DPedro LLúcio L(2006)Formal test generation from UML modelsDependable Systems10.5555/2167792.2167801(145-171)Online publication date: 1-Jan-2006
https://dl.acm.org/doi/10.5555/2167792.2167801
Sinha AParadkar ABultan T(2006)Model-based functional conformance testing of web services operating on persistent dataProceedings of the 2006 workshop on Testing, analysis, and verification of web services and applications10.1145/1145718.1145721(17-22)Online publication date: 17-Jul-2006
https://dl.acm.org/doi/10.1145/1145718.1145721
Bigot CFaivre AGaston CSimon J(2006)Automatic test generation on a (U)SIM smart cardProceedings of the 7th IFIP WG 8.8/11.2 international conference on Smart Card Research and Advanced Applications10.1007/11733447_25(345-358)Online publication date: 19-Apr-2006
https://dl.acm.org/doi/10.1007/11733447_25
Bouquet FLegeard BPeureux FTorreborre E(2004)Mastering test generation from smart card software formal modelsProceedings of the 2004 international conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices10.1007/978-3-540-30569-9_4(70-85)Online publication date: 10-Mar-2004
https://dl.acm.org/doi/10.1007/978-3-540-30569-9_4

View Options

View options

Media

Figures

Other

Tables

View Table of Contents