Перспективы интеграции методов верификации программного обеспечения

2009 г.

Перспективы интеграции методов верификации программного обеспечения

В. В. Кулямин
Труды Института системного программирования РАН

Назад Содержание

Литература

V. Maraia. The Build Master: Microsoft's Software Configuration Management Best Practices. Addison-Wesley Professional, 2005.
G. Robles. Debian Counting. http://libresoft.dat.escet.urjc.es/debian-counting/.
C. Макконнелл. Совершенный код. М.: Русская редакция, 2005.
В. В. Кулямин. Методы верификации программного обеспечения. Всероссийский конкурс обзорно-аналитических статей по приоритетному направлению "Информационно-телекоммуникационные системы", 2008.
http://window.edu.ru/window/library?p_rid=56168.
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.
http://www.ep.liu.se/ea/trcis/2008/003/trcis08003.pdf.
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.
http://spinroot.com/.
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.
http://www.t-vec.com/.
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.
http://javapathfinder.sourceforge.net/.
http://www.microsoft.com/whdc/devtools/tools/SDV.mspx.
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 ASTRÉE 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. http://gcc.gnu.org/onlinedocs/gccint/index.html.
B. Daum. Professional Eclipse 3 for Java Developers. Wrox, 2004.
http://www.eclipse.org/.
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.
http://testng.org/doc/.

Назад Содержание