article

A framework and tool support for the systematic testing of model-based specifications

Authors:

Paul StrooperAuthors Info & Claims

ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 12, Issue 4

Pages 409 - 439

https://doi.org/10.1145/990010.990012

Published: 01 October 2003 Publication History

Abstract

Formal specifications can precisely and unambiguously define the required behavior of a software system or component. However, formal specifications are complex artifacts that need to be verified to ensure that they are consistent, complete, and validated against the requirements. Specification testing or animation tools exist to assist with this by allowing the specifier to interpret or execute the specification. However, currently little is known about how to do this effectively.This article presents a framework and tool support for the systematic testing of formal, model-based specifications. Several important generic properties that should be satisfied by model-based specifications are first identified. Following the idea of mutation analysis, we then use variants or mutants of the specification to check that these properties are satisfied. The framework also allows the specifier to test application-specific properties. All properties are tested for a range of states that are defined by the tester in the form of a testgraph, which is a directed graph that partially models the states and transitions of the specification being tested. Tool support is provided for the generation of the mutants, for automatically traversing the testgraph and executing the test cases, and for reporting any errors. The framework is demonstrated on a small specification and its application to three larger specifications is discussed. Experience indicates that the framework can be used effectively to test small to medium-sized specifications and that it can reveal a significant number of problems in these specifications.

References

[1]

Ammann, P. and Black, P. 1999. A specification-based coverage metric to evaluate test suites. Int. J. Reliab., Qual. Saf. Engg. 8, 4, pp. 275--300.]]

[2]

Ammann, P., Black, P., and Majurski, W. 1998. Using model checking to generate tests from specifications. In Proceedings of the 2nd IEEE International Conference on Formal Engineering Methods. IEEE Computer Society, pp. 46--54.]]

Digital Library

[3]

Callahan, J. S. E., and Montgomery, T. 1998. Generating test oracles via model checking. Technical Report NASA-IVV-98-015, NASA/West Virginia University Software Research Laboratory.]]

[4]

Carrington, D., MacColl, I., McDonald, J., Murray, L., and Strooper, P. 2000. From Object-Z specifications to Classbench test suites. J. Softw. Test., Verif. Reliab. 10, 2, pp. 111--137.]]

[5]

Carrington, D. and Stocks, P. 1994. A tale of two paradigms: Formal methods and software testing. In ZUM'94, Z User Workshop, J.P.Bowen and J. Hall, Eds. Springer-Verlag, pp. 51--68.]]

[6]

Chang, K. H., Liao, S. S., Seidman, S. B., and Chapman, E. 1998. Testing object-oriented programs: from formal specification to test scenario generation. J. Syst. Softw. 42, 2, pp. 141--151.]]

Digital Library

[7]

Clarke, E., Grumberg, O., and Peled, D. A. 1999. Model Checking. MIT Press, Cambridge, Mass.]]

Digital Library

[8]

DeMillo, R., Lipton, R., and Sayward, F. 1978. Hints on test data selection: Help for the practicing programmer. IEEE Comput. 11, 4, pp. 34--41.]]

Digital Library

[9]

Dick, J. and Faivre, A. 1993. Automating the generation and sequencing of test cases from model-based specifications. In Formal Methods Europe (FME'93): Industrial-Strength Formal Methods. Springer-Verlag, pp. 268--284.]]

Digital Library

[10]

Duke, R. and Rose, G. 2000. Formal Object-Oriented Specification Using Object-Z. MacMillan Press Limited, London.]]

[11]

Hamilton, N., Hazel, D., Kearney, P., Traynor, O., and Wildman, L. 1998. A complete formal development using Cogito. In Computer Science '98: Proceedings of the 21st Australasian Computer Science Conference. Springer-Verlag, pp. 319--330.]]

[12]

Hazel, D., Strooper, P., and Traynor, O. 1997. Possum: An animator for the SUM specification language. In Proceedings of Asia-Pacific Software Engineering Conference and International Computer Science Conference. IEEE Computer Society, pp. 42--51.]]

Digital Library

[13]

Hazel, D., Strooper, P., and Traynor, O. 1998. Requirements engineering and verification using specification animation. In the 13th IEEE International Conference on Automated Software Engineering. IEEE Computer Society, pp. 302--305.]]

Digital Library

[14]

Heitmeyer, C., Kirby, J., Labaw, B., and Bharadwaj, R. 1998. SCR*: A toolset for specifying and analysing software requirements. In Proceedings of Computer-Aided Verification 10th Annual Conference (CAV'98). Springer-Verlag, pp. 526--531.]]

Digital Library

[15]

Hewitt, M., O'Halloran, C., and Sennett, C. 1997. Experiences with PiZA, an animator for Z. In ZUM'97: The Z Formal Specification Notation. Springer-Verlag, pp. 37--51.]]

