Using formal specifications to support testing

ABSTRACT

Formal methods and testing are two important approaches that assist in the development of high-quality software. While traditionally these approaches have been seen as rivals, in recent years a new consensus has developed in which they are seen as complementary. This article reviews the state of the art regarding ways in which the presence of a formal specification can be used to assist testing.

REFERENCES

• 1: J.-R. Abrial, The B-book: assigning programs to meanings, Cambridge University Press, New York, NY, 1996
• 2: Lionel van Aertryck , Marc Benveniste , Daniel Le Métayer, CASTING: A Formally Based Software Test Generation Method, Proceedings of the 1st International Conference on Formal Engineering Methods, p.101, November 12-14, 1997
• 3: Aho, A. V., Dahbura, A. T., Lee, D., and Uyar, M. U. 1988. An optimization technique for protocol conformance test generation based on UIO sequences and Rural Chinese Postman Tours. In Protocol Specification, Testing, and Verification VIII. Elsevier (North-Holland), Amsterdam, The Netherlands, 75--86.
• 4: Bernhard K. Aichernig, Automated Black-Box Testing with Abstract VDM Oracles, Proceedings of the 18th International Conference on Computer Computer Safety, Reliability and Security, p.250-259, September 01, 1999
• 5: Aichernig, B. K. 2000. Formal specification techniques as a catalyst in validation. In Proceedings of the 5th IEEE High Assurance Systems Engineering Symposium (HASE, Albuquerque, NM). 203--207.
• 6: Aichernig, B. K. 2001a. Systematic black-box testing of computer based systems through formal abstraction techniques. Ph.D. dissertation, Graz University of Technology, Graz, Austria.
• 7: Bernhard K. Aichernig, Test-Case Calculation through Abstraction, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, p.571-589, March 12-16, 2001
• 8: Ahmed Al-Amayreh , Abdullah Mohd Zin, Probe: a formal specification-based testing system, Proceedings of the 20th international conference on Information Systems, p.400-404, December 12-15, 1999, Charlotte, North Carolina, United States
• 9: Allen, S. P. and Woodward, M. R. 1996. Assessing the quality of specification-based testing. In Proceedings of the 3rd International Conference on Achieving Quality in Software. Chapman and Hall, London, U.K., 341--354.
• 10: Rajeev Alur , Costas Courcoubetis , Thomas A. Henzinger , Pei-Hsin Ho, Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems, Hybrid Systems, p.209-229, January 1993
• 11: Rajeev Alur , David L. Dill, Automata For Modeling Real-Time Systems, Proceedings of the 17th International Colloquium on Automata, Languages and Programming, p.322-335, July 16-20, 1990
• 12: Rajeev Alur , David L. Dill, A theory of timed automata, Theoretical Computer Science, v.126 n.2, p.183-235, April 25, 1994 [doi>10.1016/0304-3975(94)90010-8]
• 13: Rajeev Alur , Radu Grosu , Yerang Hur , Vijay Kumar , Insup Lee, Modular Specification of Hybrid Systems in CHARON, Proceedings of the Third International Workshop on Hybrid Systems: Computation and Control, p.6-19, March 23-25, 2000
• 14: Rajeev Alur , Robert P. Kurshan, Timing analysis in COSPAN, Proceedings of the DIMACS/SYCON workshop on Hybrid systems III : verification and control: verification and control, p.220-231, July 1996, New Brunswick, NeW Jersey, United States
• 15: Ambert, F., Bouquet, F., Chemin, S., Guenaud, S., Legeard, B., Peureux, F., Utting, M., and Vacelet, N. 2002. BZ-testing-tools: A tool-set for test generation from Z and B using constraint logic programming. In Formal Approaches to Testing Software (FATES 2002). INRIA, Brno, Czech Republic, 105--120.
• 16: Amla, N. and Ammann, P. 1992. Using Z specifications in category partition testing. In COMPASS '92, Proceedings of the 7th Annual Conference on Computer Assurance (Gaithersburg, MD). 15--18.
• 17: Paul E. Ammann , Paul E. Black , William Majurski, Using Model Checking to Generate Tests from Specifications, Proceedings of the Second IEEE International Conference on Formal Engineering Methods, p.46, December 09-11, 1998
• 18: Ammann, P. and Offutt, J. 1994. Using formal methods to derive test frames in category-partition testing. In Proceedings of the 9th Annual Conference on Computer Assurance (COMPASS, Gaithersburg, MD). 69--80.
• 19: Ammann, P. E. and Black, P. E. 2000. Test generation and recognition with formal methods. In Proceedings of the International Workshop on Automated Program Analysis, Testing and Verification (Limerick, Ireland). 64--67.
• 20: Hybrid Systems II, January 1995
• 21: Hybrid Systems IV, January 1997
• 22: Antsaklis, P. J., Kohn, W., Lemmon, M., Nerode, A., and Sastry, S. 1999. Hybrid Systems. Lecture Notes in Computer Science, vol. 1567. Springer-Verlag.
• 23: Cyrille Artho , Howard Barringer , Allen Goldberg , Klaus Havelund , Sarfraz Khurshid , Mike Lowry , Corina Pasareanu , Grigore Rosu , Koushik Sen , Willem Visser , Rich Washington, Combining test case generation and runtime verification, Theoretical Computer Science, v.336 n.2-3, p.209-234, 26 May 2005 [doi>10.1016/j.tcs.2004.11.007]
• 24: Atterer, R. 2000. Automatic test data generation from VDM-SL specifications. M.S. thesis. Queen's University of Belfast, Northern Ireland, U.K.
• 25: Balanescu, T., Cowling, T., Georgescu, H., Gheorghe, M., Holcombe, M., and Vertan, C. 1999. Communicating stream X-machines systems are no more than X-machines. J. Univers. Comput. Sci. 5, 494--507.
• 26: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 27: Barnett, M., Grieskamp, W., Nachmanson, L., Schulte, W., Tillmann, N., and Veanes, M. 2003. Towards a tool environment for model--based testing with ASML. In Formal Approaches to Testing. Lecture Notes in Computer Science, vol. 2931. Springer-Verlag, Berlin, Germany, 252--266.
• 28: Salimeh Behnia , Hélène Waeselynck, Test Criteria Definition for B Models, Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume I, p.509-529, September 20-24, 1999
• 29: Johan Bengtsson , Kim Larsen , Fredrik Larsson , Paul Pettersson , Wang Yi, UPPAAL—a tool suite for automatic verification of real-time systems, Proceedings of the DIMACS/SYCON workshop on Hybrid systems III : verification and control: verification and control, p.232-243, July 1996, New Brunswick, NeW Jersey, United States
• 30: Mike Benjamin , Daniel Geist , Alan Hartman , Gerard Mas , Ralph Smeets , Yaron Wolfsthal, A study in coverage-driven test generation, Proceedings of the 36th ACM/IEEE conference on Design automation, p.970-975, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.310108]
• 31: Gilles Bernot , Marie Claude Gaudel , Bruno Marre, Software testing based on formal specifications: a theory and a tool, Software Engineering Journal, v.6 n.6, p.387-405, Nov. 1991
• 32: Dirk Beyer , Adam J. Chlipala , Rupak Majumdar, Generating Tests from Counterexamples, Proceedings of the 26th International Conference on Software Engineering, p.326-335, May 23-28, 2004
• 33: Juan Bicarregui , Jeremy Dick , Brain Matthews , Eoin Woods, Making the most of formal specification through animation, testing and proof, Science of Computer Programming, v.29 n.1-2, p.53-78, July 1997 [doi>10.1016/S0167-6423(96)00029-9]
• 34: M. Bidoit , Peter Mosses, Casl User Manual: Introduction to Using the Common Algebraic Specification Language Casl (Lecture Notes in Computer Science, 2900), SpringerVerlag, 2004
• 35: Bogdanov, K. 2000. Automated testing of Harel's Statecharts. Ph.D. dissertation, The University of Sheffield, Sheffield, U.K.
• 36: L Bougé , N Choquet , L Fribourg , M C Gaudel, Test sets generation from algebraic specifications using logic programming, Journal of Systems and Software, v.6 n.4, p.343-360, Nov. 1986 [doi>10.1016/0164-1212(86)90004-X]
• 37: Jonathan P. Bowen , Kirill Bogdanov , John A. Clark , Mark Harman , Robert M. Hierons , Paul Krause, FORTEST: Formal Methods and Testing, Proceedings of the 26th International Computer Software and Applications Conference on Prolonging Software Life: Development and Redevelopment, p.91-104, August 26-19, 2002
• 38: Bradfield, J. and Stirling, C. 2001. Modal logics and mu-calculi: An introduction. In Handbook of Process Algebra. Elsevier Science, Amsterdam, The Netherlands, 293--330.
• 39: Brinksma, E. 1988. A theory for the derivation of tests. In Protocol Specification, Testing, and Verification VIII. North-Holland, Amsterdam, The Netherlands, 63--74.
• 40: Brinksma, E., Heerink, L., and Tretmans, J. 1997. Developments in testing transition systems. In IFIP TC6 10th International Workshop on Testing of Communicating Systems. Kluwer, Dordrecht, The Netherlands, 143--166.
• 41: Ed Brinksma , Lex Heerink , Jan Tretmans, Factorized Test Generation for Multi-Input/Output Transition Systems, Proceedings of the IFIP TC6 11th International Workshop on Testing Communicating Systems, p.67-82, August 31-September 02, 1998
• 42: Bart M. Broekman, Testing Enbredded Software, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2002
• 43: Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, August 1986 [doi>10.1109/TC.1986.1676819]
• 44: Burton, S. 2002. Automated testing from specifications. Ph.D. dissertation. The University of York, York, U.K.
• 45: Callahan, J., Schneider, F., and Easterbrook, S. 1996. Automated software testing using model-checking. In SPIN '96. Rutgers University, Brunswick, NJ, 118--127.
• 46: Cardell-Oliver, R. 2000. Conformance tests for real-time systems with timed automata specifications. Form. Aspects Comput. 12, 5, 350--371.
• 47: Carrington, D. A. and Stocks, P. A. 1994. A tale of two paradigms: Formal methods and software testing. In Z User Workshop, Cambridge 1994, J. P. Bowen and J. A. Hall, Eds. Workshops in Computing. Springer-Verlag, Berlin, Germany, 51--68.
• 48: Ana R. Cavalli , Byoung-Moon Chin , Kilnam Chon, Testing methods for SDL systems, Computer Networks and ISDN Systems, v.28 n.12, p.1669-1683, June 1996 [doi>10.1016/0169-7552(95)00125-5]
• 49: Ana R. Cavalli , David Lee , Christian Rinderknecht , Fatiha Zaïdi, Hit-or-Jump: An algorithm for embedded testing with applications to IN services, Proceedings of the IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XII) and Protocol Specification, Testing and Verification (PSTV XIX), p.41-56, October 05-08, 1999
• 50: Wendy Y. L. Chan , Son T. Vuong , Mabo Robert Ito, On Test Sequence Generation for Protocols, Proceedings of the IFIP WG6.1 Ninth International Symposium on Protocol Specification, Testing and Verification IX, p.119-130, June 06-09, 1989
• 51: Chang, J. and Richardson, D. 1994. Static and dynamic specification slicing. In Proceedings of the 4th Irvine Software Symposium (Irvine, CA).
• 52: Huo Yan Chen , T. H. Tse , F. T. Chan , T. Y. Chen, In black and white: an integrated approach to class-level testing of object-oriented programs, ACM Transactions on Software Engineering and Methodology (TOSEM), v.7 n.3, p.250-295, July 1998 [doi>10.1145/287000.287004]
• 53: Huo Yan Chen , T. H. Tse , T. Y. Chen, TACCLE: a methodology for object-oriented software testing at the class and cluster levels, ACM Transactions on Software Engineering and Methodology (TOSEM), v.10 n.1, p.56-109, Jan. 2001 [doi>10.1145/366378.366380]
• 54: Chen, H. Y., Tse, T. H., and Deng, Y. T. 2000. ROCS: An object-oriented class-level testing system based on the relevant observable contexts technique. Inform. Softw. Technol. 42, 10, 677--686.
• 55: Choquet, N. 1986. Test data generation using a prolog with constraints. In Proceedings of the Workshop on Software Testing. IEEE Computer Society Press, Los Alamitos, CA, 132--141.
• 56: T. S. Chow, Testing Software Design Modeled by Finite-State Machines, IEEE Transactions on Software Engineering, v.4 n.3, p.178-187, May 1978 [doi>10.1109/TSE.1978.231496]
• 57: Ciancarini, P., Cimato, S., and Mascolo, C. 1996. Engineering formal requirements: Analysis and testing. In Proceedings of the 8th International Conference on Software Engineering and Knowledge Engineering (SEKE, Lake Tahoe, CA). 385--392.
• 58: Alessandro Cimatti , Edmund M. Clarke , Fausto Giunchiglia , Marco Roveri, NUSMV: A New Symbolic Model Verifier, Proceedings of the 11th International Conference on Computer Aided Verification, p.495-499, July 06-10, 1999
• 59: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 60: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 61: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 62: Edmund M. Clarke , Jeannette M. Wing, Formal methods: state of the art and future directions, ACM Computing Surveys (CSUR), v.28 n.4, p.626-643, Dec. 1996 [doi>10.1145/242223.242257]
• 63: L. A. Clarke , J. Hassell , D. J. Richardson, A Close Look at Domain Testing, IEEE Transactions on Software Engineering, v.8 n.4, p.380-390, July 1982 [doi>10.1109/TSE.1982.235572]
• 64: Cleaveland, R., Li, T., and Sims, S. 2000. The Concurrency Workbench of the New Century. SUNY, Stony Brook, NY.
• 65: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 66: Craggs, I., Sardis, M., and Heuillard, T. 2003. AGEDIS case studies: Model-based testing in industry. In Proceedings of the 1st European Conference on Model-Driven Software Engineering. 106--117.
• 67: Elspeth Cusack , Clazien D. Wezeman, Deriving Tests for Objects Specified in Z, Proceedings of the Z User Workshop, p.180-195, December 14-15, 1992
• 68: P. Dauchy , M.-C. Gaudel , B. Marre, Using algebraic specifications in software testing: a case study on the software of an automatic subway, Journal of Systems and Software, v.21 n.3, p.229-244, June 1993 [doi>10.1016/0164-1212(93)90025-S]
• 69: C. Daws , A. Olivero , S. Tripakis , S. Yovine, The tool KRONOS, Proceedings of the DIMACS/SYCON workshop on Hybrid systems III : verification and control: verification and control, p.208-219, July 1996, New Brunswick, NeW Jersey, United States
• 70: de Vries, R. G. and Tretmans, J. 2000. On-the-fly conformance testing using Spin. Softw. Tools Technol. Transf. 2, 4 (Mar.), 382--393.
• 71: Richard A. De Millo , Richard J. Lipton , Alan J. Perlis, Social processes and proofs of theorems and programs, Communications of the ACM, v.22 n.5, p.271-280, May 1979 [doi>10.1145/359104.359106]
• 72: Derrick, J. and Boiten, E. 1999. Testing refinements of state-based formal specifications. Softw. Test. Verif. Reliab. 9, 27--50.
• 73: Jeremy Dick , Alain Faivre, Automating the Generation and Sequencing of Test Cases from Model-Based Specifications, Proceedings of the First International Symposium of Formal Methods Europe on Industrial-Strength Formal Methods, p.268-284, April 19-23, 1993
• 74: Edsger W. Dijkstra, Chapter I: Notes on structured programming, Structured programming, Academic Press Ltd., London, UK, 1972
• 75: Roong-Ko Doong , Phyllis G. Frankl, Case studies on testing object-oriented programs, Proceedings of the symposium on Testing, analysis, and verification, p.165-177, October 08-10, 1991, Victoria, British Columbia, Canada [doi>10.1145/120807.120822]
• 76: Roong-Ko Doong , Phyllis G. Frankl, The ASTOOT approach to testing object-oriented programs, ACM Transactions on Software Engineering and Methodology (TOSEM), v.3 n.2, p.101-130, April 1994 [doi>10.1145/192218.192221]
• 77: Ali Y. Duale , M. Ümit Uyar, A Method Enabling Feasible Conformance Test Sequence Generation for EFSM Models, IEEE Transactions on Computers, v.53 n.5, p.614-627, May 2004 [doi>10.1109/TC.2004.1275300]
• 78: Samuel Eilenberg, Automata, Languages, and Machines, Academic Press, Inc., Orlando, FL, 1974
• 79: Eisner, C. 2005. Formal verification of software source code through semi-automatic modeling. Softw. Syst. Model. 4, 1, 14--31.
• 80: El-Far, I. K., Thompson, H. H., and Mottay, F. E. 2001. Experiences in testing pocket PS applications. In Proceedings of the International Internet & Software Quality Week Europe Conference.
• 81: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 82: Abdeslam En-Nouaary , Rachida Dssouli , Ferhat Khendek, Timed Wp-Method: Testing Real-Time Systems, IEEE Transactions on Software Engineering, v.28 n.11, p.1023-1038, November 2002 [doi>10.1109/TSE.2002.1049402]
• 83: A. En-Nouaary , R. Dssouli , F. Khendek , A. Elqortobi, Timed Test Cases Generation Based on State Characterization Technique, Proceedings of the IEEE Real-Time Systems Symposium, p.220, December 02-04, 1998
• 84: André Engels , Loe M. G. Feijs , Sjouke Mauw, Test Generation for Intelligent Networks Using Model Checking, Proceedings of the Third International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.384-398, April 02-04, 1997
• 85: Summary of Dynamically discovering likely program invariants, Proceedings of the IEEE International Conference on Software Maintenance (ICSM'01), p.540, November 07-09, 2001
• 86: Farchi, E., Hartman, A., and Pinter, S. 2002. Using a model-based test generator to test for standard conformance. IBM Syst. J. 41, 1, 89--110.
• 87: Norman Fenton , Paul Krause , Martin Neil, Software Measurement: Uncertainty and Causal Modeling, IEEE Software, v.19 n.4, p.116-122, July 2002 [doi>10.1109/MS.2002.1020298]
• 88: Jean-Claude Fernandez , Claude Jard , Thierry Jéron , César Viho, Using On-The-Fly Verification Techniques for the Generation of test Suites, Proceedings of the 8th International Conference on Computer Aided Verification, p.348-359, August 03, 1996
• 89: James H. Fetzer, Program verification: the very idea, Communications of the ACM, v.31 n.9, p.1048-1063, Sept. 1988 [doi>10.1145/48529.48530]
• 90: Rohan Fletcher , A. S. M. Sajeev, A Framework for Testing Object-Oriented Software Using Formal Specifications, Proceedings of the 1996 Ada-Europe International Conference on Reliable Software Technologies, p.159-170, June 10-14, 1996
• 91: Formal Systems (Europe) Ltd. 1997. Failures-Divergence Refinement: FDR2 User Manual. Formal Systems (Europe) Ltd. Oxford, U.K.
• 92: Frantzen, L., Tretmans, J., and Willemse, T. A. C. 2004. Test generation based on symbolic specifications. In Proceedings of the Formal Approaches to Software Testing, 4th International Workshop (FATES) Linz, Austria), 1--15.
• 93: Susumu Fujiwara , Gregor von Bochmann , Ferhat Khendek , Mokhtar Amalou , Abderrazak Ghedamsi, Test Selection Based on Finite State Models, IEEE Transactions on Software Engineering, v.17 n.6, p.591-603, June 1991 [doi>10.1109/32.87284]
• 94: John Gannon , Paul McMullin , Richard Hamlet, Data Abstraction, Implementation, Specification, and Testing, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.3, p.211-223, July 1981 [doi>10.1145/357139.357140]
• 95: Hubert Garavel , Holger Hermanns, On Combining Functional Verification and Performance Evaluation Using CADP, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods - Getting IT Right, p.410-429, July 22-24, 2002
• 96: Angelo Gargantini , Constance Heitmeyer, Using model checking to generate tests from requirements specifications, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.146-162, September 06-10, 1999, Toulouse, France
• 97: Marie-Claude Gaudel, Testing Can Be Formal, Too, Proceedings of the 6th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.82-96, May 22-26, 1995
• 98: Marie-Claude Gaudel, Testing from Formal Specifications, a Generic Approach, Proceedings of the 6th Ade-Europe International Conference Leuven on Reliable Software Technologies, p.35-48, May 14-18, 2001
• 99: Gaudel, M.-C. and James, P. R. 1998. Testing algebraic data types and processes: a unifying theory. Form. Aspect. Comput. 10, 5--6, 436--451.
• 100: Christopher Paul Garrard , Derek Coleman , Robin M. Gallimore, Formal Specification and Design Time Testing, IEEE Transactions on Software Engineering, v.16 n.1, p.1-12, January 1990 [doi>10.1109/32.44359]
• 101: Gill, A. 1962. Introduction to the Theory of Finite-State Machines. McGraw-Hill, New York, NY.
• 102: Girard, A. R., Spry, S., and Hedrick, J. K. 2005. Real-time embedded hybrid control software for intelligent cruise control applications. IEEE Robot. Automat. Mag. 12, 1, 22--28.
• 103: Patrice Godefroid , J. van Leeuwen , J. Hartmanis , G. Goos , Pierre Wolper, Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 104: Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France [doi>10.1145/263699.263717]
• 105: John-Morten Godhavn , Trygve Lauvdal , Olav Egeland, Hybrid control in sea traffic management systems, Proceedings of the DIMACS/SYCON workshop on Hybrid systems III : verification and control: verification and control, p.149-160, July 1996, New Brunswick, NeW Jersey, United States
• 106: Goguen, J. A. and Malcolm, G. 2000. Software Engineering with OBJ: Algebraic Specifications in Action. Kluwer Academic Publishers, Dordrecht, The Netherlands.
• 107: Goguen, J. A. and Tardo, J. J. 1979. An introduction to OBJ: A language for writing and testing formal algebraic specifications. In Proceedings of the IEEE Conference on Specifications of Reliable Software. IEEE Computer Society Press, Los Alamitos, CA, 170--189.
• 108: G. Gonenc, A Method for the Design of Fault Detection Experiments, IEEE Transactions on Computers, v.19 n.6, p.551-558, June 1970 [doi>10.1109/T-C.1970.222975]
• 109: Goodenough, J. B. and Gerhart, S. L. 1975. Toward a theory of test data selection. IEEE Trans. Softw. Eng. 1, 2, 156--173.
• 110: Arnaud Gotlieb , Bernard Botella , Michel Rueher, Automatic test data generation using constraint solving techniques, Proceedings of the 1998 ACM SIGSOFT international symposium on Software testing and analysis, p.53-62, March 02-04, 1998, Clearwater Beach, Florida, United States
• 111: Wolfgang Grieskamp , Yuri Gurevich , Wolfram Schulte , Margus Veanes, Generating finite state machines from abstract state machines, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 112: Alex Groce , Doron Peled , Mihalis Yannakakis, Adaptive Model Checking, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.357-370, April 08-12, 2002
• 113: Elsa Gunter , Doron Peled, Model checking, testing and verification working together, Formal Aspects of Computing, v.17 n.2, p.201-221, August 2005 [doi>10.1007/s00165-005-0059-8]
• 114: V. Gupta , R. Jagadeesan , V. A. Saraswat, Computing with continuous change, Science of Computer Programming, v.30 n.1-2, p.3-49, Jan. 1998 [doi>10.1016/S0167-6423(97)00006-3]
• 115: Hall, P. A. V. 1988. Towards testing with respect to formal specification. In Proceedings of the 2nd IEE/BCS Conference on Software Engineering. 159--163.
• 116: R. Hamlet, Theoretical comparison of testing methods, Proceedings of the ACM SIGSOFT '89 third symposium on Software testing, analysis, and verification, p.28-37, December 13-15, 1989, Key West, Florida, United States
• 117: Harder, M. 2002. Improving test suites via generated specifications. Tech. rep. 848. Department of EECS. Cambridge, MA.
• 118: David Harel , Eran Gery, Executable Object Modeling with Statecharts, Computer, v.30 n.7, p.31-42, July 1997 [doi>10.1109/2.596624]
• 119: Mark Harman , Lin Hu , Rob Hierons , Joachim Wegener , Harmen Sthamer , André Baresel , Marc Roper, Testability Transformation, IEEE Transactions on Software Engineering, v.30 n.1, p.3-16, January 2004 [doi>10.1109/TSE.2004.1265732]
• 120: Havelund, K. and Pressburger, T. 1998. Model checking Java programs using Java PathFinder. Softw. Tools Technol. Transf. 2, 4, 366--381.
• 121: Klaus Havelund , Grigore Roşu, An Overview of the Runtime Verification Tool Java PathExplorer, Formal Methods in System Design, v.24 n.2, p.189-215, March 2004 [doi>10.1023/B:FORM.0000017721.39909.4b]
• 122: I J Hayes, Specification directed module testing, IEEE Transactions on Software Engineering, v.12 n.1, p.124-133, Jan. 1986
• 123: Steffen Helke , Thomas Neustupny , Thomas Santen, Automating Test Case Generation from Z Specifications with Isabelle, Proceedings of the 10th International Conference of Z Users on The Z Formal Specification Notation, p.52-71, April 03-04, 1997
• 124: F. C. Hennine, Fault detecting experiments for sequential circuits, Proceedings of the 1964 Proceedings of the Fifth Annual Symposium on Switching Circuit Theory and Logical Design, p.95-110, November 11-13, 1964 [doi>10.1109/SWCT.1964.8]
• 125: Henzinger, T., Jhala, R., Majumdar, R., and Sutre, G. 2003. Software verification with Blast. In SPIN 2003. Lecture Notes in Computer Science, vol. 2648. Springer-Verlag, Berlin, Germany, 235--239.
• 126: Thomas A. Henzinger , Orna Kupferman , Moshe Y. Vardi, A Space-Efficient On-the-fly Algorithm for Real-Time Model Checking, Proceedings of the 7th International Conference on Concurrency Theory, p.514-529, August 26-29, 1996
• 127: Hierons, R. M. 1997a. Testing from a finite state machine: Extending invertibility to sequences. Comput. J. 40, 4, 220--230.
• 128: Hierons, R. M. 1997b. Testing from a Z specification. Softw. Test. Verif. Reliab. 7, 1, 19--33.
• 129: Hierons, R. M. 2001. Checking states and transitions of a set of communicating finite state machines. Microproc. Microsyst. (Special Issue on Testing and Testing Techniques for Real-Time Embedded Software Systems) 24, 9, 443--452.
• 130: R. M. Hierons, Comparing test sets and criteria in the presence of test hypotheses and fault domains, ACM Transactions on Software Engineering and Methodology (TOSEM), v.11 n.4, p.427-448, October 2002 [doi>10.1145/606612.606615]
• 131: R. M. Hierons, Using a minimal number of resets when testing from a finite state machine, Information Processing Letters, v.90 n.6, p.287-292, 30 June 2004 [doi>10.1016/j.ipl.2004.03.003]
• 132: Rob M. Hierons, Testing from a Nondeterministic Finite State Machine Using Adaptive State Counting, IEEE Transactions on Computers, v.53 n.10, p.1330-1342, October 2004 [doi>10.1109/TC.2004.85]
• 133: Hierons, R. M. and Harman, M. 2000. Testing comformance to a quasi-non-determinstic stream X-machine. Form. Aspects Comput. 12, 6, 423--442.
• 134: R. M. Hierons , M. Harman, Testing conformance of a deterministic implementation against a non-deterministic stream X-machine, Theoretical Computer Science, v.323 n.1-3, p.191-233, 14 September 2004 [doi>10.1016/j.tcs.2004.04.002]
• 135: R. M. Hierons , T.-H. Kim , H. Ural, On the testability of SDL specifications, Computer Networks: The International Journal of Computer and Telecommunications Networking, v.44 n.5, p.681-700, 5 April 2004 [doi>10.1016/j.comnet.2003.06.001]
• 136: Hierons, R. M., Sadeghipour, S., and Singh, H. 2001. Testing a system specified using Statecharts and Z. Inform. Softw. Technol. 43, 2, 137--149.
• 137: Rob M. Hierons , Hasan Ural, Optimizing the Length of Checking Sequences, IEEE Transactions on Computers, v.55 n.5, p.618-629, May 2006 [doi>10.1109/TC.2006.80]
• 138: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 139: C. A. R. Hoare, How Did Software Get So Reliable Without Proof?, Proceedings of the Third International Symposium of Formal Methods Europe on Industrial Benefit and Advances in Formal Methods, p.1-17, March 18-22, 1996
• 140: Holcombe, M. and Ipate, F. 1998. Correct Systems: Building a Business Process Solution. Springer-Verlag, Berlin, Germany.
• 141: Gerard Holzmann, Spin model checker, the: primer and reference manual, Addison-Wesley Professional, 2003
• 142: Gerard Holzmann, On-the-fly model checking, ACM Computing Surveys (CSUR), v.28 n.4es, Dec. 1996 [doi>10.1145/242224.242379]
• 143: Holzmann, G. J. and Smith, M. H. 2001. Software model checking: Extracting verification models from source code. Softw. Test. Verif. Reliab. 11, 2, 65--79.
• 144: Hyoung Seok Hong , Sung Deok Cha , Insup Lee , Oleg Sokolsky , Hasan Ural, Data flow testing as model checking, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
• 145: Hyoung Seok Hong , Insup Lee , Oleg Sokolsky , Hasan Ural, A Temporal Logic Based Theory of Test Coverage and Generation, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.327-341, April 08-12, 2002
• 146: Hong, H. S., Lee, I., Sokolsky, O., and Cha, S. D. 2001. Automatic test generation from Statecharts using model checking. In FATES '01. BRICS Notes Series, vol. NS-01-4. BRICS, Aarhus, Denmark, 15--30.
• 147: Hörcher, H.-M. and Peleska, J. 1995. Using formal specifications to support software testing. Softw. Qual. J. 4, 4, 309--327.
• 148: Johann Hörl , Bernhard K. Aichernig, Validating Voice Communication Requirements Using Lightweight Formal Methods, IEEE Software, v.17 n.3, p.21-27, May 2000 [doi>10.1109/52.896246]
• 149: E. P. Hsieh, Checking Experiments ror Sequential Machines, IEEE Transactions on Computers, v.20 n.10, p.1152-1166, October 1971 [doi>10.1109/T-C.1971.223100]
• 150: Franz Huber , Bernhard Schätz , Geralf Einert, Consistent Graphical Specification of Distributed Systems, Proceedings of the 4th International Symposium of Formal Methods Europe on Industrial Applications and Strengthened Foundations of Formal Methods, p.122-141, September 15-19, 1997
• 151: Merlin Hughes , David Stotts, Daistish: systematic algebraic testing for OO programs in the presence of side-effects, Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis, p.53-61, January 08-10, 1996, San Diego, California, United States
• 152: Yerang Hur , Rafael Fierro , Insup Lee, Modeling Distributed Autonomous Robots Using CHARON: Formation Control Case Study, Proceedings of the Sixth IEEE International Symposium on Object-Oriented Real-Time Distributed Computing, p.93, May 14-16, 2003
• 153: Ipate, F. and Holcombe, M. 1997. An integration testing method that is proved to find all faults. Int. J. Comput. Math. 63, 3&4, 159--178.
• 154: Ipate, F. and Holcombe, M. 2000. Generating test sets from non-deterministic stream X-machines. Form. Aspects Comput. 12, 6, 443--458.
• 155: ISO. 1989a. ISO 8807:1989 Information Processing Systems, Open Systems Interconnection—LOTOS—A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. ISO, Geneva, Switzerland.
• 156: ISO. 1989b. ISO 9074; Estelle—A Formal Description Technique Based on an Extended State Transition Model. ISO, Geneva, Switzerland.
• 157: ITU-T. 1997. Recommendation Z.500 Framework on Formal Methods in Conformance Testing. International Telecommunications Union, Geneva, Switzerland.
• 158: ITU-T. 1999. Recommendation Z.100 Specification and Description Language (SDL). International Telecommunications Union, Geneva, Switzerland.
• 159: Daniel Jackson , Mandana Vaziri, Finding bugs with a constraint solver, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.14-25, August 21-24, 2000, Portland, Oregon, United States
• 160: Jalote, P. 1983. Specification and testing of abstract data types. In Proceedings of the 7th International Computer Software and Applications Conference (COMPSAC). IEEE Computer Society Press, Los Alamitos, CA, 508--511.
• 161: Jalote, P. and Caballero, M. G. 1988. Automated testcase generation for data abstraction. In Proceedings of the 12th International Computer Software and Applications Conference (COMPSAC). IEEE Computer Society Press, Los Alamitos, CA, 205--210.
• 162: Claude Jard , Thierry Jéron, TGV: theory, principles and algorithms: A tool for the automatic synthesis of conformance test cases for non-deterministic reactive systems, International Journal on Software Tools for Technology Transfer (STTT), v.7 n.4, p.297-315, August 2005 [doi>10.1007/s10009-004-0153-x]
• 163: Cliff B. Jones, Systematic software development using VDM (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 164: R. A. Kemmerer, Testing Formal Specifications to Detect Design Errors, IEEE Transactions on Software Engineering, v.11 n.1, p.32-43, January 1985 [doi>10.1109/TSE.1985.231535]
• 165: Kerbrat, A., Jéron, T., and Groz, R. 1999. Automated test generation from SDL specifications. In SDL For. 135--152.
• 166: Brian W. Kernighan , P. J. Plauger, Software Tools in Pascal, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1981
• 167: Steve King , Jonathan Hammond , Rod Chapman , Andy Pryor, Is Proof More Cost-Effective Than Testing?, IEEE Transactions on Software Engineering, v.26 n.8, p.675-686, August 2000 [doi>10.1109/32.879807]
• 168: Kohavi, Z. 1978. Switching and Finite State Automata Theory. McGraw-Hill, New York, NY.
• 169: Kondo, K. and Yoshida, M. 2005. Use of hybrid models for testing and debugging control software for electromechanical systems. IEEE/ASME Trans. Mechatron. 10, 3, 275--284.
• 170: Koné, O. 2001. A local approach to the testing of real-time systems. Comput. J. 44, 5, 435--447.
• 171: Krichen, M. and Tripakis, S. 2004. Black-box conformance testing for real-time systems. In Proceedings of the 11th International SPIN Workshop. 109--126.
• 172: Krichen, M. and Tripakis, S. 2005. An expressive and implementable formal framework for testing real-time systems. In Proceedings of the 17th IFIP TC6/WG 6.1 International Conference on Testing of Communicating Systems (TestCom). 209--225.
• 173: D. Richard Kuhn, Fault classes and error detection capability of specification-based testing, ACM Transactions on Software Engineering and Methodology (TOSEM), v.8 n.4, p.411-424, Oct. 1999 [doi>10.1145/322993.322996]
• 174: Man F. Lau , Yuen T. Yu, An extended fault class hierarchy for specification-based testing, ACM Transactions on Software Engineering and Methodology (TOSEM), v.14 n.3, p.247-276, July 2005 [doi>10.1145/1072997.1072998]
• 175: Guy Leduc, Conformance Relation, Associated Equivalence, and New Canonical Tester in LOTOS, Proceedings of the IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XI, p.249-264, June 18-20, 1991
• 176: D. Lee , M. Yannakakis, Testing Finite-State Machines: State Identification and Verification, IEEE Transactions on Computers, v.43 n.3, p.306-320, March 1994 [doi>10.1109/12.272431]
• 177: Lee, D. and Yannakakis, M. 1996. Principles and methods of testing finite-state machines. Proc. IEEE 84, 8, 1089--1123.
• 178: Bruno Legeard , Fabien Peureux , Mark Utting, Automated Boundary Testing from Z and B, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods - Getting IT Right, p.21-40, July 22-24, 2002
• 179: Bruno Legeard , Fabien Peureux , Mark Utting, A Comparison of the BTT and TTF Test-Generation Methods, Proceedings of the 2nd International Conference of B and Z Users on Formal Specification and Development in Z and B, p.309-329, January 23-25, 2002
• 180: Grégory Lestiennes , Marie-Claude Gaudel, Testing Processes from Formal Specifications with Inputs, Outputs and Data Types, Proceedings of the 13th International Symposium on Software Reliability Engineering, p.3, November 12-15, 2002
• 181: Orna Lichtenstein , Amir Pnueli, Checking that finite state concurrent programs satisfy their linear specification, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-107, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318622]
• 182: Bev Littlewood, Dependability assessment of software-based systems: state of the art, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062461]
• 183: Shaoying Liu, Verifying Consistency and Validity of Formal Specifications by Testing, Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume I, p.896-914, September 20-24, 1999
• 184: Shaoying Liu , T. Fukuzaki , K. Miyamoto, A GUI and testing tool for SOFL, Proceedings of the Seventh Asia-Pacific Software Engineering Conference, p.421, December 05-08, 2000
• 185: López, N. and Núñez, M. 2004. An overview of probabilistic process algebras and their equivalences. In Validation of Stochastic Systems. Lecture Notes in Computer Science, vol. 2925. Springer, Berlin, Germany, 89--123.
• 186: Gang Luo , Alexandre Petrenko , Gregor v. Bochmann, Selecting test sequences for partially-specified nondeterministic finite state machines, 7th IFIP WG 6.1 international workshop on Protocol test systems, p.95-110, November 1995, Tokyo, Japan
• 187: Gang Luo , G. von Bochmann , A. Petrenko, Test Selection Based on Communicating Nondeterministic Finite-State Machines Using a Generalized Wp-Method, IEEE Transactions on Software Engineering, v.20 n.2, p.149-162, February 1994 [doi>10.1109/32.265636]
• 188: Lynce, I. and Marques-Silva, J. 2002. Building state-of-the-art sat solvers. In Proceedings of the 15th European Conference on Artificial Intelligence (ECAI). 166--170.
• 189: MacColl, I. and Carrington, D. 1998. Testing MATIS: A case study on specification-based testing of interactive systems. In FAHCI98: Proceedings of the Formal Aspects of Human Computer Interaction Workshop. British Computer Society, Swindon, U.K., 57--69.
• 190: Patrícia D. L. Machado, Testing from Structured Algebraic Specifications, Proceedings of the 8th International Conference on Algebraic Methodology and Software Technology, p.529-544, May 20-27, 2000
• 191: Zohar Manna , Amir Pnueli, Verifying Hybrid Systems, Hybrid Systems, p.4-35, January 1993
• 192: Zohar Manna , Amir Pnueli, Temporal verification of reactive systems: safety, Springer-Verlag New York, Inc., New York, NY, 1995
• 193: Darko Marinov , Sarfraz Khurshid, TestEra: A Novel Framework for Automated Testing of Java Programs, Proceedings of the 16th IEEE international conference on Automated software engineering, p.22, November 26-29, 2001
• 194: Bruno Marre, LOFT: A Tool for Assisting Selection of Test Data Sets from Algebraic Specifications, Proceedings of the 6th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.799-800, May 22-26, 1995
• 195: Marriott, K. and Stuckey, P. 1998. Programming with Constraints: An Introduction. MIT Press, Cambridge, MA.
• 196: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 197: P. R. McMullin , J. D. Gannon, Combining Testing with Formal Specifications: A Case Study, IEEE Transactions on Software Engineering, v.9 n.3, p.328-335, May 1983 [doi>10.1109/TSE.1983.236869]
• 198: Meudec, C. 1997. Automatic generation of software tests from formal specifications. Ph.D. dissertation, Queen's University of Belfast, Northern Ireland, U.K.
• 199: Huaikou Miao , Xiaolei Gao , Ling Liu, An Approach to Testing the Nonexistence of Initial State in Z Specifications, Proceedings of the 8th Asian Test Symposium, p.289, November 16-18, 1999
• 200: Erich Mikk, Compilation of Z Specifications into C for Automatic Test Result Evaluation, Proceedings of the 9th International Conference of Z Usres on The Z Formal Specification Notation, p.167-180, September 07-09, 1995
• 201: MIL-STD 188-220B. 1998. Military Standard-Interoperability Standard for Digital Message Device Subsystems. Department of Defense, Washington, DC.
• 202: Raymond E. Miller , Sanjoy Paul, On the generation of minimal-length conformance tests for communication protocols, IEEE/ACM Transactions on Networking (TON), v.1 n.1, p.116-129, Feb. 1993 [doi>10.1109/90.222912]
• 203: R. Milner, Communication and Concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 204: Moore, E. P. 1956. Gedanken-experiments. In Automata Studies, C. Shannon and J. McCarthy, Eds. Princeton University Press, Princeton, NJ.
• 205: Peter D. Mosses, Casl Reference Manual: The Complete Documentation Of The Common Algebraic Specification Language (LECTURE NOTES IN COMPUTER SCIENCE), SpringerVerlag, 2004
• 206: MOST Cooperation. 2002. MOST media oriented system transport—multimedia and control networking technology. MOST Cooperation. Karlsruhe, Germany.
• 207: Leesa Murray , David A. Carrington , Ian MacColl , Jason McDonald , Paul A. Strooper, Formal Derivation of Finite State Machines for Class Testing, Proceedings of the 11th International Conference of Z Users on The Z Formal Specification Notation, p.42-59, September 24-26, 1998
• 208: Naito, S. and Tsunoyama, M. 1981. Fault detection for sequential machines. In Proceedings of the IEEE Fault Tolerant Computing Conference. 238--243.
• 209: Nielsen, B. and Skou, A. 2003. Automated test generation from timed automata. Softw. Tools Technol. Transf. 5, 1, 59--77.
• 210: Núñez, M. and Rodríguez, I. 2003. Towards testing stochastic timed systems. In Formal Techniques for Networked and Distributed Systems (FORTE 2003). Lecture Notes in Computer Science, vol. 2767. Springer, Berlin, Germany, 335--350.
• 211: A. Jefferson Offut , Shaoying Liu, Generating test data from SOFL specifications, Journal of Systems and Software, v.49 n.1, p.49-62, Dec. 15, 1999 [doi>10.1016/S0164-1212(99)00066-7]
• 212: T. J. Ostrand , M. J. Balcer, The category-partition method for specifying and generating fuctional tests, Communications of the ACM, v.31 n.6, p.676-686, June 1988 [doi>10.1145/62959.62964]
• 213: Park, D., Stern, U., Skakkebaek, J. U., and Dill, D. L. 2000. Java model checking. In Proceedings of the International Workshop on Automated Program Analysis, Testing and Verification (Limerick, Ireland). 74--82.
• 214: Doron Peled, Ten Years of Partial Order Reduction, Proceedings of the 10th International Conference on Computer Aided Verification, p.17-28, June 28-July 02, 1998
• 215: Peled, D. 2003. Model checking and testing combined. In Automata, Languages and Programming, 30th International Colloquium (ICALP 2003). Lecture Notes in Computer Science, vol. 2719. Springer-Verlag, Berlin, Germany, 47--63.
• 216: Doron Peled , Moshe Y. Vardi , Mihalis Yannakakis, Black box checking, Journal of Automata, Languages and Combinatorics, v.7 n.2, p.225-246, November 2001
• 217: Alexandre Petrenko, Checking Experiments with Protocol Machines, Proceedings of the IFIP TC6/WG6.1 Fourth International Workshop on Protocol Test Systems IV, p.83-94, October 15-17, 1991
• 218: Alexandre Petrenko, Fault model-driven test derivation from finite state models: annotated bibliography, Modeling and verification of parallel processes, Springer-Verlag New York, Inc., New York, NY, 2001
• 219: Alexandre Petrenko , Sergiy Boroday , Roland Groz, Confirming configurations in EFSM, Proceedings of the IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XII) and Protocol Specification, Testing and Verification (PSTV XIX), p.5-24, October 05-08, 1999
• 220: Alexandre Petrenko , Sergiy Boroday , Roland Groz, Confirming Configurations in EFSM Testing, IEEE Transactions on Software Engineering, v.30 n.1, p.29-42, January 2004 [doi>10.1109/TSE.2004.1265734]
• 221: Alexandre Petrenko , Nina Yevtushenko , Alexandre Lebedev , Anindya Das, Nondeterministic State Machines in Protocol Conformance Testing, Proceedings of the IFIP TC6/WG6.1 Sixth International Workshop on Protocol Test systems VI, p.363-378, September 28-30, 1993
• 222: A. Petrenko , N. Yevtushenko , G. v. Bochmann, Testing deterministic implementations from nondeterministic FSM specifications, Selected proceedings of the IFIP TC6 9th international workshop on Testing of communicating systems, p.125-140, September 1996, Darmstadt, Germany
• 223: Marc Phalippou, Executable Testers, Proceedings of the IFIP TC6/WG6.1 Sixth International Workshop on Protocol Test systems VI, p.35-50, September 28-30, 1993
• 224: Amir Pnueli, The temporal logic of programs, Proceedings of the 18th Annual Symposium on Foundations of Computer Science, p.46-57, September 30-October 31, 1977
• 225: A. Pretschner , W. Prenninger , S. Wagner , C. Kühnel , M. Baumgartner , B. Sostawa , R. Zölch , T. Stauner, One evaluation of model-based testing and its automation, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062529]
• 226: Jean-Pierre Queille , Joseph Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th Colloquium on International Symposium on Programming, p.337-351, April 06-08, 1982
• 227: Anders P. Ravn , Hans Rischel , Finn Conrad , Torben O. Andersen, Hybrid Control of a Robot - A Case Study, Hybrid Systems II, p.391-404, January 1995
• 228: Michael D. Rice , Stephen B. Seidman, An approach to architectural analysis and testing, Proceedings of the third international workshop on Software architecture, p.121-123, November 01-05, 1998, Orlando, Florida, United States [doi>10.1145/288408.288439]
• 229: Debra J. Richardson , Stephanie Leif Aha , T. Owen O'Malley, Specification-based test oracles for reactive systems, Proceedings of the 14th international conference on Software engineering, p.105-118, May 11-15, 1992, Melbourne, Australia [doi>10.1145/143062.143100]
• 230: D. J. Richardson , L. A. Clarke, Partition Analysis: A Method Combining Testing and Verification, IEEE Transactions on Software Engineering, v.11 n.12, p.1477-1490, December 1985 [doi>10.1109/TSE.1985.231892]
• 231: J. Robinson , Andrei Voronkov, Handbook of Automated Reasoning: Volume 1, MIT Press, Cambridge, MA, 2001
• 232: Krishan Sabnani , Anton Dahbura, A protocol test generation procedure, Computer Networks and ISDN Systems, v.15 n.4, p.285-297, Sept. 1988 [doi>10.1016/0169-7552(88)90064-5]
• 233: Fumiaki Sato , Kotaro Katsuyama , Tadanori Mizuno, TENT: Test Sequence Generation Tool for Communication Systems, Proceedings of the IFIP TC/WG6.1 Second International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, p.1-5, December 05-08, 1989
• 234: Michael Schmitt , Anders Ek , Beat Koch , Jens Grabowski , Dieter Hogrefe, Autolink - Putting SDL-Based Test Generation Into Practice, Proceedings of the IFIP TC6 11th International Workshop on Testing Communicating Systems, p.227-244, August 31-September 02, 1998
• 235: Deepinder P. Sidhu , Ting-kau Leung, Formal Methods for Protocol Testing: A Detailed Study, IEEE Transactions on Software Engineering, v.15 n.4, p.413-426, April 1989 [doi>10.1109/32.16602]
• 236: Sims, S. 1999. The Process Algebra Compiler User's Manual. Reactive Systems, Inc., Falls Church, VA.
• 237: Harbhajan Singh , Mirko Conrad , Sadegh Sadeghipour, Test Case Design Based on Z and the Classification-Tree Method, Proceedings of the 1st International Conference on Formal Engineering Methods, p.81, November 12-14, 1997
• 238: J. M. Spivey, Understanding Z: a specification language and its formal semantics, Cambridge University Press, New York, NY, 1988
• 239: J. M. Spivey, The Z notation: a reference manual, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1992
• 240: Thomas Stauner , Olaf Müller , Max Fuchs, Using HYTECH to Verify an Automative Control System, Proceedings of the International Workshop on Hybrid and Real-Time Systems, p.139-153, March 26-28, 1997
• 241: Susan Stepney, Testing as Abstraction, Proceedings of the 9th International Conference of Z Usres on The Z Formal Specification Notation, p.137-151, September 07-09, 1995
• 242: Colin Stirling, Modal and temporal logics, Handbook of logic in computer science (vol. 2): background: computational structures, Oxford University Press, Inc., New York, NY, 1993
• 243: Stocks, P. A. 1993. Applying formal methods to software testing. Ph.D. dissertation, University of Queensland, Brisbane, Australia.
• 244: Phil Stocks , David Carrington, A Framework for Specification-Based Testing, IEEE Transactions on Software Engineering, v.22 n.11, p.777-793, November 1996 [doi>10.1109/32.553698]
• 245: Tan, L., Kim, J., Sokolsky, O., and Lee, I. 2004. Model-based testing and monitoring for hybrid embedded systems. In Proceedings of the IEEE International Conference on Information Reuse and Integration (IRI). 487--492.
• 246: Taouil-Traverson, S. and Vignes, S. 1996. Preliminary analysis cycle for B-method software development. In EUROMICRO 96: Proceedings of the 22nd EUROMICRO Conference, Beyond 2000: Hardware and Software Design Strategies. 319--325.
• 247: N. Tracey , J. Clark , K. Mander , J. McDermid, Automated test-data generation for exception conditions, Software—Practice & Experience, v.30 n.1, p.61-79, Jan. 2000 [doi>10.1002/(SICI)1097-024X(200001)30:1<61::AID-SPE292>3.0.CO;2-9]
• 248: Helen Treharne , J. Draper , Steve Schneider, Test Case Preparation Using a Prototype, Proceedings of the Second International B Conference on Recent Advances in the Development and Use of the B Method, p.293-311, April 22-24, 1998
• 249: Jan Tretmans, Conformance testing with labelled transition systems: implementation relations and test generation, Computer Networks and ISDN Systems, v.29 n.1, p.49-79, Dec. 1996 [doi>10.1016/S0169-7552(96)00017-7]
• 250: Tretmans, J. and Brinksma, E. 2003. TorX: Automated Model Based Testing. In Proceedings of the First European Conference on Model-Driven Software Engineering, A. Hartman and K. Dussa-Zieger, Eds. Imbuss, Möhrendorf, Germany. 13 pages.
• 251: Tatsuhiro Tsuchiya , Tohru Kikuno, On fault classes and error detection capability of specification-based testing, ACM Transactions on Software Engineering and Methodology (TOSEM), v.11 n.1, p.58-62, January 2002 [doi>10.1145/504087.504089]
• 252: Ural, H., Saleh, K., and Williams, A. 2000. Test generation based on control and data dependencies within system specifications in SDL. Comput. Commun. 23, 609--627.
• 253: Hasan Ural , Xiaolin Wu , Fan Zhang, On Minimizing the Lengths of Checking Sequences, IEEE Transactions on Computers, v.46 n.1, p.93-99, January 1997 [doi>10.1109/12.559807]
• 254: Uyar, M. U. and Duale, A. Y. 1999. Resolving inconsistencies in EFSM modeled specifications. In Proceedings of the IEEE Military Communications Conference (MILCOM, Atlantic City, NJ).
• 255: Uyar, M. Ü., Fecko, M. A., Duale, A. Y., Amer, P. D., and Sethi, A. S. 2003. Experience in developing and testing network protocol software using FDTs. Inform. Softw. Technol. 45, 12, 815--835.
• 256: Antti Valmari, A Stubborn Attack On State Explosion, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.156-165, June 18-21, 1990
• 257: Varaiya, P. 1993. Smart cars on smart roads. IEEE Trans. Automat. Cont. 38, 2, 195--207.
• 258: Vardi, M. and Wolper, P. 1986. An automata-theoretic approach to automatic program verification. In Proceedings of the Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press, Los Alamitos, CA, 332--344.
• 259: Vasilevskii, M. P. 1973. Failure Diagnosis of Automata. Cybernetics. Plenum Publishing Corporation, New York, NY.
• 260: Sergiy A. Vilkomir , Jonathan P. Bowen, Formalization of Software Testing Criteria using the Z Notation, Proceedings of the 25th International Computer Software and Applications Conference on Invigorating Software Development, p.351-356, October 08-12, 2001
• 261: Sergiy A. Vilkomir , Jonathan P. Bowen, Reinforced Condition/Decision Coverage (RC/DC): A New Criterion for Software Testing, Proceedings of the 2nd International Conference of B and Z Users on Formal Specification and Development in Z and B, p.291-308, January 23-25, 2002
• 262: Gregor V. Bochmann , Alexandre Petrenko, Protocol testing: review of methods and relevance for software testing, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.109-124, August 17-19, 1994, Seattle, Washington, United States [doi>10.1145/186258.187153]
• 263: von Bochmann, G., Petrenko, A., Bellal, O., and Marguiraga, S. 1997. Automating the process of test derivation from SDL specifications. In Proceedings of the 8th SDL forum, INT. Evry, France, 261--276.
• 264: Helene Waeselynck , Salimeh Behnia, B Model Animation for External Verification, Proceedings of the Second IEEE International Conference on Formal Engineering Methods, p.36, December 09-11, 1998
• 265: Aki Watanabe , Ken Sakamura, A specification-based adaptive test case generation strategy for open operating system standards, Proceedings of the 18th international conference on Software engineering, p.81-89, March 25-29, 1996, Berlin, Germany
• 266: Weyuker, E. J. 2002. Thinking formally about testing without a formal specification. In Proceedings of the Conference on Formal Approaches to Testing of Software (Brno, Czech Republic). 1--10.
• 267: E. J. Weyuker , T. J. Ostrand, Theories of Program Testing and the Application of Revealing Subdomains, IEEE Transactions on Software Engineering, v.6 n.3, p.236-246, May 1980 [doi>10.1109/TSE.1980.234485]
• 268: Clazien D. Wezeman, The CO-OP Method for Compositional Derivation of Conformance Testers, Proceedings of the IFIP WG6.1 Ninth International Symposium on Protocol Specification, Testing and Verification IX, p.145-158, June 06-09, 1989
• 269: L. J. White , E. I. Cohen, A Domain Strategy for Computer Program Testing, IEEE Transactions on Software Engineering, v.6 n.3, p.247-257, May 1980 [doi>10.1109/TSE.1980.234486]
• 270: Wimmel, G., Lötzbeyer, H., Pretschner, A., and Slotosch, O. 2000. Specification based test sequence generation with propositional logic. Softw. Test. Verif. Reliab. 10, 229--248.
• 271: Win, T. and Ernst, M. 2002. Verifying distributed algorithms via dynamic analysis and theorem proving. Tech. rep. 841. MIT Laboratory for Computer Science, MIT, Cambridge, MA.
• 272: Woodward, M. R. 1993. Errors in algebraic specifications and an experimental mutation testing tool. IEE/BCS Softw. Eng. J. 8, 4, 211--224.
• 273: B. Yang , H. Ural, Protocol conformance test generation using multiple UIO sequences with overlapping, Proceedings of the ACM symposium on Communications architectures & protocols, p.118-125, September 26-28, 1990, Philadelphia, Pennsylvania, United States
• 274: Mingyu Yao , Alexandre Petrenko , Gregor von Bochmann, Conformance Testing of Protocol Machines without Reset, Proceedings of the IFIP TC6/WG6.1 Thirteenth International Symposium on Protocol Specification, Testing and Verification XIII, p.241-256, May 25-28, 1993
• 275: Yevtushenko, N. V., Lebedev, A. V., and Petrenko, A. F. 1991. On checking experiments with nondeterministic automata. Automat. Contr. Comput. Sci. 6, 81--85.
• 276: Michael Young , Richard N. Taylor, Rethinking the taxonomy of fault detection techniques, Proceedings of the 11th international conference on Software engineering, p.53-62, May 1989, Pittsburgh, Pennsylvania, United States [doi>10.1145/74587.74593]
• 277: Hong Zhu, A Note on Test Oracles and Semantics of Algebraic Specifications, Proceedings of the Third International Conference on Quality Software, p.91, November 06-07, 2003

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
      D.2.5 Testing and Debugging

General Terms:
Reliability, Verification

Keywords:
Software testing, formal methods