Combining test case generation and runtime verification. (English) Zbl 1080.68062
Summary: Software testing is typically an ad hoc process where human testers manually write test inputs and descriptions of expected test results, perhaps automating their execution in a regression suite. This process is cumbersome and costly. This paper reports results on a framework to further automate this process. The framework consists of combining automated test case generation based on systematically exploring the input domain of the program with runtime verification, where execution traces are monitored and verified against properties expressed in temporal logic. Capabilities also exist for analyzing traces for concurrency errors, such as deadlocks and data races. The input domain of the program is explored using a model checker extended with symbolic execution. Properties are formulated in an expressive temporal logic. A methodology is advocated that automatically generates properties specific to each input rather than formulating properties uniformly true for all inputs. The paper describes an application of the technology to a NASA rover controller.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
Keywords:
Automated testing; Test case generation; Model checking; Symbolic execution; Runtime verification; Temporal logic; Concurrency analysis; NASA rover controllerReferences:
| [1] | AGEDIS—model based test generation tools, http://www.agedis.de; AGEDIS—model based test generation tools, http://www.agedis.de |
| [2] | P. Ammann, P. Black, A specification-based coverage metric to evaluate test sets, in: Proc. Fourth IEEE Internat. Symp. on High Assurance Systems and Engineering, November 1999, pp. 239-248.; P. Ammann, P. Black, A specification-based coverage metric to evaluate test sets, in: Proc. Fourth IEEE Internat. Symp. on High Assurance Systems and Engineering, November 1999, pp. 239-248. |
| [3] | C. Artho, K. Havelund, A. Biere, High-level data races, Journal on Software Testing, Verification and Reliability (STVR) 13 (4) (2003).; C. Artho, K. Havelund, A. Biere, High-level data races, Journal on Software Testing, Verification and Reliability (STVR) 13 (4) (2003). |
| [4] | C. Artho, V. Schuppan, A. Biere, P. Eugster, M. Baur, B. Zweimüller, JNuke: efficient dynamic analysis for Java, in: Proc. CAV’04: Computer Aided Verification, Lecture Notes in Computer Science, Springer, Berlin, 2004.; C. Artho, V. Schuppan, A. Biere, P. Eugster, M. Baur, B. Zweimüller, JNuke: efficient dynamic analysis for Java, in: Proc. CAV’04: Computer Aided Verification, Lecture Notes in Computer Science, Springer, Berlin, 2004. · Zbl 1103.68602 |
| [5] | M. Barnett, W. Schulte, Contracts, components, and their runtime verification, Technical Report MSR-TR-2002-38, Microsoft Research, April 2002, Download: http://research.microsoft.com/fse; M. Barnett, W. Schulte, Contracts, components, and their runtime verification, Technical Report MSR-TR-2002-38, Microsoft Research, April 2002, Download: http://research.microsoft.com/fse |
| [6] | Barringer, H.; Fisher, M.; Gabbay, D.; Gough, G.; Owens, R., METATEMan introduction, Formal Aspects Comput., 7, 5, 533-549 (1995) · Zbl 0838.68014 |
| [7] | H. Barringer, A. Goldberg, K. Havelund, K. Sen, Program monitoring with LTL in EAGLE; H. Barringer, A. Goldberg, K. Havelund, K. Sen, Program monitoring with LTL in EAGLE |
| [8] | H. Barringer, A. Goldberg, K. Havelund, K. Sen, Rule-based runtime verification, in: B. Steffen, G. Levi (Eds.), Proc. Fifth Internat. Conf. on Verification, Model Checking and Abstract Interpretation, Lecture Notes in Computer Science, Vol. 2937, Springer, Berlin, January 2004, pp. 44-57.; H. Barringer, A. Goldberg, K. Havelund, K. Sen, Rule-based runtime verification, in: B. Steffen, G. Levi (Eds.), Proc. Fifth Internat. Conf. on Verification, Model Checking and Abstract Interpretation, Lecture Notes in Computer Science, Vol. 2937, Springer, Berlin, January 2004, pp. 44-57. · Zbl 1202.68243 |
| [9] | S. Bensalem, M. Bozga, M. Krichen, S. Tripakis, Testing conformance of real-time software by automatic generation of observers, in: Proc. RV’04: Fourth Internat. Workshop on Runtime Verification, Electronic Notes in Theoretical Computer Science, vol. 113, Barcelona, Spain, Elsevier Science, Amsterdam, 2004.; S. Bensalem, M. Bozga, M. Krichen, S. Tripakis, Testing conformance of real-time software by automatic generation of observers, in: Proc. RV’04: Fourth Internat. Workshop on Runtime Verification, Electronic Notes in Theoretical Computer Science, vol. 113, Barcelona, Spain, Elsevier Science, Amsterdam, 2004. |
| [10] | S. Bensalem, K. Havelund, Deadlock analysis of multi-threaded Java programs, Kestrel Technology, NASA Ames Research Center, CA, October 2002.; S. Bensalem, K. Havelund, Deadlock analysis of multi-threaded Java programs, Kestrel Technology, NASA Ames Research Center, CA, October 2002. |
| [11] | C. Boyapati, S. Khurshid, D. Marinov, Korat: automated testing based on Java predicates, in: Proc. Internat. Symp. Software Testing and Analysis (ISSTA), July 2002, pp. 123-133.; C. Boyapati, S. Khurshid, D. Marinov, Korat: automated testing based on Java predicates, in: Proc. Internat. Symp. Software Testing and Analysis (ISSTA), July 2002, pp. 123-133. |
| [12] | G. Brat, D. Giannakopoulou, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, A. Venet, W. Visser, Experimental evaluation of verification and validation tools on Martian rover software, in: SEI Software Model Checking Workshop, 2003, extended version, J. Formal Methods System Design, 25 (2) (2004).; G. Brat, D. Giannakopoulou, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, A. Venet, W. Visser, Experimental evaluation of verification and validation tools on Martian rover software, in: SEI Software Model Checking Workshop, 2003, extended version, J. Formal Methods System Design, 25 (2) (2004). · Zbl 1078.68665 |
| [13] | F. Chen, G. Roşu, Towards monitoring-oriented programming: a paradigm combining specification and implementation, in: Proc. RV’03: the Third Internat. Workshop on Runtime Verification, Electronic Notes in Theoretical Computer Science, Boulder, USA, Vol. 89(2), Elsevier Science, Amsterdam, 2003.; F. Chen, G. Roşu, Towards monitoring-oriented programming: a paradigm combining specification and implementation, in: Proc. RV’03: the Third Internat. Workshop on Runtime Verification, Electronic Notes in Theoretical Computer Science, Boulder, USA, Vol. 89(2), Elsevier Science, Amsterdam, 2003. |
| [14] | K. Claessen, J. Hughes, Testing monadic code with QuickCheck, in: Proc. ACM SIGPLAN Workshop on Haskell, 2002, pp. 65-77.; K. Claessen, J. Hughes, Testing monadic code with QuickCheck, in: Proc. ACM SIGPLAN Workshop on Haskell, 2002, pp. 65-77. |
| [15] | Clarke, L. A., A system to generate test data and symbolically execute programs, IEEE Trans. Software Engrg., SE-2, 215-222 (1976) |
| [16] | D. Drusinsky, The temporal rover and the ATG rover, in: Proc. SPIN’00: SPIN Model Checking and Software Verification, Lecture Notes in Computer Science, Vol. 1885, Stanford, CA, USA, Springer, Berlin, 2000, pp. 323-330.; D. Drusinsky, The temporal rover and the ATG rover, in: Proc. SPIN’00: SPIN Model Checking and Software Verification, Lecture Notes in Computer Science, Vol. 1885, Stanford, CA, USA, Springer, Berlin, 2000, pp. 323-330. · Zbl 0976.68571 |
| [17] | D. Drusinsky, Monitoring temporal rules combined with time series, in: Proc. CAV’03: Computer Aided Verification, Lecture Notes in Computer Science, Vol. 2725, Boulder, USA, Springer, Berlin, 2003, pp. 114-118.; D. Drusinsky, Monitoring temporal rules combined with time series, in: Proc. CAV’03: Computer Aided Verification, Lecture Notes in Computer Science, Vol. 2725, Boulder, USA, Springer, Berlin, 2003, pp. 114-118. |
| [18] | B. Finkbeiner, S. Sankaranarayanan, H. Sipma, Collecting statistics over runtime executions, in: Proc. RV’02: The Second Internat. Workshop on Runtime Verification, Electronic Notes in Theoretical Computer Science, Vol. 70(4), Paris, France, Elsevier Science, Amsterdam, 2002.; B. Finkbeiner, S. Sankaranarayanan, H. Sipma, Collecting statistics over runtime executions, in: Proc. RV’02: The Second Internat. Workshop on Runtime Verification, Electronic Notes in Theoretical Computer Science, Vol. 70(4), Paris, France, Elsevier Science, Amsterdam, 2002. |
| [19] | Finkbeiner, B.; Sipma, H., Checking finite traces using alternating automata, Formal Methods System Design, 24, 2, 101-128 (2004) · Zbl 1073.68053 |
| [20] | First, Second, Third and Fourth Workshops on Runtime Verification (RV’01-RV’04), ENTCS, Vol. 55(2), 70(4), 89(2), 113, Elsevier Science, Amsterdam, 2001, 2002, 2003, 2004.; First, Second, Third and Fourth Workshops on Runtime Verification (RV’01-RV’04), ENTCS, Vol. 55(2), 70(4), 89(2), 113, Elsevier Science, Amsterdam, 2001, 2002, 2003, 2004. |
| [21] | Foundations of Software Engineering, Microsoft Research, The AsmL test generator tool. http://research.microsoft.com/fse/asml/doc/AsmLTester.html; Foundations of Software Engineering, Microsoft Research, The AsmL test generator tool. http://research.microsoft.com/fse/asml/doc/AsmLTester.html |
| [22] | A. Gargantini, C. Heitmeyer, Using model checking to generate tests from requirements specifications, in: Proc. Seventh European Engineering Conf. Held Jointly with the Seventh ACM SIGSOFT Internat. Symp. Foundations of Software Engineering, Springer, Berlin, 1999, pp. 146-162.; A. Gargantini, C. Heitmeyer, Using model checking to generate tests from requirements specifications, in: Proc. Seventh European Engineering Conf. Held Jointly with the Seventh ACM SIGSOFT Internat. Symp. Foundations of Software Engineering, Springer, Berlin, 1999, pp. 146-162. |
| [23] | D. Giannakopoulou, K. Havelund, Automata-based verification of temporal properties on running programs, in: Proc. ASE’01: Internat. Conf. on Automated Software Engineering, Institute of Electrical and Electronics Engineers, Coronado Island, CA, 2001, pp. 412-416.; D. Giannakopoulou, K. Havelund, Automata-based verification of temporal properties on running programs, in: Proc. ASE’01: Internat. Conf. on Automated Software Engineering, Institute of Electrical and Electronics Engineers, Coronado Island, CA, 2001, pp. 412-416. |
| [24] | A. Goldberg, K. Havelund, Instrumentation of Java bytecode for runtime analysis, in: Proc. Formal Techniques for Java-like Programs, Technical Reports from ETH Zurich, Vol. 408, Switzerland, ETH Zurich, 2003.; A. Goldberg, K. Havelund, Instrumentation of Java bytecode for runtime analysis, in: Proc. Formal Techniques for Java-like Programs, Technical Reports from ETH Zurich, Vol. 408, Switzerland, ETH Zurich, 2003. |
| [25] | A. Gotlieb, B. Botella, M. Rueher, Automatic test data generation using constraint solving techniques, in: Proc. Internat. Symp. Software Testing and Analysis (ISSTA), Clearwater Beach, FL, March 1998, pp. 53-62.; A. Gotlieb, B. Botella, M. Rueher, Automatic test data generation using constraint solving techniques, in: Proc. Internat. Symp. Software Testing and Analysis (ISSTA), Clearwater Beach, FL, March 1998, pp. 53-62. |
| [26] | W. Grieskamp, Y. Gurevich, W. Schulte, M. Veanes, Generating finite state machines from abstract state machines, in: Proc. Internat. Symp. Software Testing and Analysis (ISSTA), July 2002, pp. 112-122.; W. Grieskamp, Y. Gurevich, W. Schulte, M. Veanes, Generating finite state machines from abstract state machines, in: Proc. Internat. Symp. Software Testing and Analysis (ISSTA), July 2002, pp. 112-122. |
| [27] | A. Groce, W. Visser, Model checking Java programs using structural heuristics, in: Proc. 2002 Internat. Symp. Software Testing and Analysis ISSTA, ACM Press, New York, July 2002, pp. 12-21; A. Groce, W. Visser, Model checking Java programs using structural heuristics, in: Proc. 2002 Internat. Symp. Software Testing and Analysis ISSTA, ACM Press, New York, July 2002, pp. 12-21 · Zbl 1077.68684 |
| [28] | E. Gunter, D. Peled, Tracing the executions of concurrent programs, in: Proc. of RV’02: Second Internat. Workshop on Runtime Verification, Electronic Notes in Theoretical Computer Science, Vol. 70(4), Copenhagen, Denmark, Elsevier Science, Amsterdam, 2002.; E. Gunter, D. Peled, Tracing the executions of concurrent programs, in: Proc. of RV’02: Second Internat. Workshop on Runtime Verification, Electronic Notes in Theoretical Computer Science, Vol. 70(4), Copenhagen, Denmark, Elsevier Science, Amsterdam, 2002. |
| [29] | Gurevich, Y., Evolving algebras 1993lipari guide, (Specification and Validation Methods (1995), Oxford University Press: Oxford University Press Oxford), 9-36 · Zbl 0852.68053 |
| [30] | A. Hartman, Model based test generation tools,; A. Hartman, Model based test generation tools, |
| [31] | K. Havelund, G. Roşu, Monitoring programs using rewriting, in: Proc. of the Internat. Conf. Automated Software Engineering (ASE’01), IEEE CS Press, Coronado Island, CA, 2001, pp. 135-143, extended version to appear in J. Automat. Software Engrg.; K. Havelund, G. Roşu, Monitoring programs using rewriting, in: Proc. of the Internat. Conf. Automated Software Engineering (ASE’01), IEEE CS Press, Coronado Island, CA, 2001, pp. 135-143, extended version to appear in J. Automat. Software Engrg. |
| [32] | Havelund, K.; Roşu, G., An overview of the runtime verification tool Java PathExplorer, Formal Methods System Design, 24, 2, 189-215 (2004) · Zbl 1073.68549 |
| [33] | K. Havelund, G. Roşu, Synthesizing monitors for safety properties, in: Tools and Algorithms for Construction and Analysis of Systems (TACAS’02), Lecture Notes in Computer Science, Vol. 2280, Springer, Berlin, 2002, pp. 342-356, extended version in Internat. J. Software Tools Technol. Transfer 6 (2) (2004) 158-173.; K. Havelund, G. Roşu, Synthesizing monitors for safety properties, in: Tools and Algorithms for Construction and Analysis of Systems (TACAS’02), Lecture Notes in Computer Science, Vol. 2280, Springer, Berlin, 2002, pp. 342-356, extended version in Internat. J. Software Tools Technol. Transfer 6 (2) (2004) 158-173. |
| [34] | M.P.E. Heimdahl, S. Rayadurgam, W. Visser, D. George, J. Gao, Auto-generating test sequences using model checkers: a case study, in: Proc. Third Internat. Workshop on Formal Approaches to Testing of Software (FATES), Lecture Notes in Computer Science, Vol. 2931, Montreal, Canada, Springer, Berlin, October 2003, pp. 42-59.; M.P.E. Heimdahl, S. Rayadurgam, W. Visser, D. George, J. Gao, Auto-generating test sequences using model checkers: a case study, in: Proc. Third Internat. Workshop on Formal Approaches to Testing of Software (FATES), Lecture Notes in Computer Science, Vol. 2931, Montreal, Canada, Springer, Berlin, October 2003, pp. 42-59. |
| [35] | H.S. Hong, I. Lee, O. Sokolsky, H. Ural, A temporal logic based theory of test coverage and generation, in: Proc. Eighth Internat. Conf. on Tools and Algorithms for Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, Vol. 2280, Grenoble, France, Springer, Berlin, April 2002, pp. 327-341.; H.S. Hong, I. Lee, O. Sokolsky, H. Ural, A temporal logic based theory of test coverage and generation, in: Proc. Eighth Internat. Conf. on Tools and Algorithms for Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, Vol. 2280, Grenoble, France, Springer, Berlin, April 2002, pp. 327-341. · Zbl 1043.68573 |
| [36] | Huang, J. C., An approach to program testing, ACM Comput. Surv., 7, 3 (1975) · Zbl 0321.68011 |
| [37] | S. Khurshid, C. Pasareanu, W. Visser, Generalized symbolic execution for model checking and testing, in: Proc. TACAS’03: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Vol. 2619, Warsaw, Poland, April 2003.; S. Khurshid, C. Pasareanu, W. Visser, Generalized symbolic execution for model checking and testing, in: Proc. TACAS’03: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Vol. 2619, Warsaw, Poland, April 2003. · Zbl 1031.68519 |
| [38] | Kim, M.; Viswanathan, M.; Kannan, S.; Lee, I.; Sokolsky, O., Java-MaCa run-time assurance tool for Java, Formal Methods System Design, 24, 2, 129-156 (2004) · Zbl 1073.68552 |
| [39] | King, J. C., Symbolic execution and program testing, Comm. ACM, 19, 7, 385-394 (1976) · Zbl 0329.68018 |
| [40] | Korel, B., Automated software test data generation, IEEE Trans. Software Engrg., 16, 8, 870-879 (1990) |
| [41] | B. Korel, Automated test data generation for programs with procedures, in: Proc. Internat. Symp. Software Testing and Analysis (ISSTA), San Diego, CA, 1996, pp. 209-215.; B. Korel, Automated test data generation for programs with procedures, in: Proc. Internat. Symp. Software Testing and Analysis (ISSTA), San Diego, CA, 1996, pp. 209-215. |
| [42] | Kortenkamp, D.; Simmons, R.; Milam, T.; Fernandez, J., A suite of tools for debugging distributed autonomous systems, Formal Methods System Design, 24, 2, 157-188 (2004) · Zbl 1073.68525 |
| [43] | K. Jelling Kristoffersen, C. Pedersen, H.R. Andersen, Runtime verification of timed LTL using disjunctive normalized equation systems, in: Proc. RV’03: Third Internat. Workshop on Runtime Verification, Electronic Notes in Theoretical Computer Science, Vol. 89(2), Boulder, USA, Elsevier Science, Amsterdam, 2003.; K. Jelling Kristoffersen, C. Pedersen, H.R. Andersen, Runtime verification of timed LTL using disjunctive normalized equation systems, in: Proc. RV’03: Third Internat. Workshop on Runtime Verification, Electronic Notes in Theoretical Computer Science, Vol. 89(2), Boulder, USA, Elsevier Science, Amsterdam, 2003. |
| [44] | D. Marinov, Testing using a solver for imperative constraints, Ph.D. Thesis, Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology, 2004, to appear.; D. Marinov, Testing using a solver for imperative constraints, Ph.D. Thesis, Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology, 2004, to appear. |
| [45] | Marinov, D.; Khurshid, S., TestEraa novel framework for automated testing of Java programs, (Proc. 16th IEEE Internat. Conf. Automated Software Engineering ASE (November 2001), San Diego: San Diego CA), 22-34 |
| [46] | N. Markey, P. Schnoebelen, Model checking a path (preliminary report), in: Proc. CONCUR’03: Internat. Conf. Concurrency Theory, Lecture Notes in Computer Science, Vol. 2761, Marseille, France, Springer, Berlin, August 2003, pp. 251-265.; N. Markey, P. Schnoebelen, Model checking a path (preliminary report), in: Proc. CONCUR’03: Internat. Conf. Concurrency Theory, Lecture Notes in Computer Science, Vol. 2761, Marseille, France, Springer, Berlin, August 2003, pp. 251-265. · Zbl 1274.68197 |
| [47] | Maurer, P. M., Generating test data with enhanced context-free grammars, IEEE Software, 7, 4, 50-55 (1990) |
| [48] | B. Nichols, D. Buttlar, J.P. Farrell, Pthreads Programming, O’Reilly, 1998.; B. Nichols, D. Buttlar, J.P. Farrell, Pthreads Programming, O’Reilly, 1998. |
| [49] | T. O’Malley, D. Richardson, L. Dillon, Efficient specification-based oracles for critical systems, in: Proc. California Software Symp., 1996.; T. O’Malley, D. Richardson, L. Dillon, Efficient specification-based oracles for critical systems, in: Proc. California Software Symp., 1996. |
| [50] | Parasoft, http://www.parasoft.com; Parasoft, http://www.parasoft.com |
| [51] | A. Pnueli, The temporal logic of programs, in: Proc. 18th IEEE Symp. Foundations of Computer Science, 1977, pp. 46-77.; A. Pnueli, The temporal logic of programs, in: Proc. 18th IEEE Symp. Foundations of Computer Science, 1977, pp. 46-77. |
| [52] | Pugh, W., A practical algorithm for exact array dependence analysis, Comm. ACM, 35, 8, 102-114 (1992) |
| [53] | Purify: Fast Detection of Memory Leaks and Access Errors, January 1992.; Purify: Fast Detection of Memory Leaks and Access Errors, January 1992. |
| [54] | Ramamoorthy, C. V.; Ho, Siu-Bun F.; Chen, W. T., On the automated generation of program test data, IEEE Trans. Software Engrg., 2, 4, 293-300 (1976) |
| [55] | Richardson, D. J.; Aha, S. L.; O’Malley, T. O., Specification-based test oracles for reactive systems, (Proc. ICSE’92: Internat. Conf. Software Engineering (1992), Melbourne: Melbourne Australia), 105-118 |
| [56] | Savage, S.; Burrows, M.; Nelson, G.; Sobalvarro, P.; Anderson, T., Erasera dynamic data race detector for multithreaded programs, ACM Trans. Comput. Systems, 15, 4, 391-411 (1997) |
| [57] | A. Sen, V.K. Garg, Partial order trace analyzer (POTA) for distributed programs, in: Proc. RV’03: the Third Internat. Workshop on Runtime Verification, Electronic Notes in Theoretical Computer Science, Vol. 89(2), Boulder, USA, Elsevier Science, Amsterdam, 2003.; A. Sen, V.K. Garg, Partial order trace analyzer (POTA) for distributed programs, in: Proc. RV’03: the Third Internat. Workshop on Runtime Verification, Electronic Notes in Theoretical Computer Science, Vol. 89(2), Boulder, USA, Elsevier Science, Amsterdam, 2003. |
| [58] | K. Sen, G. Roşu, Generating optimal monitors for extended regular expressions, in: Proc. RV’03: Third Internat. Workshop on Runtime Verification, Electronic Notes in Theoretical Computer Science, Vol. 89(2), Boulder, USA, Elsevier Science, Amsterdam, 2003.; K. Sen, G. Roşu, Generating optimal monitors for extended regular expressions, in: Proc. RV’03: Third Internat. Workshop on Runtime Verification, Electronic Notes in Theoretical Computer Science, Vol. 89(2), Boulder, USA, Elsevier Science, Amsterdam, 2003. |
| [59] | K. Sen, G. Roşu, G. Agha, Generating optimal linear temporal logic monitors by coinduction, in: V.A. Saraswat (Ed.), Proc. Eighth Asian Computing Science Conf. (ASIAN’03), Lecture Notes in Computer Science, Vol. 2896, December 2003, pp. 260-275.; K. Sen, G. Roşu, G. Agha, Generating optimal linear temporal logic monitors by coinduction, in: V.A. Saraswat (Ed.), Proc. Eighth Asian Computing Science Conf. (ASIAN’03), Lecture Notes in Computer Science, Vol. 2896, December 2003, pp. 260-275. · Zbl 1215.68134 |
| [60] | K. Sen, G. Roşu, G. Agha, Runtime safety analysis of multithreaded programs, in: Proc. ESEC/FSE’03: European Software Engineering Conf. and ACM SIGSOFT Internat. Symp. on the Foundations of Software Engineering, ACM, Helsinki, Finland, September 2003, pp. 337-346.; K. Sen, G. Roşu, G. Agha, Runtime safety analysis of multithreaded programs, in: Proc. ESEC/FSE’03: European Software Engineering Conf. and ACM SIGSOFT Internat. Symp. on the Foundations of Software Engineering, ACM, Helsinki, Finland, September 2003, pp. 337-346. |
| [61] | E.G. Sirer, B.N. Bershad, Using production grammars in software testing, in: Proc. Second Conf. on Domain-specific languages, 1999, pp. 1-13.; E.G. Sirer, B.N. Bershad, Using production grammars in software testing, in: Proc. Second Conf. on Domain-specific languages, 1999, pp. 1-13. |
| [62] | K. Stobie, Advanced modeling, model based test generation, and abstract state machine language AsmL, http://www.sasqag.org/pastmeetings/asml.ppt; K. Stobie, Advanced modeling, model based test generation, and abstract state machine language AsmL, http://www.sasqag.org/pastmeetings/asml.ppt |
| [63] | P. Thati, G. Roşu, Monitoring algorithms for metric temporal logic, in: Proc. RV’04: Fourth Internat. Workshop on Runtime Verification, Electronic Notes in Theoretical Computer Science, vol. 113, Barcelona, Spain, Elsevier Science, Amsterdam, 2004.; P. Thati, G. Roşu, Monitoring algorithms for metric temporal logic, in: Proc. RV’04: Fourth Internat. Workshop on Runtime Verification, Electronic Notes in Theoretical Computer Science, vol. 113, Barcelona, Spain, Elsevier Science, Amsterdam, 2004. |
| [64] | The test sequence generator TGV, http://www-verimag.imag.fr/\( \sim;\); The test sequence generator TGV, http://www-verimag.imag.fr/\( \sim;\) |
| [65] | N. Tracey, J. Clark, K. Mander, The way forward for unifying dynamic test-case generation: the optimisation-based approach, in: Internat. Workshop on Dependable Computing and Its Applications (DCIA), IFIP, January 1998, pp. 169-180.; N. Tracey, J. Clark, K. Mander, The way forward for unifying dynamic test-case generation: the optimisation-based approach, in: Internat. Workshop on Dependable Computing and Its Applications (DCIA), IFIP, January 1998, pp. 169-180. |
| [66] | T-VEC,; T-VEC, |
| [67] | Visser, W.; Havelund, K.; Brat, G.; Park, S.-J.; Lerda, F., Model checking programs, Automat. Software Engrg. J., 10, 2, 203-232 (2003) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