Digital Library

[16]

Hierons, R. M. 1997. Testing from a Z specification. Softw. Test., Verif. Reliab. 7, 1, pp. 19--33.]]

[17]

Hoffman, D. M. and Strooper, P. A. 1995. The testgraphs methodology---automated testing of collection classes. J. Obj.-Orient. Program., pp. 35--41.]]

[18]

Hoffman, D. M. and Strooper, P. A. 1998. ClassBench: A methodology and framework for automated class testing. In Testing Object-Oriented Software, D. C. Kung, P. Hsia, and J. Gao, Eds. IEEE Computer Society, pp. 152--176.]]

[19]

IFAD. Features of VDM tools. http://www.ifad.dk/products/vdmtools/features.htm.]]

[20]

Kazmierczak, E., Dart, P., Stirling, L., and Winikoff, M. 2000. Verifying requirements through mathematical modelling and animation. Int. J. Softw. Engg. Knowl. Engg. 10, 2, pp. 251--273.]]

[21]

Kazmierczak, E., Kearney, P., Traynor, O., and Wang, L. 1995. A modular extension to Z for specification, reasoning and refinement. Technical report 95-15, Software Verification Research Centre. February.]]

[22]

Legeard, B., Peureux, F., and Utting, M. 2002. Automated boundary testing from Z and B. In Proceedings of Formal Methods Europe 2002. Springer, pp. 21--40.]]

Digital Library

[23]

Liu, S. 1999. Verifying consistency and validity of formal specifications by testing. In Proceedings of the World Congress on Formal Methods in the Development of Computing Systems. Springer-Verlag, pp. 896--914.]]

Digital Library

[24]

Miller, T. and Strooper, P. 2001. Animation can show only the presence of errors, never their absence. In the Australian Software Engineering Conference (ASWEC 2001) (Canberra, Australia). IEEE Computer Society Press, pp. 76--85.]]

Digital Library

[25]

Miller, T. and Strooper, P. 2002a. A framework and tool support for the systematic testing of model-based specifications. Technical Report 02-35, SVRC, The University of Queensland, Australia.]]

[26]

Miller, T. and Strooper, P. 2002b. Model-based animation using testgraphs. In the International Conference on Formal Engineering Methods. Springer Verlag, pp. 192--203.]]

Digital Library

[27]

Miller, T. and Strooper, P. 2003. Supporting the software testing process through specification animation. In the 1st International Conference on Software Engineering and Formal Methods. IEEE Computer Society, pp. 14--23.]]

[28]

Murray, L., Carrington, D., MacColl, I., McDonald, J., and Strooper, P. 1998. Formal derivation of finite state machines for class testing. In ZUM'98: The Z Formal Specification Notation, J. B. Hinchey, A. Fett, and M.G., Eds. Vol. 1493. Springer-Verlag, pp. 42--59.]]

Digital Library

[29]

Robinson, N., Barney, D., Kearney, P., Nikandros, G., and Tombs, D. 2001. Automatic generation and verification of design specifications for railway signalling applications. In Proceedings of INCOSE 11th Annual International Symposium.]]

[30]

Schneider, S. 2001. The B-Method: An Introduction. Palgrave.]]

[31]

Stocks, P. and Carrington, D. 1996. A framework for specification-based testing. IEEE Trans. Softw. Engg. 22, 11, pp. 777--793.]]

Digital Library

[32]

Treharne, H., Ormsby, B., Draper, J., and Boyce, T. 1996. Evaluating the B-Method on an avionics example. In Proceedings of DASIA Conference. pp. 89--97.]]

[33]

Turner, C. and Robson, D. 1995. A state-based approach to the testing of class-based programs. Softw.--Conc. Tools 16, 3, pp. 106--112.]]

[34]

Utting, M. 2000. Data structures for Z testing tools, FM-TOOLS Workshop.]]

[35]

Waeselynck, H. and Behnia, S. 1998. B-Model animation for external verification. In Proceedings of the International Conference for Formal Engineering Methods. IEEE Computer Society, pp. 36--45.]]

Digital Library

Cited By

