Источники

1. Кларк Э. М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. М.: МЦНМО, 2002. 416 с.

2. Синицын С. В., Налютин Н. Ю. Верификация программного обеспечения.

3. Pnueli A. The temporal logic of programs / 18^th IEEE Symposium on Foundations of Computer Science. 1977. Pp. 46-57. http://www.inf.ethz.ch/personal/kroening/classes/fv/f2007/readings/focs77.pdf

4. Карпов Ю. Г.Model Checking: верификация параллельных и распределенных программных систем. СПб.: БХВ-Петербург, 2010. 560 с.

5. Вельдер С.Э., Лукин М.А., Шалыто А.А., Яминов Б.Р. Верификация

автоматных программ. СПб.: Наука, 2011. 244 с.

(http://is.ifmo.ru/verification/velder_verification_posobie_nauka.pdf).

6. Mikk E., Lakhnech Y., Siegel M. , Holzmann G. J. Implementing Statecharts in Promela/SPIN. Proceedings of WIFT'98, 1998.

7. Latella D., Majzik I., Massink M. Automatic verification of a behavioral subset UML statechart diagrams using the SPIN model-checker // Formal Aspects of Computing 11, 1999. Pp. 637-664.

http: //home. mit.bme. hu/~maj zik/publicat/fac99.pdf

8. Lilius, J., Paltor I. P. Formalising UML State Machines for Model Checking, in: R. B. France and B. Rumpe, editors / Proceedings of 2nd International Conference UML. 1999. LNCS: Volume 1723. Pp. 430-445.

9. Eschbah R. A verification approach for distributed abstract state machines. // PSI '02, 2001. Pp. 109-115. http://dl.acm.org/citation.cfm?id=705973

10. Shaffer T., Knapp A., Merz S. Model checking UML state machines and collaborations // Electronic notes in theoretical computer science 47, 2001. Pp. 1-13.

11. Tiwari A. Formal semantics and analysis methods for Simulink Stateflow models. Technical report. SRI International. 2002. http: //www.csl .sri.com/~tiwari/~stateflow.html

12. Pingree P. J., Mikk E., Holzmann G. J., Smith M.

13. Roux C., Encrenaz E. CTL May Be Ambiguous when Model Checking

Moore Machines. UPMC LIP6 ASIM, CHARME. 2003.

http://sed.free.fr/cr/charme2003.ps

14. Gnesi S., Mazzanti F. On the fly model checking of communicating UML state machines. 2004. http://fmt.isti.cnr.it/WEBPAPER/onthefly- SERA04.pdf

15. Gnesi S., Mazzanti F. A model checking verification environment for UML statecharts / Proceedings of XLIII Congresso Annuale AICA, 2005. http: //fmt.isti .cnr. it/~gnesi/matdid/aica.pdf

16. Виноградов Р. А., Кузьмин Е. В., Соколов В. А. Верификация автоматных программ средствами CPN/Tools // Моделирование и анализ информационных систем. 2006. № 2, с. 4-15.

http ://is. ifmo .ru/verification/_cpnverif. pdf

17. Кузьмин Е. В., Соколов В. А. О верификации «автоматных программ». Актуальные проблемы математики и информатики. / Сборник статей к 20-летию факультета ИВТ ЯрГУ им. П. Г. Демидова, Ярославль: ЯрГУ, 2006. С. 27 - 32.

18. Кузьмин Е. В., Соколов В. А. О некоторых подходах к верификации автоматных программ. / Сборник докладов семинара Go4IT - шаг к новым технологиям Интернета. Москва, Институт системного программирования, 2007. С. 43 - 48.

19. Васильева К. А., Кузьмин Е. В. Верификация автоматных программ с

использованием LTL // Моделирование и анализ информационных систем. 2007. № 1, с. 3-14.

http ://is. ifmo .ru/verification/_LTL_for_Spin.pdf

20. Лукин М. А. Верификация автоматный программ. Бакалаврская работа. СПбГУ ИТМО, 2007. 32 с. http://is.ifmo.ru/papers/_lukin_bachelor.pdf

21. Яминов Б. Р. Автоматизация верификации автоматных UniMod-

моделей на основе инструментального средства Bogor. Бакалаврская работа. СПбГУ ИТМО, 2007. 46 с.

http ://is. ifmo. ru/papers/_j aminov_bachelor. pdf

22. Ma G. Model checking support for CoreASM: model checking distributed

abstract state machines using Spin.

http: //summit.sfu.ca/item/8056

23. David A., Moller O., Yi W. Formal Verification of UML Statecharts with Real-time Extensions. Formal Methods. 2006. Vol. 3. Pp. 15-22.

24. Кубасов С.В., Соколов В.А. Синхронная модель автоматной программы // Моделирование и анализ информационных систем. 2007. № 1, с. 11-18

25. Егоров К. В., Шалыто А. А. Методика верификации автоматных

программ // Информационно-управляющие системы. 2008. № 5,

с. 15-21. http://is.ifmo.ru/works/_egorov.pdf

26. Кузьмин Е. В., Соколов В. А. Моделирование, спецификация и верификация автоматных программ // Программирование. 2008. № 1.

27. Курбацкий Е. А. Верификация программ, построенных на основе автоматного подхода с использованием программного средства SMV // Научно-технический вестник СПбГУ ИТМО. Вып. 53. Автоматное программирование. 2008, с. 137-144.

http: //books. ifmo .ru/ntv/ntv/5 3/ntv_5 3 .pdf

28. Лукин М. А., Шалыто А. А. Верификация автоматных программ с использованием верификатора Spin // Научно-технический вестник СПбГУ ИТМО. Вып. 53. Автоматное программирование. 2008, с. 145-162. http://books.ifmo.ru/ntv/ntv/53/ntv_53.pdf

29. Гуров В. С., Яминов Б. Р. Верификация автоматных программ при помощи верификатора UNIMOD.VERIFIER // Научно-технический вестник СПбГУ ИТМО. Вып. 53. Автоматное программирование. 2008, с. 162-176. http://books.ifmo.ru/ntv/ntv/53/ntv_53.pdf

30. Егоров К. В., Шалыто А. А. Разработка верификатора автоматных программ // Научно-технический вестник СПбГУ ИТМО. Вып. 53. Автоматное программирование. 2008, с. 177-188. http://books.ifmo.ru/ntv/ntv/53/ntv_53.pdf

31. Prashanth C.M., Shet K. C. Efficient Algorithms for Verification of UML Statechart Models. // Journal of Software. 2009. Issue 3. Pp 175-182.

32. Лукин М. А. Верификация визуальных автоматных программ с использованием инструментального средства Spin. СПбГУ ИТМО, 2009. 50 с. http://is.ifmo.ru/papers/_lukin_master.pdf

33. Вельдер С. Э., Шалыто А. А. Верификация автоматных моделей методом редуцированного графа переходов // Научно-технический вестник СПбГУ ИТМО.

34. Ремизов А. О., Шалыто А. А. Верификация автоматных программ / Сборник докладов научно-технической конференции «Состояние, проблемы и перспективы создания корабельных информационно- управляющих комплексов. ОАО «Концерн Моринформсистема Агат». М.: 2010, с. 90-98. http://is.ifmo.ru/works/_2010_05_25_verific.pdf

35. Клебанов А. А., Степанов О. Г., Шалыто А. А. Применение шаблонов требований к формальной спецификации и верификации автоматных программ / Труды семинара «Семантика, спецификация и верификация программ: теория и приложения». Казань, 2010, с. 124-130. http://is.ifmo.ru/works/_2010-10-01_klebanov.pdf

36. Вельдер С. Э., Шалыто А. А. Верификация автоматных моделей методом редуцированного графа переходов // Научно-технический вестник СПбГУ ИТМО. 2009. Вып. 6(64), c. 66-77. http://is.ifmo.ru/works/_2010_01_29_velder.pdf

37. Шошмина И. В., Карпов Ю. Г. Технология проектирования и верификации распределенных бортовых систем / Материалы международного семинара PSSV. Казань. 2010.

38. Вяткин В. В., Дубинин В. Н. Верификация приложений IEC 61499 на основе метода Model checking. // Известия высших учебных заведений. Поволжский район. Технические науки. 2011. Вып. 3 (19), с. 44 - 55. http://cyberleninka.ru/article/n/verifikatsiya-prilozheniy-iec-61499-na- osnove-metoda-model-checking

39. Miyazawa A., Cavalcanti A. Refinement-based verification of sequential implementations of Stateflow charts // Formal aspects of computing. 2011. Issuie 6.

40. Chen C., Sun J., Liu Y., Dong J., Zheng M. Formal modeling and validation of Stateflow diagrams // International Journal on Software Tools for Technology Transfer. 2012. Issue 6. Pp. 653 - 671.

41. D. Harel. Statecharts: A visual formalism for complex systems // Sci. Comput. Program., 1987. Issue 8. 231-274.

42. Шалыто А. А. Switch-технология. Алгоритмизация и

программирование задач логического управления. СПб.: Наука, 1998.

43. Cardei I., Jha R., Cardei M. Hierarchical architecture for real-time adaptive resource management. Secaucus, NJ, USA: Springer-Verlag, 2000.

44. Кузьмин Е. В. Иерархическая модель автоматных программ. // Моделирование и анализ информационных систем. Ярославль: ЯрГУ. Т. 13, №1 (2006) с. 26 - 34.

45. Поликарпова Н. И., Шалыто А. А. Автоматное программирование. СПб.: Питер, 2010. 168 с. http://is.ifmo.ru/books/_book.pdf

46. Вельдер С.Э., Лукин М.А., Шалыто А.А., Яминов Б.Р. Верификация автоматных программ. Учебное пособие. СПб.: НИУ ИТМО, 2011. 242 с. http://is.ifmo.ru/verification/velder_verification_posobie.pdf

47. Lukin M., Velder S., Shalyto A., Yaminov B. Verification of automata-based programs. Монография на английском (рукопись). СПб.: НИУ ИТМО, 2013. 104 с. http://is.ifmo.ru/verification/3_3_37_54_UP_Software_verification.pdf

48. Хопкрофт Дж., Мотвани Р., Ульман Дж. Введение в теорию автоматов, языков и вычислений. М.: Вильямс, 2001. 528 c.

49. Mealy G. H. A Method to Synthesizing Sequential Circuits // Bell Systems Technical Journal. AT&T, 1955. Vol. 5 (34). Pp. 1045-1079.

Moore E. Gedanken-experiments on sequential machines // Annals of mathematics studies, Princeton, N.J.: Princeton University Press, 1956. Vol. 34. Automata studies. Pp. 129-153.

http://www.ams.org/journals/proc/1961-012-04/S0002-9939-1961-0177048- 3/#sthash.PWMBmNS0.dpuf

Руководство по Matlab.Распространение событий для синхронизации состояний. http: //www. mathworks .com/help/stateflow/ug/broadcasting-

events-to-synchronize-states.html

Biere A., Cimatti A., Clarke E., Strichman O., Zhu Y. Bounded Model Checking // Advances in Computers. 2003. Volume 58. Pp. 117-148. http://fmv.jku.at/papers/BiereCimattiClarkeStrichmanZhu-Advances-58- 2003-preprint.pdf

Описание Therac-25.http://ru.wikipedia.org/wiki/Therac-25

S. Kane, E. Liberman, T. DiViesti, F. Click. Toyota Sudden Unintended Acceleration. Safety Research & Strategies, Inc, 2010.

http://www.safetyresearch.net/Library/ToyotaSUA020510FINAL.pdf

Блумберг. http://www.bloomberg.com/news/2012-10-17/knight-capital-

reports-net-loss-as-software-error-takes-toll-1-.html

Umrigar Z., Pitchumani !-.Formal verification of a real-time hardware design / Proceedings of the 20^th Design Automation Conference, 1983. http://portal.acm.org/ft_gateway.cfm?id=800667&type=pdf&CFID=112534 228&CFTOKEN=12780503

Chlipala A. Certified Programming with Dependent Types. Cambridge: The MIT Press, 2013. 424 p.

Официальная страница продукта Valgrind. http://www.valgrind.org/

Официальная страница компании Coverity. http://www.coverity.com/Официальная страница продукта PVS-Studio.

http: //www.viva64 .com/ru/pvs-studio/

Dynamic program analysis- Wikipedia.

http: //en.wikipedia.org/wiki/Dynamic_program_analysis

Глухих М. И., Ицыксон В. М. Программная инженерия. Обеспечения качества программных средств методами статического анализа : учеб. пособие // СПб.: Изд-во Политехн. ун-та, 2011. 150 с.

Java Pathfinder homepage.http://javapathfinder.sourceforge.net/

CBMC homepage.http://www.cprover.org/cbmc/

Разработка технологии верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода. Промежуточный отчёт по I этапу «Выбор направления исследований и базовых методов». http://is.ifmo.ru/verification/_2007_01_report-

verification.pdf

Разработка технологии верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода. Промежуточный отчёт по II этапу «Теоретические исследования

поставленных перед НИР задач».

http://is.ifmo.ru/verification/_2007_02_report-verification.pdf

67. Разработка технологии верификации управляющих программ со

сложным поведением, построенных на основе автоматного подхода. Промежуточный отчёт по III этапу «Экспериментальные исследования поставленных перед НИР задач».

http://is.ifmo.ru/verification/_2007_03_report-verification.pdf

68. Разработка технологии верификации управляющих программ со

сложным поведением, построенных на основе автоматного подхода. Заключительный отчёт по IV этапу «Обобщение и оценка результатов исследований». http://is.ifmo.ru/verification/_2007_04_report-

verification.pdf

69. Разработка технологии верификации управляющих программ со

сложным поведением, построенных на основе автоматного подхода. Отчёт о патентных исследованиях.

http://is.ifmo.ru/verification/_2007_01_patent-verification.pdf

70. Официальная страница инструментального средства Uppaal. http: //www. uppaal. org/

71. Бейзер Б. Тестирование черного ящика. Технологии функционального тестирования программного обеспечения и систем. СПб.: Питер, 2004. 165 c.

72. Promela reference - ltl. http://www.spinroot.com/spin/Man/ltl.html

73. Spin homepage.http://spinroot.com

74. Шошмина И. В., Карпов Ю. Г. Введение в язык Promela и систему комплексной верификации Spin. Учебное пособие. СПбГПУ. 2010. 111 с.

75. Лукин М. А., Шалыто А. А. Разработка и автоматическая верификация распределенных автоматных программ // Информационно-управляющие системы. 2013. № 5 (66). С. 43 - 50.

76. Лукин М. А. Верификация параллельных автоматных программ // Научно-технический вестник СПбГУ ИТМО. 2014. № 1 (89). С. 145-162.

77. Dijkstra E.W. Guarded commands, non-determinacy and formal derivation

of programs // CACM. 1975. Vol. 8. Pp. 453-457

http://www.cs.virginia.edu/~weimer/615/reading/DijkstraGC.pdf

78. ISO/IEC 9899:2011. Information technology - Programming languages - C, 2011. 683 p.

79. Promela reference- printf. http://spinroot.com/spin/Man/printf.html

80. Promela reference - Run-Time Options http://spinroot.com/spin/Man/Spin.html

81. Unimod home page. http://unimod.sourceforge.net/

82. Гамма Э., Хелм Р., Джонсон Р., Влиссидес Дж. Приемы объектно­ориентированного проектирования. Паттерны проектирования . СПб: Питер, 2001. 368 с.

83. Ульянцев В. Отчёт о верификации программы управления часами с будильником. is.ifmo.ru/verification/2013/alarm_clock_verification.pdf

84. Buzdalov, M., Sokolov, A. Evolving EFSMs Solving a Path-Planning Problem by Genetic Programming / Proceedings of Genetic and Evolutionary Computation Conference Companion. Pp. 591-594 (2012).

85. Lumelsky V., Stepanov A. Path planning strategies for a point mobile automaton moving amidst unknown obstacles of arbitrary shape // Algorithmica, 1987. Vol. 2. Pp. 403-430.

86. Kamon I., Rivlin E., Rimon E. A new range-sensor based globally convergent navigation algorithm for mobile robots / Proceedings of IEEE International Conference on Robotics and Automation, no. 1, 1996. Pp. 429-435.

87. Lukin M. A, Buzdalov M. V, Shalyto A. A. Formal Verification of 800 Genetically Constructed Automata Programs: A Case Study / Proceedings of the 10^th IBM Haifa Verification Conference, 2014. LNCS 8855. Pp. 165-170.