Ïåðñïåêòèâû èíòåãðàöèè ìåòîäîâ âåðèôèêàöèè ïðîãðàììíîãî îáåñïå÷åíèÿ
       

Ëèòåðàòóðà


  • V. Maraia. The Build Master: Microsoft's Software Configuration Management Best Practices. Addison-Wesley Professional, 2005.
  • G. Robles. Debian Counting. .
  • C. Ìàêêîííåëë. Ñîâåðøåííûé êîä. Ì.: Ðóññêàÿ ðåäàêöèÿ, 2005.
  • Â. Â. Êóëÿìèí. Ìåòîäû âåðèôèêàöèè ïðîãðàììíîãî îáåñïå÷åíèÿ. Âñåðîññèéñêèé êîíêóðñ îáçîðíî-àíàëèòè÷åñêèõ ñòàòåé ïî ïðèîðèòåòíîìó íàïðàâëåíèþ "Èíôîðìàöèîííî-òåëåêîììóíèêàöèîííûå ñèñòåìû", 2008.
    .
  • D. L. Detlefs, K. R. M. Leino, G. Nelson, J. B. Saxe. Extended static checking. Technical Report SRC-RR-159, Digital Equipment Corporation, Systems Research Center, 1998.
  • D. R. Cok, J. R. Kiniry. ESC/Java2: Uniting ESC/Java and JML. Proc. of International Workshop on the Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS'04), LNCS 3362:108-128, Springer-Verlag, January 2005.
  • P. Emanuelsson, U. Nilsson. A Comparative Study of Industrial Static Analysis Tools. Technical Report 2008:3, Linkoping University, 2008.
    .
  • T. A. Henzinger, R. Jhala, R. Majumdar, G. Sutre. Software Verification with Blast. Proc. of 10-th SPIN Workshop on Model Checking Software (SPIN 2003), LNCS 2648:235-239, Springer-Verlag, 2003.
  • T. Ball, S. K. Rajamani. Automatically Validating Temporal Safety Properties of Interfaces. Proc. of Model Checking of Software, LNCS 2057:103-122, Springer, 2001.
  • B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Mine, D. Monniaux, X. Rival. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. T. Mogensen, D. A. Schmidt, I. H. Sudborough, eds. The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones. LNCS 2566:85-108, Springer-Verlag 2002.
  • Y. Smaragdakis, C. Csallner. Combining Static and Dynamic Reasoning for Bug Detection. Proc. of TAP 2007, LNCS 4454:1-16, Springer, 2007.
  • K. Sen, G. Agha. CUTE and jCUTE: Concolic unit testing and explicit path model-checking tools. Proc. of Computer Aided Verification, pp.419-423, August 2006.
  • T. Xie, D. Marinov, W. Schulte, D. Notkin.
    Symstra: A Framework for Generating Object- Oriented Unit Tests using Symbolic Execution. Proc. of 11-th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), Edinburgh, UK, pp. 365-381, April 2005.
  • N. Tillmann, W. Schulte. Parameterized Unit Tests with Unit Meister. ACM SIGSOFT Software Engineering Notes, 30(5):241-244, September 2005.
  • C. Pacheco, S. K. Lahiri, M. D. Ernst, T. Ball. Feedback-Directed Random Test Generation. Proc. of International Conference on Software Engineering, pp. 75-84, 2007.
  • P. Godefroid. Compositional dynamic test generation. Proc. of 34-th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (PLOP 2007), pp. 47-54, 2007.
  • M. Broy, B. Jonsson, J.-P. Katoen, M. Leucker, A. Pretschner, eds. Model Based Testing of Reactive Systems. LNCS 3472, Springer, 2005.
  • M. Utting, B. Legeard. Practical Model-Based Testing: A Tools Approach. Morgan-Kaufmann, 2007.
  • J. Jacky, M. Veanes, C. Campbell, W. Schulte. Model-Based Software Testing and Analysis with C#. Cambridge University Press, 2007.
  • B. Korel. Automated Test Data Generation. IEEE Trans. on Software Engineering, 16(8):870-879, 1990.
  • R. DeMillo, A. Offutt. Constraint-based automatic test data generation. IEEE Trans. on Software Engineering, 17(9):900-910, 1991.
  • A. Gotlieb, B. Botella, M. Rueher. Automatic test data generation using constraint solving techniques. ACM SIGSOFT Software Engineering Notes, 23(2):53-62, 1998.
  • A. Gargantini, C. Heitmeyer. Using Model Checking to Generate Tests from Requirements Specifications. Proc. of Joint 7-th European Software Engineering Conference and 7-th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/FSE99), ACM Press, September 1999, pp. 146-162.
  • H. S. Hong, I. Lee, O. Sokolsky, S. D. Cha. Automatic Test Generation from Statecharts Using Model Checking. Technical Report MS-CIS-01-07, Feb 2001.
  • G. Hamon, L. de Moura, J. Rushby. Generating Efficient Test Sets with a Model Checker.


    Proc. of the 2- nd Software Engineering and Formal Methods International Conference, p. 261-270, 2004.
  • D. Beyer, A. J. Chlipala, T. A. Henzinger, R. Jhala, R. Majumdar. Generating tests from counterexamples. Proc. of 26-th International Conference on Software Engineering (ICSE), p. 326-335, 2004.
  • I. Lee, S. Kannan, M. Kim, O. Sokolsky, M. Viswanathan. Runtime Assurance Based On Formal Specifications. Proc. of International Conference on Parallel and Distributed Processing Techniques and Applications PDPTA’1999, pp. 279-287, 1999.
  • Y. Cheon, G. T. Leavens. A runtime assertion checker for the Java Modeling Language (JML). Proc. of International Conference on Software Engineering Research and Practice (SERP’02), pp. 322-328, CSREA Press, June 2002.
  • A. Cavalli, C. Gervy, S. Prokopenko. New approaches for passive testing using an Extended Finite State Machine Specification. Information and Software Technology, 45(12):837-852, Elsevier, September 2003.
  • D. Drusinsky. Modeling and Verification Using UML Statecharts. Newnes, 2006.
  • M. R. Blackburn, R. D. Busser, A. M. Nauman. Interface-Driven, Model-Based Test Automation. CrossTalk, The Journal of Defense Software Engineering, May 2003.
  • C. Artho, H. Barringer, A. Goldberg, K. Havelund, S. Khurshid, M. Lowry, C. Pasareanu, G. Rosu, K. Sen, W. Visser, R. Washington. Combining test case generation and runtime verification. Theoretical Computer Science, 336(2-3):209-234, May 2005.
  • G. Brat, K. Havelund, S. Park, W. Visser. Model Checking Programs. Proc. of 15-th IEEE International Conference on Automated Software Engineering, Grenoble, France, pp. 3-11, September 2000.
  • G. J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 2003.
  • .
  • M. Blackburn, R. D. Busser, J. S. Fontaine. Automatic generation of test vectors for SCR-style specifications. Proc. of 12-th Annual Conference on Computer Assurance, June 1997, pp. 54-67.
  • .
  • G. Brat, W. Visser, K. Havelund, S. Park. Java PathFinder — second generation of a Java model checker.


    Proc. of Workshop on Advances in Verification, Chicago, Illinois, July 2000.
  • .
  • .
  • T. Ball, S. K. Rajamani. Automatically Validating Temporal Safety Properties of Interfaces. Proc. of Model Checking of Software, LNCS 2057:103-122, Springer, 2001.
  • T. Ball, E. Bounimova, B. Cook, V. Levin, J. Lichtenberg, C. McGarvey, B. Ondrusek, S. K. Rajamani, A. Ustuner. Thorough Static Analysis of Device Drivers. ACM SIGOPS Operating Systems Review 40(4):73-85, 2006.
  • W. Grieskamp, N. Kicillof, D. MacDonald, A. Nandan, K. Stobie, F. L. Wurden. Model-Based Quality Assurance of Windows Protocol Documentation. Proc. of 1-st International Conference on Software Testing, Verification, and Validation, ICST 2008, Lillehammer, Norway, April 2008, pp. 502-506.
  • M. Veanes, C. Campbell, W. Grieskamp, W. Schulte, N. Tillmann, L. Nachmanson. Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer. Formal Methods and Testing, LNCS 4949:39-76, Springer Verlag, 2008.
  • V. Kuliamin, A. Petrenko, N. Pakoulin. Practical Approach to Specification and Conformance Testing of Distributed Network Applications. In M. Malek, E. Nett, N. Suri, eds. Service Availability. LNCS 3694, pp. 68-83, Springer-Verlag, 2005.
  • A. Grinevich, A. Khoroshilov, V. Kuliamin, D. Markovtsev, A. Petrenko, V. Rubanov. Formal Methods in Industrial Software Standards Enforcement. Proc. of PSI’2006, Novosibirsk, Russia, June 2006, LNCS 4378:459-469, Springer-Verlag, 2006.
  • Ñ. Â. Çåëåíîâ, Ñ. À. Çåëåíîâà, À. Ñ. Êîñà÷åâ, À. Ê. Ïåòðåíêî. Ãåíåðàöèÿ òåñòîâ äëÿ êîìïèëÿòîðîâ è äðóãèõ òåêñòîâûõ ïðîöåññîðîâ. Ïðîãðàììèðîâàíèå, 29(2):59–69, 2003.
  • Â. Â. Êóëÿìèí, À. Ê. Ïåòðåíêî, À. Ñ. Êîñà÷åâ, È. Á. Áóðäîíîâ. Ïîäõîä UniTesK ê ðàçðàáîòêå òåñòîâ. Ïðîãðàììèðîâàíèå, 29(6):25-43, 2003.
  • J. Souyris, D. Delmas. Experimental Assessment of ASTREE on Safety-Critical Avionics Software. Proc. of Int. Conf. on Computer Safety, Reliability, and Security, SAFECOMP 2007, F. Saglietti, N. Oster, eds., Nuremberg, Germany, September 2007, LNCS 4680:479-490, Springer, 2007.
  • P. Manolios, G. Subramanian, D. Vroon.


    Automating component- based system assembly. Proc. of ISSTA 2007, London, UK, 2007, pp. 61-72.
  • E. Poll, J. van den Berg, B. Jacobs. Specification of the JavaCard API in JML. In Proc. of CARDIS’00. Kluwer Academic Publishers, 2000.
  • F. Bouquet, B. Legeard. Reification of executable test scripts in formal specification-based test generation: The Java card transaction mechanism case study. In Proc. of the International Symposium of Formal Methods Europe, pp. 778-795, Springer-Verlag, 2003.
  • A. R. Bradley, H. B. Sipma, S. Solter, Z. Manna. Integrating tools for practical software analysis. Proc. of 2004 CUE Workshop, Vienna, Austria, October 2004.
  • T. Gilb, D. Graham. Software Inspection. Addison-Wesley, 1993.
  • A. Porter, H. Siy, L. Votta. A Review of Software Inspections. University of Maryland at College Park, Technical Report CS-TR-3552, 1995.
  • O. Laitenberger. A Survey of Software Inspection Technologies. In Handbook on Software Engineering and Knowledge Engineering, v. 2, pp. 517-555. World Scientific Publishing, 2002.
  • GNU Compiler Collection Internals. .
  • B. Daum. Professional Eclipse 3 for Java Developers. Wrox, 2004.
  • .
  • G. Yorsh, T. Ball, M. Sagiv. Testing, abstraction, theorem proving: better together! Proc. of ISSTA 2006, Partland, Maine, USA, 2006, pp. 145-156.
  • C. Beust, H. Suleiman. Next Generation Java Testing: TestNG and Advanced Concepts. Addison-Wesley Professional, 2007.
  • .


    Ñîäåðæàíèå ðàçäåëà