lect02 (1158543), страница 2
Текст из файла (страница 2)
Постановка задачи моделированияне все требования кпрограмме формализуемы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,• Информация и задачи – по почте..