Использование средств статической отладки для верификации программной среды ScopeShell

Авторы

  • С.В. Степанов
  • А.Г. Шишкин

Ключевые слова:

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

Аннотация

Рассматриваются свободно распространяемые пакеты для статической верификации кодов, написанных на языке Java. Приведены результаты тестирования и оценка эффективности применения различных верификаторов на примере программной системы ScopeShell, разработанной на кафедре автоматизации научных исследований факультета ВМиК МГУ.

Новые вычислительные технологии

Загрузки

Опубликован

2009-01-14

Выпуск

Том 10 (2009): Выпуск 1.

Раздел

Раздел 2. Программирование

Авторы

С.В. Степанов

Московский государственный университет имени М.В. Ломоносова,
факультет вычислительной математики и кибернетики
Ленинские горы, 119992, Москва
• студент

А.Г. Шишкин

Московский государственный университет имени М.В. Ломоносова,
факультет вычислительной математики и кибернетики
Ленинские горы, 119992, Москва
• старший научный сотрудник

Библиографические ссылки

  1. Gnuplot (http://www.gnuplot.info/).
  2. Hovemeyer D., Pugh W. Finding bugs is easy // ACM Sigplan Notices. 2004. 39. 92-106.
  3. FindBugs (http://findbugs.sourceforge.net).
  4. BCEL (http://jakarta.apache.org/bcel).
  5. PMD/Java (http://pmd.sourceforge.net).
  6. Lint4j (http://www.jutils.com).
  7. JLint (http://artho.com/jlint).
  8. Artho C. Finding faults in multi-threaded programs. Master’s Th. Institute of Computer Systems, Federal Institute of Technology. Zürich/Austin, 2001.
  9. Flanagan C., Leino K.R. M., Lillibridge N.M. G., Saxe J.B., Stata R. Extended static checking for Java // Proc. of the 2002 ACM SIGPLAN Conf. on Programming Language Design and Implementation. Berlin, 2002. 234-245.
  10. Burdy L., Cheon Y., Cok D., Ernst M., Kiniry J., Leavens G.T., Leino K.R. M., Poll E. An overview of JML tools and applications // Int. J. on Software Tools for Technology Transfer. 2005. 7, N 3. 212-232.
  11. Leavens G.T., Leino K.R. M., Poll E., Ruby C., Jacobs B. JML: Notations and tools supporting detailed design in Java // OOPSLA’00 Companion. Minneapolis, 2000. 105-106.
  12. Hammurapi (http://www.hammurapi.biz).
  13. QJ-Pro (http://qjpro.sourceforge.net).
  14. Clarkware Consulting (http://www.clarkware.com).
  15. Condenser (http://condenser.sourceforge.net).
  16. Dependency Finder (http://depfind.sourceforge.net).
  17. UCDetector (http://www.ucdetector.org).
  18. Jackson D. Micromodels of software: modelling and analysis with Alloy (http://sdg.lcs.mit.edu/alloy/book.pdf).
  19. Alloy (http://alloy.mit.edu).
  20. Jackson D., Schechter I., Shlyakhter I. ALCOA: The Alloy constraint analyzer // Proc. of the 22nd Int. Conf. on Software Engineering. Limerick, 2000. 730-733.