Ji RXu M(2023)Finding Specification Blind Spots via Fuzz Testing2023 IEEE Symposium on Security and Privacy (SP)10.1109/SP46215.2023.10179438(2708-2725)Online publication date: May-2023
https://doi.org/10.1109/SP46215.2023.10179438
Liu SMiao W(2021)A formal specification animation method for operation validationJournal of Systems and Software10.1016/j.jss.2021.110948178(110948)Online publication date: Aug-2021
https://doi.org/10.1016/j.jss.2021.110948
khan Miftikhar SIqbal MSherin S(2018)Empirical studies omit reporting necessary detailsComputer Standards & Interfaces10.1016/j.csi.2017.08.00255:C(156-170)Online publication date: 1-Jan-2018
https://dl.acm.org/doi/10.1016/j.csi.2017.08.002
Show More Cited By

Index Terms

A framework and tool support for the systematic testing of model-based specifications
1. Software and its engineering
  1. Software creation and management
    1. Designing software
      1. Requirements analysis
    2. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

Testing Formal Specifications to Detect Design Errors

Formal specification and verification techniques are now apused to increase the reliability of software systems. However, these proaches sometimes result in specifying systems that cannot be realized or that are not usable. This paper demonstrates why ...
Formal mutation testing for Circus

Context: The demand from industry for more dependable and scalable test-development mechanisms has fostered the use of formal models to guide the generation of tests. Despite many advancements having been obtained with state-based models, such as Finite ...
Using Modechart Modules for Testing Formal Specifications
HASE '99: The 4th IEEE International Symposium on High-Assurance Systems Engineering

Automated model-checking of formal specifications for real-time systems has remained an elusive goal due to the {\em state-space} explosion problem. This paper describes an approach to testing formal specifications using automatically generated testing ...

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Software Engineering and Methodology

ACM Transactions on Software Engineering and Methodology Volume 12, Issue 4

October 2003

103 pages

ISSN:1049-331X

EISSN:1557-7392

DOI:10.1145/990010

Issue’s Table of Contents

Copyright © 2003 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 October 2003

Published in TOSEM Volume 12, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

18
Total Citations
View Citations
1,952
Total Downloads

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

Reflects downloads up to 05 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Ji RXu M(2023)Finding Specification Blind Spots via Fuzz Testing2023 IEEE Symposium on Security and Privacy (SP)10.1109/SP46215.2023.10179438(2708-2725)Online publication date: May-2023
https://doi.org/10.1109/SP46215.2023.10179438
Liu SMiao W(2021)A formal specification animation method for operation validationJournal of Systems and Software10.1016/j.jss.2021.110948178(110948)Online publication date: Aug-2021
https://doi.org/10.1016/j.jss.2021.110948
khan Miftikhar SIqbal MSherin S(2018)Empirical studies omit reporting necessary detailsComputer Standards & Interfaces10.1016/j.csi.2017.08.00255:C(156-170)Online publication date: 1-Jan-2018
https://dl.acm.org/doi/10.1016/j.csi.2017.08.002
Liu S(2016)Validating formal specifications using testing-based specification animationProceedings of the 4th FME Workshop on Formal Methods in Software Engineering10.1145/2897667.2897668(29-35)Online publication date: 14-May-2016
https://dl.acm.org/doi/10.1145/2897667.2897668
Li MLiu S(2016)Integrating Animation-Based Inspection Into Formal Design Specification Construction for Reliable Software SystemsIEEE Transactions on Reliability10.1109/TR.2015.245685365:1(88-106)Online publication date: Mar-2016
https://doi.org/10.1109/TR.2015.2456853
Xinju Zhang Shuzhen Yao (2015)The new method of liveness verification with Object-Oriented Timed Petri Nets2015 Seventh International Conference on Advanced Computational Intelligence (ICACI)10.1109/ICACI.2015.7184779(7-11)Online publication date: Mar-2015
https://doi.org/10.1109/ICACI.2015.7184779
Liu S(2015)Automatic Selection of System Functional Scenarios for Formal Specification Animation2015 Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC.2015.15(72-79)Online publication date: Dec-2015
https://doi.org/10.1109/APSEC.2015.15
Liu S(2014)Extending Operation Semantics to Enhance the Applicability of Formal RefinementSpecification, Algebra, and Software10.1007/978-3-642-54624-2_21(434-440)Online publication date: 2014
https://doi.org/10.1007/978-3-642-54624-2_21
Xinju Zhang Shuzhen Yao (2013)Bank switching performance verification with object-oriented timed Petri nets2013 IEEE 8th Conference on Industrial Electronics and Applications (ICIEA)10.1109/ICIEA.2013.6566636(1664-1669)Online publication date: Jun-2013
https://doi.org/10.1109/ICIEA.2013.6566636
Miller TStrooper P(2011)A case study in model‐based testing of specifications and implementationsSoftware Testing, Verification and Reliability10.1002/stvr.43122:1(33-63)Online publication date: 27-Dec-2011
https://doi.org/10.1002/stvr.431
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents