Robert M. Hierons
Jonathan P. Bowen
Jeremy Dick
Gerald Lüttgen
Skip Abstract Section
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.
- Abrial, J.-R. 1996. The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge, U.K. Google Scholar
Digital Library
- Aertryck, L. V., Benveniste, M., and Le Metayer, D. 1997. CASTING: A formally based software test generation method. In ICFEM'97: 1st International Conference on Formal Engineering Methods, IEEE (Hiroshima, Japan). Google ScholarDigital Library
- 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.Google Scholar
- Aichernig, B. K. 1999. Automated black-box testing with abstract VDM oracles. In Computer Safety, Reliability and Security: The 18th International Conference, SAFECOMP'99, Toulouse, France, September 1999, M. Felici, K. Kanoun, and A. Pasquini, Eds. Lecture Notes in Computer Science, vol. 1698. Springer-Verlag, Berlin, Germany, 250--259. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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.Google Scholar
- Aichernig, B. K. 2001b. Test-case calculation through abstraction. In Formal Methods Europe (FME 2001), J. N. Oliveira and P. Zave, Eds. Lecture Notes in Computer Science, vol. 2021. Springer-Verlag, Berlin, Germany, 571--589. Google ScholarDigital Library
- Al-Amayreh, A. and Zin, A. M. 1999. PROBE: A formal specification-based testing system. In Proceedings of the 20th International Conference on Information Systems. 400--404. Google ScholarDigital Library
- 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.Google Scholar
- Alur, R., Courcoubetis, C., Henzinger, T., and Ho, P. 1993. Hybrid Automata: An Algorithmic approach to the specification and analysis of hybrid systems. In Hybrid Systems, R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, Eds. Lecture Notes in Computer Science, vol. 736, 209--229. Google ScholarDigital Library
- Alur, R. and Dill, D. 1990. Automata for modeling real-time systems. In Automata, Languages and Programming, 17th International Colloquium, ICALP90. Lecture Notes in Computer Science, vol. 443. Springer-Verlag, Berlin, Germany, 322--335. Google ScholarDigital Library
- Alur, R. and Dill, D. L. 1994. A theory of timed automata. Theoret. Comput. Sci. 126, 2, 183--235. Google ScholarDigital Library
- Alur, R., Grosu, R., Hur, Y., Kumar, V., and Lee, I. 2000. Modular specification of hybrid systems in CHARON. In Hybrid Systems: Computation and Control, Third International Workshop (HSCC). 6--19. Google ScholarDigital Library
- Alur, R. and Kurshan, R. 1996. Timing analysis in COSPAN. In Hybrid Systems III: Verification and Control, Proceedings of the DIMACS/SYCON Workshop, October 22--25, 1995, Rutgers University, New Brunswick, NJ, USA, R. Alur, T. A. Henziger, and E. D. Sontag, Eds. Lecture Notes in Computer Science, vol. 1066, 220--231. Google ScholarDigital Library
- 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.Google Scholar
- 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.Google Scholar
- Ammann, P., Black, P. E., and Majurski, W. 1998. Using model checking to generate tests from specifications. In Proceedings of the 2nd IEEE International Conference on Formal Engineering Methods (ICFEM, Brisbane, Australia). 46--54. Google ScholarDigital Library
- 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.Google Scholar
- 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.Google Scholar
- Antsaklis, P., Kohn, W., Nerode, A., and Sastry, S., Eds. 1995. Hybrid Systems II. Lecture Notes in Computer Science, vol. 999. Springer-Verlag. Google ScholarDigital Library
- Antsaklis, P. J., Ed. 1997. Hybrid Systems IV. Lecture Notes in Computer Science, vol. 1237. Springer-Verlag, Berlin, Germany. Google ScholarDigital Library
- Antsaklis, P. J., Kohn, W., Lemmon, M., Nerode, A., and Sastry, S. 1999. Hybrid Systems. Lecture Notes in Computer Science, vol. 1567. Springer-Verlag.Google Scholar
- Artho, C., Barringer, H., Goldberg, A., Havelund, K., Khurshid, S., Lowry, M., Pasareanu, C., Rosu, G., Sen, K., Visser, W., and Washington, R. 2005. Combining test case generation and runtime verification. Theoret. Comput. Sci. 336, 2--3, 209--234. Google ScholarDigital Library
- Atterer, R. 2000. Automatic test data generation from VDM-SL specifications. M.S. thesis. Queen's University of Belfast, Northern Ireland, U.K.Google Scholar
- 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.Google Scholar
- Ball, T. and Rajamani, S. 2001. Automatically validating temporal safety properties of interfaces. In SPIN 2001. Lecture Notes in Computer Science, vol. 2057. Springer-Verlag, Berlin, Germany, 103--122. Google ScholarDigital Library
- 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.Google Scholar
- Behnia, S. and Waeselynck, H. 1999. Test criteria definition for B models. In Proceedings of the World Congress on Formal Methods. 509--529. Google ScholarDigital Library
- Bengtsson, J., Larsen, K. G., Larson, F., Pettersson, P., and Yi, W. 1995. UppAal: A tool suite for automatic verification of real-time systems. In Hybrid Systems III: Verification and Control, Proceedings of the DIMACS/SYCON Workshop, October 22--25, 1995, Rutgers University, New Brunswick, NJ, USA, R. Alur, T. A. Henzinger, and E. D. Sontag, Eds. Lecture Notes in Computer Science, vol. 1066. Springer, Berlin, Germany, 232--243. Google ScholarDigital Library
- Benjamin, M., Geist, D., Hartman, A., Mas, G., Smeets, R., and Wolfsthal, Y. 1999. A study in coverage-driven test generation. In Proceedings of the 36th Design Automation Conference (DAC). 970--975. Google ScholarDigital Library
- Bernot, G., Gaudel, M.-C., and Marre, B. 1991. Software testing based on formal specifications: A theory and a tool. IEE/BCS Softw. Eng. J. 6, 6, 387--405. Google ScholarDigital Library
- Beyer, D., Chlipala, A., Henzinger, T., Jhala, R., and Majumdar, R. 2004. Generating tests from counterexamples. In Proceedings of the ICSE 2004. IEEE Computer Society Press, Los Alamitos, CA, 326--335. Google ScholarDigital Library
- Bicarregui, J., Dick, J., Matthews, B., and Woods, E. 1997. Making the most of formal specification through animation, testing and proof. Sci. Comput. Program. 29/1--2, 55--80. Google ScholarDigital Library
- Bidoit, M. and Mosses, P. 2003. CASL User Manual: Introduction to Using the Common Algebraic Specification Language. Lecture Notes in Computer Science, vol. 2900. Springer-Verlag, Berlin, Germany. Google ScholarDigital Library
- Bogdanov, K. 2000. Automated testing of Harel's Statecharts. Ph.D. dissertation, The University of Sheffield, Sheffield, U.K.Google Scholar
- Bougé, L., Choquet, N., Fribourg, L., and Gaudel, M.-C. 1986. Test sets generation from algebraic specifications using logic programming. J. Syst. Softw. 6, 4, 343--360. Google ScholarDigital Library
- Bowen, J. P., Bogdanov, K., Clark, J., Harman, M., Hierons, R. M., and Krause, P. 2002. FORTEST: Formal methods and testing. In Proceedings of the 26th IEEE Computer Software and Applications (COMPSAC). 91--101. Google ScholarDigital Library
- 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.Google Scholar
- Brinksma, E. 1988. A theory for the derivation of tests. In Protocol Specification, Testing, and Verification VIII. North-Holland, Amsterdam, The Netherlands, 63--74.Google Scholar
- 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.Google Scholar
- Brinksma, E., Heerink, L., and Tretmans, J. 1998. Factorized test generation for multi-input/output transition systems. In IFIP TC6 11th International Workshop on Testing of Communicating Systems. Kluwer, Dordrecht, The Netherlands, 67--82. Google ScholarDigital Library
- Broekman, B. and Notenboom, E. 2003. Testing Embedded Software. Addison--Wesley, London, U.K. Google ScholarDigital Library
- Bryant, R. E. 1986. Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35, 8, 677--691. Google ScholarDigital Library
- Burton, S. 2002. Automated testing from specifications. Ph.D. dissertation. The University of York, York, U.K.Google Scholar
- Callahan, J., Schneider, F., and Easterbrook, S. 1996. Automated software testing using model-checking. In SPIN '96. Rutgers University, Brunswick, NJ, 118--127.Google Scholar
- Cardell-Oliver, R. 2000. Conformance tests for real-time systems with timed automata specifications. Form. Aspects Comput. 12, 5, 350--371.Google ScholarCross Ref
- 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.Google Scholar
- Cavalli, A. R., Chin, B.-M., and Chon, K. 1996. Testing methods for SDL systems. Comput. Netw. ISDN Syst. 28, 12, 1669--1683. Google ScholarDigital Library
- Cavalli, A. R., Lee, D., Rinderknecht, C., and Zaïdi, F. 1999. Hit-or-Jump: An algorithm for embedded testing with applications to in services. In Proceedings of the Conference on Formal Methods for Protocol Engineering and Distributed Systems (FORTE XII). 41--56. Google ScholarDigital Library
- Chan, W. Y. L., Vuong, S. T., and Ito, M. R. 1989. On test sequence generation for protocols. In Proceedings of the IFIP WG6.1 Ninth International Symposium on Protocol Specification, Testing and Verification. 119--130. Google ScholarDigital Library
- Chang, J. and Richardson, D. 1994. Static and dynamic specification slicing. In Proceedings of the 4th Irvine Software Symposium (Irvine, CA).Google Scholar
- Chen, H. Y., Tse, T. H., Chan, F. T., and Chen, T. Y. 1998. In black and white: An integrated approach to class-level testing of object-oriented programs. ACM Trans. Softw. Eng. Methodol. 7, 3, 250--295. Google ScholarDigital Library
- Chen, H. Y., Tse, T. H., and Chen, T. Y. 2001. TACCLE: A methodology for object-oriented software testing at the class and cluster levels. ACM Trans. Softw. Eng. Methodol. 10, 4, 56--109. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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.Google Scholar
- Chow, T. S. 1978. Testing software design modeled by finite state machines. IEEE Trans. Softw. Eng. 4, 178--187. Google ScholarDigital Library
- 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.Google Scholar
- Cimatti, A., Clarke, E. M., Giunchiglia, F., and Roveri, M. 1999. NuSMV: A new symbolic model verifier. In CAV '99. Lecture Notes in Computer Science, vol. 1464. Springer-Verlag, Berlin, Germany, 495--499. Google ScholarDigital Library
- Clarke, E. M. and Emerson, E. A. 1981. Synthesis of synchronization skeletons for branching time temporal logic. In Workshop on Logics of Programs. Lecture Notes in Computer Science, vol. 131. Springer-Verlag, Berlin, Germany, 52--71. Google ScholarDigital Library
- Clarke, E. M., Emerson, E. A., and Sistala, A. P. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8, 2, 244--263. Google ScholarDigital Library
- Clarke, E. M., Grumberg, O., and Peled, D. 1999. Model Checking. MIT Press, Cambridge, MA. Google ScholarDigital Library
- Clarke, E. M. and Wing, J. M. 1996. Formal methods: State of the art and future directions. ACM Comput. Surv. 28, 4, 626--643. Google ScholarDigital Library
- Clarke, L. A., Hassell, J., and Richardson, D. J. 1982. A close look at domain testing. IEEE Trans. Softw. Eng. 8, 4, 380--390. Google ScholarDigital Library
- Cleaveland, R., Li, T., and Sims, S. 2000. The Concurrency Workbench of the New Century. SUNY, Stony Brook, NY.Google Scholar
- Corbett, J. C., Dwyer, M. B., Hatcliff, J., Laubach, S., Pasareanu, C. S., Robby, and Zheng, H. 2000. Bandera: Extracting finite-state models from Java source code. In Proceedings of the International Conference on Software Engineering. IEEE Computer Society Press, Los Alamitos, CA, 439--448. Google ScholarDigital Library
- 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.Google Scholar
- Cusack, E. and Wezeman, C. 1993. Deriving tests for objects specified in z. In Z User Workshop, London 1992, J. P. Bowen and J. E. Nicholls, Eds. Workshops in Computing. Springer-Verlag, Berlin, Germany, 180--195. Google ScholarDigital Library
- Dauchy, P., Gaudel, M.-C., and Marre, B. 1993. Using algebraic specifications in software testing: A case study on the software of an automatic subway. J. Syst. Softw. 21, 3, 229--244. Google ScholarDigital Library
- Daws, C., Olivero, A., Tripakis, S., and Yovine, S. 1995. The tool kronos. In Hybrid Systems. Lecture Notes in Computer Science, vol. 1066. Springer, Berlin, Germany, 208--219. Google ScholarDigital Library
- de Vries, R. G. and Tretmans, J. 2000. On-the-fly conformance testing using Spin. Softw. Tools Technol. Transf. 2, 4 (Mar.), 382--393.Google Scholar
- DeMillo, R., Lipton, R. J., and Perlis, A. J. 1979. Social processes and proofs of theorems and programs. Commun. ACM 22, 5, 271--280. Google ScholarDigital Library
- Derrick, J. and Boiten, E. 1999. Testing refinements of state-based formal specifications. Softw. Test. Verif. Reliab. 9, 27--50.Google ScholarCross Ref
- Dick, J. and Faivre, A. 1993. Automating the generation and sequencing of test cases from model based specifications. In FME '93: Industrial Strength Formal Methods, J. C. P. Woodcock and P. G. Larsen, Eds. Lecture Notes in Computer Science, vol. 670. Springer-Verlag, Berlin, Germany, 268--284. Google ScholarDigital Library
- Dijkstra, E. W. 1972. Notes of structured programming. In Structured Programming, O. J. Dahl, E. W. Dijkstra, and C. A. R. Hoare, Eds. Academic Press, New York, NY. Google ScholarDigital Library
- Doong, R.-K. and Frankl, P. G. 1991. Case studies on testing object-oriented programs. In The Symposium on Testing, Analysis and Verification (TAV4). ACM Press, New York, NY, 165--177. Google ScholarDigital Library
- Doong, R.-K. and Frankl, P. G. 1994. The ASTOOT approach to testing object-oriented programs. ACM Trans. Softw. Eng. Methodol. 3, 2, 101--130. Google ScholarDigital Library
- Duale, A. Y. and Uyar, M. U. 2004. A method enabling feasible conformance test sequence generation for EFSM models. IEEE Trans. Comput. 53, 5, 614--627. Google ScholarDigital Library
- Eilenberg, S. 1974. Automata, languages and machines. Vol. A. Academic Press, New York, NY. Google ScholarDigital Library
- Eisner, C. 2005. Formal verification of software source code through semi-automatic modeling. Softw. Syst. Model. 4, 1, 14--31.Google ScholarDigital Library
- 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.Google Scholar
- Emerson, E. A. 1990. Temporal and modal logic. In Handbook of Theoretical Computer Science. Vol. B. North-Holland, Amsterdam, The Netherlands, 995--1072. Google ScholarDigital Library
- En-Nouaary, A., Dssouli, R., and Khendek, F. 2002. Timed Wp-method: Testing real-time systems. IEEE Trans. Softw. Eng. 28, 11, 1023--1038. Google ScholarDigital Library
- En-Nouaary, A., Dssouli, R., Khendek, F., and Elqortobi, A. 1998. Timed test cases generation based on state characterization technique. In Proceedings of the IEEE Real-Time Systems Symposium. 220--229. Google ScholarDigital Library
- Engels, A., Feijs, L. M. G., and Mauw, S. 1997. Test generation for intelligent networks using model checking. In Tools and Algorithms for Construction and Analysis of Systems, Third International Workshop, TACAS '97. Lecture Notes in Computer Science, vol. 1217. Springer-Verlag, Berlin, Germany, 384--398. Google ScholarDigital Library
- Ernst, M. D. 2001. Summary of dynamically discovering likely program invariants. In Proceedings of the International Conference on Software Maintenance (ICSM). 540--544. Google ScholarDigital Library
- 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.Google ScholarDigital Library
- Fenton, N., Krause, P., and Neil, M. 2002. Software measurement: Uncertainty and causal modeling. IEEE Softw. 10, 4, 116--122. Google ScholarDigital Library
- Fernandez, J.-C., Jard, C., Jeron, T., and Viho, G. 1996. Using on-the-fly verification techniques for the generation of test suites. In Computer Aided Verification, 8th International Conference, CAV'96, New Brunswick, NJ, USA, July 31-- August 3, 1996, Proceedings, R. Alur and T. A. Henzinger, Eds. Lecture Notes in Computer Science, vol. 1102. Springer, Berlin, Germany, 348--359. Google ScholarDigital Library
- Fetzer, J. H. 1988. Program verification: The very idea. Commun. ACM 31, 9, 1048--1063. Google ScholarDigital Library
- Fletcher, R. and Sajeev, A. S. M. 1996. A framework for testing object-oriented software using formal specifications. In Proceedings of the Ada-Europe'96, International Conference on Reliable Software Technologies (Montreux, Switzerland). 159--170. Google ScholarDigital Library
- Formal Systems (Europe) Ltd. 1997. Failures-Divergence Refinement: FDR2 User Manual. Formal Systems (Europe) Ltd. Oxford, U.K.Google Scholar
- 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.Google Scholar
- Fujiwara, S., von Bochmann, G., Khendek, F., Amalou, M., and Ghedamsi, A. 1991. Test selection based on finite state models. IEEE Trans. Softw. Eng. 17, 6, 591--603. Google ScholarDigital Library
- Gannon, J., McMullin, P., and Hamlet, R. 1981. Data-abstraction implementation, specification, and testing. ACM Trans. Program. Lang. Syst. 3, 2, 211--223. Google ScholarDigital Library
- Garavel, H. and Hermanns, H. 2002. On combining functional verification and performance evaluation using CADP. In Proceedings of the International Symposium of Formal Methods Europe (FME). 410--429. Google ScholarDigital Library
- Gargantini, A. and Heitmeyer, C. 1999. Using model checking to generate tests from requirements specifications. In ESEC '99. Lecture Notes in Computer Science, vol. 1687. Springer-Verlag, Berlin, Germany, 146--162. Google ScholarDigital Library
- Gaudel, M.-C. 1995. Testing can be formal too. In TAPSOFT '95. Springer-Verlag, Berlin, Germany, 82--96. Google ScholarDigital Library
- Gaudel, M.-C. 2001. Testing from formal specifications, a generic approach. In Ada--Europe. Lecture Notes in Computer Science, vol. 2043. Springer-Verlag, Berlin, Germany, 35--48. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- Gerrard, C. P., Coleman, D., and Gallimore, R. M. 1990. Formal specification and design time testing. IEEE Trans. Softw. Eng. 16, 1, 1--12. Google ScholarDigital Library
- Gill, A. 1962. Introduction to the Theory of Finite-State Machines. McGraw-Hill, New York, NY.Google Scholar
- 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.Google ScholarCross Ref
- Godefroid, P. 1996. Partial-Order Methods for the Verification of Concurrent Systems—An Approach to the State-Explosion Problem. Lecture Notes in Computer Science, vol. 1032. Springer-Verlag, New York, NY. Google ScholarDigital Library
- Godefroid, P. 1997. Model checking for programming languages using VeriSoft. In Principles of Programming Languages. ACM Press, New York, NY, 174--186. Google ScholarDigital Library
- Godhavn, J.-M., Lauvdal, T., and Egeland, O. 1996. Hybrid control in sea traffic management systems. In Hybrid Systems III. Lecture Notes in Computer Science, vol. 1066, Springer, Berlin, Germany, 149--160. Google ScholarDigital Library
- Goguen, J. A. and Malcolm, G. 2000. Software Engineering with OBJ: Algebraic Specifications in Action. Kluwer Academic Publishers, Dordrecht, The Netherlands.Google Scholar
- 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.Google Scholar
- Gonenc, G. 1970. A method for the design of fault detection experiments. IEEE Trans. Comput. 19, 551--558. Google ScholarDigital Library
- Goodenough, J. B. and Gerhart, S. L. 1975. Toward a theory of test data selection. IEEE Trans. Softw. Eng. 1, 2, 156--173.Google ScholarDigital Library
- Gotlieb, A., Botella, B., and Rueher, M. 1998. Automatic test data generation using constraint solving techniques. In Proceedings of ISSTA '98. ACM Press, New York, NY, 53--62. Google ScholarDigital Library
- Grieskamp, W., Gurevich, Y., Schulte, W., and Veanes, M. 2002. Generating finite state machines from abstract state machines. In Proceedings of the ACM SIGSOFT Symposium on Software Testing and Analysis. 112--122. Google ScholarDigital Library
- Groce, A., Peled, D., and Yannakakis, M. 2002. Adaptive model checking. In TACAS 2002. Lecture Notes in Computer Science, vol. 2280. Springer-Verlag, Berlin, Germany, 357--370. Google ScholarDigital Library
- Gunter, E. and Peled, D. 2005. Model checking, testing and verification working together. Form. Aspects Comput. 17, 201--221. Google ScholarCross Ref
- Gupta, V., Jagadeesan, R., and Saraswat, V. A. 1998. Computing with continuous change. Sci. Comput. Program. 30, 1--2, 3--49. Google ScholarDigital Library
- 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.Google Scholar
- Hamlet, R. 1989. Theoretical comparison of testing methods. In Proceedings of the Third Symposium on Testing, Analysis and Verification. ACM Press, New York, NY, 28--37. Google ScholarDigital Library
- Harder, M. 2002. Improving test suites via generated specifications. Tech. rep. 848. Department of EECS. Cambridge, MA.Google Scholar
- Harel, D. and Gery, E. 1997. Executable object modeling with Statecharts. IEEE Comput., 30, 7, 31--42. Google ScholarDigital Library
- Harman, M., Hu, L., Hierons, R. M., Wegener, J., Sthamer, H., Baresel, A., and Roper, M. 2004. Testability transformation. IEEE Trans. Softw. Eng. 30, 1, 3--16. Google ScholarDigital Library
- Havelund, K. and Pressburger, T. 1998. Model checking Java programs using Java PathFinder. Softw. Tools Technol. Transf. 2, 4, 366--381.Google ScholarCross Ref
- Havelund, K. and Rosu, G. 2004. An overview of the runtime verification tool Java PathExplorer. Form. Meth. Syst. Des. 24, 2, 189--215. Google ScholarDigital Library
- Hayes, I. J. 1986. Specification directed module testing. IEEE Trans. Softw. Eng. 12, 1, 124--133. Google ScholarDigital Library
- Helke, S., Neustupny, T., and Santen, T. 1997. Automating test case generation from Z specifications with Isabelle. In ZUM '97: The Z Formal Specification Notation, J. P. Bowen, M. G. Hinchey, and D. Till, Eds. Lecture Notes in Computer Science, vol. 1212. Springer-Verlag, Berlin, Germany, 52--71. Google ScholarDigital Library
- Hennie, F. C. 1964. Fault-detecting experiments for sequential circuits. In Proceedings of the 5th Annual Symposium on Switching Circuit Theory and Logical Design. 95--110. Google ScholarDigital Library
- 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.Google Scholar
- Henzinger, T. A., Kupferman, O., and Vardi, M. Y. 1996. A space-efficient on-the-fly algorithm for real-time model checking. In CONCUR '96. Lecture Notes in Computer Science, vol. 1119. Springer-Verlag, Berlin, Germany, 514--529. Google ScholarDigital Library
- Hierons, R. M. 1997a. Testing from a finite state machine: Extending invertibility to sequences. Comput. J. 40, 4, 220--230.Google ScholarCross Ref
- Hierons, R. M. 1997b. Testing from a Z specification. Softw. Test. Verif. Reliab. 7, 1, 19--33.Google ScholarCross Ref
- 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.Google Scholar
- Hierons, R. M. 2002. Comparing tests in the presence of hypotheses. ACM Trans. Softw. Eng. Methodol. 11, 4, 427--448. Google ScholarDigital Library
- Hierons, R. M. 2004a. Minimizing the number of resets when testing from a finite state machine. Inform. Process. Lett. 90, 6, 287--292. Google ScholarDigital Library
- Hierons, R. M. 2004b. Testing from a non-deterministic finite state machine using adaptive state counting. IEEE Trans. Comput. 53, 10, 1330--1342. Google ScholarDigital Library
- Hierons, R. M. and Harman, M. 2000. Testing comformance to a quasi-non-determinstic stream X-machine. Form. Aspects Comput. 12, 6, 423--442.Google ScholarCross Ref
- Hierons, R. M. and Harman, M. 2004. Testing conformance of a deterministic implementation to a non--deterministic stream X--machine. Theoret. Comput. Sci. 323, 1--3, 191--233. Google ScholarDigital Library
- Hierons, R. M., Kim, T.-H., and Ural, H. 2004. On the testability of SDL specifications. Comput. Netw. 44, 5, 681--700. Google ScholarDigital Library
- Hierons, R. M., Sadeghipour, S., and Singh, H. 2001. Testing a system specified using Statecharts and Z. Inform. Softw. Technol. 43, 2, 137--149.Google ScholarCross Ref
- Hierons, R. M. and Ural, H. 2006. Optimizing the length of checking sequences. IEEE Trans. Comput. 55, 5, 618--629. Google ScholarDigital Library
- Hoare, C. A. R. 1985. Communicating Sequential Processes. Prentice Hall International Series in Computer Science. Prentice Hall, Englewood Cliffs, NJ. Google ScholarDigital Library
- Hoare, C. A. R. 1996. How did software get so reliable without proof? In Cost 237 Workshop, D. Hutchison, H. Christiansen, G. Coulson, and A. S. Danthine, Eds. Lecture Notes in Computer Science, vol. 1052. Springer, Berlin, Germany, 1--17. Google ScholarDigital Library
- Holcombe, M. and Ipate, F. 1998. Correct Systems: Building a Business Process Solution. Springer-Verlag, Berlin, Germany.Google ScholarCross Ref
- Holzmann, G. 2003. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading, MA. Google ScholarDigital Library
- Holzmann, G. J. 1996. On-the-fly model checking. ACM Comput. Surv. 28, 4, 120--120. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- Hong, H., Cha, S., Lee, I., Sokolsky, O., and Ural, H. 2003. Data flow testing as model checking. In Proceedings of ICSE 2003. IEEE Computer Society Press, Los Alamitos, CA, 232--243. Google ScholarDigital Library
- Hong, H., Lee, I., Sokolsky, O., and Ural, H. 2002. A temporal logic based theory of test coverage and generation. In TACAS 2002. Lecture Notes in Computer Science, vol. 2280. Springer-Verlag, Berlin, Germany, 327--341. Google ScholarDigital Library
- 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.Google Scholar
- Hörcher, H.-M. and Peleska, J. 1995. Using formal specifications to support software testing. Softw. Qual. J. 4, 4, 309--327.Google ScholarCross Ref
- Hörl, J. and Aichernig, B. K. 2000. Validating voice communication requirements using lightweight formal methods. IEEE Softw. 17, 3, 21--27. Google ScholarDigital Library
- Hsieh, E. P. 1971. Checking experiments for sequential machines. IEEE Trans. Comput. 20, 1152--1166. Google ScholarDigital Library
- Huber, F., Schätz, B., and Einert, G. 1997. Consistent graphical specification of distributed systems. In Proceedings of the 4th International Symposium of Formal Methods Europe (FME). 122--141. Google ScholarDigital Library
- Hughes, M. and Stotts, D. 1996. Daistish: Systematic algebraic testing for OO programs in the presence of side-effects. In Proceedings of the International Symposium on Software Testing and Analysis. ACM Press, New York, NY, 53--61. Google ScholarDigital Library
- Hur, Y., Fierro, R. B., and Lee, I. 2003. Modeling distributed autonomous robots using CHARON: Formation control case study. In Proceedings of the 6th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC). 93--98. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- Ipate, F. and Holcombe, M. 2000. Generating test sets from non-deterministic stream X-machines. Form. Aspects Comput. 12, 6, 443--458.Google ScholarCross Ref
- 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.Google Scholar
- ISO. 1989b. ISO 9074; Estelle—A Formal Description Technique Based on an Extended State Transition Model. ISO, Geneva, Switzerland.Google Scholar
- ITU-T. 1997. Recommendation Z.500 Framework on Formal Methods in Conformance Testing. International Telecommunications Union, Geneva, Switzerland.Google Scholar
- ITU-T. 1999. Recommendation Z.100 Specification and Description Language (SDL). International Telecommunications Union, Geneva, Switzerland.Google Scholar
- Jackson, D. and Vaziri, M. 2000. Finding bugs with a constraint solver. In ISSTA'00: Proceedings of the International Symposium on Software Testing and Analysis. ACM Press, New York, NY, 14--25. Google ScholarDigital Library
- 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.Google Scholar
- 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.Google Scholar
- Jard, C. and Jéron, T. 2005. TGV: Theory, principles and algorithms. Int. J. Softw. Tools Technol. Trans. 7, 4, 297--315. Google ScholarDigital Library
- Jones, C. B. 1991. Systematic Software Development using VDM, 2nd ed. Prentice Hall International Series in Computer Science. Prentice Hall, Englewood Cliffs, NJ. Google ScholarDigital Library
- Kemmerer, R. A. 1985. Testing formal specifications to detect design errors. IEEE Trans. Softw. Eng. 11, 1, 32--43. Google ScholarDigital Library
- Kerbrat, A., Jéron, T., and Groz, R. 1999. Automated test generation from SDL specifications. In SDL For. 135--152.Google Scholar
- Kernighan, B. W. and Plauger, P. J. 1981. Software Tools in Pascal. Addison-Wesley, Reading, MA. Google ScholarDigital Library
- King, S., Hammond, J., Chapman, R., and Pryor, A. 2000. Is proof more cost-effective than testing? IEEE Trans. Softw. Eng. 26, 8 (Aug.), 675--686. Google ScholarDigital Library
- Kohavi, Z. 1978. Switching and Finite State Automata Theory. McGraw-Hill, New York, NY.Google Scholar
- 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.Google ScholarCross Ref
- Koné, O. 2001. A local approach to the testing of real-time systems. Comput. J. 44, 5, 435--447.Google ScholarCross Ref
- Krichen, M. and Tripakis, S. 2004. Black-box conformance testing for real-time systems. In Proceedings of the 11th International SPIN Workshop. 109--126.Google Scholar
- 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.Google Scholar
- Kuhn, D. R. 1999. Fault classes and error detection capability of specification--based testing. ACM Trans. Softw. Eng. Methodol. 8, 4, 411--424. Google ScholarDigital Library
- Lau, M. F. and Yu, Y.-T. 2005. An extended fault class hierarchy for specification-based testing. ACM Trans. Softw. Eng. Methodol. 14, 3, 247--276. Google ScholarDigital Library
- Leduc, G. 1991. Conformance relation, associated equivalence, and a new canonical tester in LOTOS. In Protocol Specification, Testing, and Verification XI. Elsevier (North-Holland), Amsterdam, The Netherlands, 249--264. Google ScholarDigital Library
- Lee, D. and Yannakakis, M. 1994. Testing finite-state machines: State identification and verification. IEEE Trans. Comput. 43, 3, 306--320. Google ScholarDigital Library
- Lee, D. and Yannakakis, M. 1996. Principles and methods of testing finite-state machines. Proc. IEEE 84, 8, 1089--1123.Google ScholarCross Ref
- Legeard, B., Peureux, F., and Utting, M. 2002a. Automated boundary testing from Z and B. In Formal Methods Europe (FME 02). Lecture Notes in Computer Science, vol. 2391. Springer, Berlin, Germany, 21--40. Google ScholarDigital Library
- Legeard, B., Peureux, F., and Utting, M. 2002b. A comparison of the BTT and TTF test-generation methods. In Proceedings of the Conference on Formal Specification and Development in Z and B (ZB). 309--329. Google ScholarDigital Library
- Lestiennes, G. and Gaudel, M.-C. 2002. Testing processes from formal specifications with inputs, outputs and data types. In Proceedings of the 13th International Symposium on Software Reliability Engineering (ISSRE). 3--14. Google ScholarDigital Library
- Lichtenstein, O. and Pnueli, A. 1985. Checking that finite state concurrent programs satisfy their linear specification. In Principles of Programming Languages. IEEE Computer Society Press, Los Alamitos, CA, 97--107. Google ScholarDigital Library
- Littlewood, B. 2005. CASTING: Dependability assessment of software-based systems: State of the art. In ICSE'05: Proceedings of the 27th International Conference on Software Engineering. 6--7. Google ScholarDigital Library
- Liu, S. 1999. Verifying consistency and validity of formal specifications by testing. In World Congress on Formal Methods, J. Wing, J. Woodcock, and J. Davies, Eds. Lecture Notes in Computer Science, vol. 1708. Springer-Verlag, Berlin, Germany, 896--914. Google ScholarDigital Library
- Liu, S., Fukuzaki, T., and Miyamoto, K. 2000. A GUI and testing tool for SOFL. In APSEC 2000: Proceedings of the 7th Asia-Pacific Software Engineering Conference. IEEE Computer Society Press, Los Alamitos, CA, 421--425. Google ScholarDigital Library
- 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.Google Scholar
- Luo, G. L., Petrenko, A., and von Bochmann, G. 1994a. Selecting test sequences for partially-specified nondeterministic finite state machines. In Proceedings of the 7th IFIP Workshop on Protocol Test Systems. Chapman and Hall, London, U.K., 95--110. Google ScholarDigital Library
- Luo, G. L., von Bochmann, G., and Petrenko, A. 1994b. Test selection based on communicating nondeterministic finite-state machines using a generalized Wp-method. IEEE Trans. Softw. Eng. 20, 2, 149--161. Google ScholarDigital Library
- 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.Google Scholar
- 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.Google Scholar
- Machado, P. D. L. 2000. Testing from structured algebraic specifications. In Proceedings of the Algebraic Methodology and Software Technology (AMAST). 529--544. Google ScholarDigital Library
- Manna, Z. and Pnueli, A. 1992. Verifying hybrid systems. In Hybrid Systems. Lecture Notes in Computer Science, vol. 736. Springer-Verlag, Berlin, Germany, 4--35. Google ScholarDigital Library
- Manna, Z. and Pnueli, A. 1995. Temporal Verification of Reactive Systems. Springer-Verlag, Berlin, Germany. Google ScholarDigital Library
- Marinov, D. and Khurshid, S. 2001. TestEra: A novel framework for automated testing of Java programs. In Proceedings of the 16th IEEE Conference on Automated Software Engineering (ASE). Google ScholarDigital Library
- Marre, B. 1995. LOFT: A tool for assisting selection of test data sets from algebraic specifications. In TAPSOFT'95: Theory and Practice of Software Development. Lecture Notes in Computer Science, vol. 915. Springer, Berlin, Germany, 799--800. Google ScholarDigital Library
- Marriott, K. and Stuckey, P. 1998. Programming with Constraints: An Introduction. MIT Press, Cambridge, MA.Google ScholarCross Ref
- McMillan, K. L. 1993. Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht, The Netherlands. Google ScholarDigital Library
- McMullin, P. R. and Gannon, J. D. 1983. Combining testing with formal specifications: A case study. IEEE Trans. Softw. Eng. 9, 3, 328--335. Google ScholarDigital Library
- Meudec, C. 1997. Automatic generation of software tests from formal specifications. Ph.D. dissertation, Queen's University of Belfast, Northern Ireland, U.K.Google Scholar
- Miao, H., Gao, X., and Liu, L. 1999. An approach to testing the nonexistence of initial state in Z specifications. In Proceedings of the Test Symposium. (ATS) . 289--294. Google ScholarDigital Library
- Mikk, E. 1995. Compilation of Z specifications into C for automatic test result evaluation. In ZUM '95: The Z Formal Specification Notation, 9th International Conference of Z Users. Springer-Verlag, Berlin, Germany, 167--180. Google ScholarDigital Library
- MIL-STD 188-220B. 1998. Military Standard-Interoperability Standard for Digital Message Device Subsystems. Department of Defense, Washington, DC.Google Scholar
- Miller, R. E. and Paul, S. 1993. On the generation of minimal length conformance tests for communications protocols. IEEE/ACM Trans. Network. 1, 1, 116--129. Google ScholarDigital Library
- Milner, R. 1989. Communication and Concurrency. Prentice Hall International Series in Computer Science. Prentice Hall, Englewood Cliffs, NJ. Google ScholarDigital Library
- Moore, E. P. 1956. Gedanken-experiments. In Automata Studies, C. Shannon and J. McCarthy, Eds. Princeton University Press, Princeton, NJ.Google Scholar
- Mosses, P. D. 2004. CASL Reference Manual: The Complete Documentation of the Common Algebraic Specification Language. Lecture Notes in Computer Science, vol. 2960. Springer-Verlag, Berlin, Germany. Google ScholarDigital Library
- MOST Cooperation. 2002. MOST media oriented system transport—multimedia and control networking technology. MOST Cooperation. Karlsruhe, Germany.Google Scholar
- Murray, L., Carrington, D., MacColl, I., McDonald, J., and Strooper, P. 1998. Formal derivation of finite state machines for class testing. In 11th International Conference of Z Users. Lecture Notes in Computer Science, vol. 1493. Springer, Berlin, Germany, 42--59. Google ScholarDigital Library
- Naito, S. and Tsunoyama, M. 1981. Fault detection for sequential machines. In Proceedings of the IEEE Fault Tolerant Computing Conference. 238--243.Google Scholar
- Nielsen, B. and Skou, A. 2003. Automated test generation from timed automata. Softw. Tools Technol. Transf. 5, 1, 59--77.Google ScholarDigital Library
- 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.Google Scholar
- Offutt, J. and Liu, S. 1999. Generating test data from SOFL specifications. J. Syst. Softw. 49, 1, 49--62. Google ScholarDigital Library
- Ostrand, T. J. and Balcer, M. J. 1988. The category-partition method for specifying and generating functional tests. Commun. ACM 31, 6, 676--686. Google ScholarDigital Library
- 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.Google Scholar
- Peled, D. 1998. Ten years of partial order reduction. In Computer Aided Verification, 10th International Conference (CAV '98). Lecture Notes in Computer Science, vol. 1427. Springer-Verlag, Berlin, Germany, 17--28. Google ScholarDigital Library
- 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.Google Scholar
- Peled, D., Vardi, M., and Yannakakis, M. 2002. Black box checking. J. Automat. Lang. Combin. 7, 2, 225--246. Google ScholarDigital Library
- Petrenko, A. 1991. Checking experiments with protocol machines. In Protocol Test Systems. IFIP Transactions. North-Holland, Amsterdam, The Netherlands, 83--94. Google ScholarDigital Library
- Petrenko, A. 2001. Fault model-driven test derivation from finite state models: Annotated bibliography. Lecture Notes in Computer Science, vol. 2067. Springer, Berlin, Germany, 196--205. Google ScholarDigital Library
- Petrenko, A., Boroday, S., and Groz, R. 1999. Configurations in EFSM. In Proceedings of the IFIP Joint International Conference on Formal Description Techniques for Distributed Systems (FORTE XII) and Communication Protocols, and Protocol Specification, Testing, and Verification (PSTV XIX, China). 5--24. Google ScholarDigital Library
- Petrenko, A., Boroday, S., and Groz, R. 2004. Confirming configurations in EFSM testing. IEEE Trans. Softw. Eng. 30, 1, 29--42. Google ScholarDigital Library
- Petrenko, A., Yevtushenko, N., Lebedev, A., and Das, A. 1994. Nondeterministic state machines in protocol conformance testing. In Protocol Test Systems, VI (C-19). Elsevier Science (North-Holland), Amsterdam, The Netherlands, 363--378. Google ScholarDigital Library
- Petrenko, A., Yevtushenko, N., and von Bochmann, G. 1996. Testing deterministic implementations from nondeterministic FSM specifications. In Proceedings of the 9th International Workshop on Testing of Communicating Systems (IWTCS). 125--140. Google ScholarDigital Library
- Phalippou, M. 1994. Executable testers. In Protocol Test Systems VI. North-Holland, Amsterdam, The Netherlands, 35--50. Google ScholarDigital Library
- Pnueli, A. 1977. The temporal logic of programs. In Proceedings of FOCS. IEEE Computer Society Press, Los Alamitos, CA, 46--57. Google ScholarDigital Library
- Pretschner, A., Prenninger, W., Wagner, S., Kühnel, C., Baumgartner, M., Sostawa, B., Zölch, R., and Stauner, T. 2005. One evaluation of model-based testing and its automation. In Proceedings of the 27th ACM/IEEE International Conference on Software Engineering (ICSE, St. Louis, MO), 392--401. Google ScholarDigital Library
- Queille, J. P. and Sifakis, J. 1982. Specification and verification of concurrent systems in CESAR. In International Symposium on Programming. Lecture Notes in Computer Science, vol. 137. Springer-Verlag, Berlin, Germany, 337--351. Google ScholarDigital Library
- Ravn, A. P., Rischel, H., Conrad, F., and Andersen, T. O. 1995. Hybrid control of a robot—a case study. In Hybrid Systems II. Lecture Notes in Computer Science, vol. 999, Springer, Berlin, Germany, 391--404. Google ScholarDigital Library
- Rice, M. D. and Seidman, S. B. 1998. An approach to architectural analysis and testing. In Proceedings of the 3rd International Workshop on Software Architecture. ACM Press, New York, NY, 121--123. Google ScholarDigital Library
- Richardson, D., Aha, S. L., and O'Malley, T. O. 1992. Specification-based test oracles for reactive systems. In Proceedings of the 14th IEEE International Conference on Software Engineering. 105--118. Google ScholarDigital Library
- Richardson, D. J. and Clarke, L. A. 1985. Partition analysis: A method combining testing and verification. IEEE Trans. Softw. Eng. 14, 12, 1477--1490. Google ScholarDigital Library
- Robinson, A. and Voronkov, A. 2001. Handbook of Automated Reasoning. MIT Press, Cambridge, MA. Google ScholarDigital Library
- Sabnani, K. and Dahbura, A. 1998. A protocol test generation procedure. Comput. Netw. 15, 4, 285--297. Google ScholarDigital Library
- Sato, F., Munemori, J., Ideguchi, T., and Mizuno, T. 1989. Sequence generation tool for communication system. In Proceedings of the 2nd International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE). Google ScholarDigital Library
- Schmitt, M., Ek, A., Grabowski, J., Hogrefe, D., and Koch, B. 1998. Autolink—putting SDL-based test generation into practice. In Testing of Communicating Systems, IFIP TC6 11th International Workshop on Testing Communicating Systems (IWTCS). Kluwer Academic Publishers, Amsterdam, The Netherlands, 227--244. Google ScholarDigital Library
- Sidhu, D. P. and Leung, T.-K. 1989. Formal methods for protocol testing: A detailed study. IEEE Trans. Softw. Eng. 15, 4, 413--426. Google ScholarDigital Library
- Sims, S. 1999. The Process Algebra Compiler User's Manual. Reactive Systems, Inc., Falls Church, VA.Google Scholar
- Singh, H., Conrad, M., and Sadeghipour, S. 1997. Test case design based on Z and the classification-tree method. In Proceedings of the 1st IEEE Conference on Formal Engineering Methods. IEEE Computer Society Press, Los Alamitos, CA, 81--90. Google ScholarDigital Library
- Spivey, J. M. 1988. Understanding Z: A Specification Language and its Formal Semantics. Cambridge University Press, Cambridge, U.K. Google ScholarDigital Library
- Spivey, J. M. 1992. The Z Notation: A Reference Manual, 2nd ed. Prentice Hall International Science in Computer Science, Prentice Hall, Englewood Cliffs, NJ. Google ScholarDigital Library
- Stauner, T., Muller, O., and Fuchs, M. 1997. Using HYTECH to verify an automotive control system. Lecture Notes in Computer Science, vol. 201. Springer, Berlin, Germany, 139--153. Google ScholarDigital Library
- Stepney, S. 1995. Testing as abstraction. In The Z Formal Specification Notation (ZUM 95). Lecture Notes in Computer Science, vol. 967. Springer, Berlin, Germany, 137--151. Google ScholarDigital Library
- Stirling, C. 1992. Modal and temporal logics. In Handbook of Logic in Computer Science. Vol. 2. Oxford University Press, Oxford, U.K., 477--563. Google ScholarDigital Library
- Stocks, P. A. 1993. Applying formal methods to software testing. Ph.D. dissertation, University of Queensland, Brisbane, Australia.Google Scholar
- Stocks, P. A. and Carrington, D. A. 1996. A framework for specification-based testing. IEEE Trans. Softw. Eng. 22, 11 (Nov.), 777--793. Google ScholarDigital Library
- 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.Google Scholar
- 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.Google Scholar
- Tracey, N., Clark, J., Mander, K., and McDermid, J. 2000. Automated test-data generation for exception conditions. Softw. Prac. Exp. 30, 1, 61--79. Google ScholarDigital Library
- Treharne, H., Draper, J., and Schneider, S. 1998. Test case preparation using a prototype. In B'98: 2nd International B Conference, Recent Advances in the Development and Use of the B Method, D. Bert, Ed. Lecture Notes in Computer Science, vol. 1393. Springer-Verlag, Berlin, Germany, 293--311. Google ScholarDigital Library
- Tretmans, J. 1996. Conformance testing with labeled transitions systems: Implementation relations and test generation. Comput. Network. ISDN Syst. 29, 1, 49--79. Google ScholarDigital Library
- 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.Google Scholar
- Tsuchiya, T. and Kikuno, T. 2002. On fault classes and error detection capability of specification-based testing. ACM Trans. Softw. Eng. Methodol. 11, 1, 58--62. Google ScholarDigital Library
- 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.Google ScholarDigital Library
- Ural, H., Wu, X., and Zhang, F. 1997. On minimizing the lengths of checking sequences. IEEE Trans. Comput. 46, 1, 93--99. Google ScholarDigital Library
- 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).Google Scholar
- 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.Google ScholarCross Ref
- Valmari, A. 1990. A stubborn attack on the state explosion problem. In Proceedings of Computer Aided Verification, 2nd International Workshop (CAV). DIMACS, vol. 3. AMS, Providence, RI, 25--42. Google ScholarDigital Library
- Varaiya, P. 1993. Smart cars on smart roads. IEEE Trans. Automat. Cont. 38, 2, 195--207.Google ScholarCross Ref
- 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.Google Scholar
- Vasilevskii, M. P. 1973. Failure Diagnosis of Automata. Cybernetics. Plenum Publishing Corporation, New York, NY.Google Scholar
- Vilkomir, S. A. and Bowen, J. P. 2001. Formalization of software testing criteria using the Z notation. In Proceedings of the 25th Annual International Computer Software and Applications Conference (COMPSAC, Chicago, IL). IEEE Computer Society, Los Alamitos, CA, 351--356. Google ScholarDigital Library
- Vilkomir, S. A. and Bowen, J. P. 2002. Reinforced condition/decision coverage (RC/DC): A new criterion for software testing. In Proceedings of the 2nd International Conference of B and Z Users (ZB). 291--308. Google ScholarDigital Library
- von Bochmann, G. and Petrenko, A. 1994. Protocol testing: Review of methods and relevance for software testing. In Proceedings of the ACM International Symposium on Software Testing and Analysis (Seattle, WA). 109--123. Google ScholarDigital Library
- 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.Google Scholar
- Waeselynck, H. and Behnia, S. 1998. B model animation for external verification. In Proceedings of the 2nd International Conference on Formal Engineering Methods. 36--45. Google ScholarDigital Library
- Watanabe, A. and Sakamura, K. 1996. A specification-based adaptive test case generation strategy for open operating system standards. In Proceedings of the 18th ACM International Conference on Software Engineering. 81--89. Google ScholarDigital Library
- 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.Google Scholar
- Weyuker, E. J. and Ostrand, T. J. 1980. Theories of program testing and the the application of revealing subdomains. IEEE Trans. Softw. Eng. 6, 3, 236--246. Google ScholarDigital Library
- Wezeman, C. D. 1989. The CO-OP method for compositional derivation of conformance testers. In Protocol Specification, Testing, and Verification IX. Elsevier (North-Holland), Amsterdam, The Netherlands, 145--158. Google ScholarDigital Library
- White, L. J. and Cohen, E. I. 1980. A domain strategy for computer program testing. IEEE Trans. Softw. Eng. 6, 3 (May), 247--257. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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.Google Scholar
- Woodward, M. R. 1993. Errors in algebraic specifications and an experimental mutation testing tool. IEE/BCS Softw. Eng. J. 8, 4, 211--224.Google ScholarCross Ref
- Yang, B. and Ural, H. 1990. Protocol conformance test generation using multiple UIO sequences with overlapping. In Proceedings of ACM SIGCOMM 90: Communications, Architectures, and Protocols (Twente, The Netherlands). 118--125. Google ScholarDigital Library
- Yao, M., Petrenko, A., and von Bochmann, G. 1993. Conformance testing of protocol machines without reset. In Protocol Specification, Testing and Verification, XIII (C-16). Elsevier (North-Holland), Amsterdam, The Netherlands, 241--256. Google ScholarDigital Library
- Yevtushenko, N. V., Lebedev, A. V., and Petrenko, A. F. 1991. On checking experiments with nondeterministic automata. Automat. Contr. Comput. Sci. 6, 81--85.Google Scholar
- Young, M. and Taylor, R. N. 1989. Rethinking the taxonomy of fault detection techniques. In Proceedings of the IEEE/ACM International Conference on Sofware Engineering. 53--62. Google ScholarDigital Library
- Zhu, H. 2003. A note on test oracles and semantics of algebraic specifications. In Proceedings of the Third International Conference on Quality Software (QSIC, Dallas, TX). 91--98. Google ScholarDigital Library
Index Terms
- Using formal specifications to support testing
Recommendations
Using Modechart Modules for Testing Formal Specifications
HASE '99: The 4th IEEE International Symposium on High-Assurance Systems EngineeringAutomated 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 ...
A Formal Framework for ASTRAL Intralevel Proof Obligations
ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL ...
Automated test case generation from IFAD VDM++ specifications
SEPADS'05: Proceedings of the 4th WSEAS International Conference on Software Engineering, Parallel & Distributed SystemsMost 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