lect02 (К. Савенков - Верификация программ на моделях (2010)), страница 2
Описание файла
Файл "lect02" внутри архива находится в папке "К. Савенков - Верификация программ на моделях (2010)". PDF-файл из архива "К. Савенков - Верификация программ на моделях (2010)", который расположен в категории "". Всё это находится в предмете "надёжность программного обеспечения" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 2 страницы из PDF
Постановка задачи моделированияне все требования кпрограмме формализуемы2. Формализация описания программыописание программы предназначено дляудобства разработки и компиляции, ноне для проверки еѐ свойств3. Абстракцияуменьшение пространствасостояний программыСпасибо за внимание!Вопросы?Литература•••••Сайт курса:http://savenkov.cs.msu.su/mc.htmlКларк, Грумберг, Пелед. Верификациямоделей программ: Model checking,МЦНМО, 2002.Holzmann.
The Spin Model Checker: Primerand Reference Manual, Addison Wesley,2003.Peled. Software Reliability Methods,Springer, 2001.Сайт Spin: http://www.spinroot.com.Практикум•••••Ауд. 758, Linux, SPIN;6 задач, по мере прохождения курса;Экзамен – устный;E-mail: model-checking@lvk.cs.msu.su,Подписаться: отправить ФИО иномер группы наmodel-checking@lvk.cs.msu.su,• Информация и задачи – по почте..