lect02 (К. Савенков - Верификация программ на моделях (2010))

Верификация программна моделяхЛекция №2Моделирование программКонстантин Савенков (лектор)План лекции• Формальные методы проверкиправильности программ: место вжизненном цикле ПО, автоматизируемость• Верификация программ на моделях:история развития, области применения,общая схема• Моделирование программ: моделируемыесвойства, состояние программы, процесспостроения моделиФормальные методыпроверки правильностипрограмм(место в жизненном цикле ПО,вопросы автоматизации)Итоги предыдущей лекцииАнализПроектированиеТребованияВалидацияТестированиеСтатическийанализ кодаДоказательствотеоремВерификацияна моделяхДинамическаяверификацияРеализацияПроектЭксплуатацияКодАвтоматизируемостьметодов верификации• Тестирование: автоматическое иавтоматизированное,• Доказательство теорем: существенное участиечеловека,• Статический анализ: полностьюавтоматический для заданной области и свойства,• Верификация на моделях: участие человекапри построении модели и при анализеконтрпримеров,• «Комбинаторный взрыв».Верификация программ намоделях(история развития, областиприменения, общая схема,проверяемые свойства)История развития: фундамент• Флойд, 1967 – assertions, гипотеза одоказуемости корректности программы,• Хоар, 1969 – пред- и пост-условия, триплетыХоара (P | S | Q), логический вывод,• Бойер, Мур, 1971 – первый автоматическийпрувер,• Дейкстра, 1975 – Guarded Command Languages,• Хоар, 1978 – взаимодействующиепоследовательные процессы (CSP),• Милнер, 1980 – Calculus of CommunicatingSystems (CCS)История развития: развитиеметодов• Пнуэли, 1977 – темпоральная логика LTL,• Пнуэли, 1981 – логика ветвящегосявремени (CTL),• Кларк, Эмерсон, 1981 и Квили, Сифакис,1982 – model checking (обход достижимыхсостояний),• Варди и Вольпер, 1986 – новая техникаmodel checking (анализ конформности),• Хольцман, 1989 – верификатор SPIN.История развития: проблема«комбинаторного взрыва»• Бриан, 1989 – Двоичные решающиедиаграммы (BDD),• МакМиллан, 1993 – верификатор SMV(символьная верификация, BDD),• Хольцман, Пелед, 1994 – редукциячастичных порядков,• 1995 – редукция частичных порядковв SPIN.История развития: дальнейшееразвитие• Кларк, 1992 – абстракция для уменьшениячисла состояний модели,• Эльсаиди, 1994 – семантическаяминимизация,• Пелед, 1996, Бир, 1998 – верификациямодели «на лету»,• Равви, 2000 – анализ достижимости сучѐтом спецификации,• Эмерсон, Прасад, 1994 -- симметрияОбласти примененияверификации на моделях•••••••Сетевые и криптографические протоколы,Протоколы работы кэш-памяти,Интегральные схемы,Стандарты (напр.

FutureBus+),Встроенные системы,Драйвера,Вообще программы на C.Примеры использования SPIN• Верификация системыуправления дамбами вРоттердаме (Нидерланды)• Верификация АТСPathStar (Lucent)• Верификация аэрокосмических систем (DeepSpace 1,Cassini, Mars ExplorationRovers, итд.)Схема верификации на моделиСистемаТребованияКлассы свойствПостроение моделиСпецификациясвойства φМодель МНайденаошибкаВерификацияM φУдача!НедостаточноресурсовКонтрпримерАнализконтрпримераПримеры классов свойств• Стандартные:––––Отсутствие ошибок времени выполнения (RTE),Отсутствие тупика (deadlock),Отсутствие удушения (starvation),Не срабатывают ассерты (assertions).• Зависящие от приложения:––––Инварианты системы,Индикаторы прогресса,Корректная завершаемость,Причинно-следственный и темпоральный порядок насостояниях системы,– Требования справедливости.Моделирование программ(пример построения модели,общая схема моделирования)Зачем строить модели программ?• Свойства задают допустимые состояния ипоследовательности состояний (вычисления)т.н.

свойства линейного времени• Модель генерирует трассы, по которым можнопроверить свойства,СистемаМодель• Абстракция от лишних состояний.СвойстваСостояние программы• Состояние программы – совокупность значенийобъектов данных и счѐтчика управления,• Как правильно оценить количество состояний?СпецификацияпрограммыИсходный кодна языкевысокогоуровняИсполняемыйкод (ASM)ПрограммноаппаратнаясистемаРаботающийкомпьютерМожет вообщене бытьсостояний(statelessпротоколы)Данные –переменныеязыка, счетчик –номервыполняемогооператораДанные –ячейки памяти вадресном пр-вепроцессора ирегистры,счѐтчик -регистр командпроцессораДанные – ячейкипамятиразличных ЗУ,кэш, буферавыборки,состояниеконвейеров,Счѐтчик – адреспоследнейкомандыАтомы,электроны,спины …• Понятие состояния всегда связано с некотороймоделью программыСостояние программы(на уровне языка С)0:1:2:3:4:5:int compare(int a, int b) {int res;if (a < b) {res = -1;} else if (a >= b) {res = 1;} else {res = 0;}6:Потенциально –7*296состоянийreturn res;}3 целочисленных переменных,|int| = 232,7 операторов языка.Достижимые состояния• Состояние называется достижимым, еслисуществует вычисление программы, вкотором оно присутствуетформализация – позже• Достижимость состояния в программе вобщем случае алгоритмическинеразрешима.неразрешима дажедостижимость точкипрограммыЧисло достижимых состояний0:1:2:3:4:5:int compare(int a, int b) {int res;if (a < b) {res = -1;} else if (a >= b) {res = 1;} else {res = 0;}6:return res;}7*4*264переменная resможет приниматьтолько 4 значения6*3*2645-й оператор недостижимПример построения моделипрограммы• Программа подсчѐта количества слов вфайле• Проверяемое свойство – всегда липрограмма закрывает открытый файл?• См.

следующий слайд.Пример построения моделипрограммы#include <stdio.h>#include <stdlib.h>int main(int argc,const char* argv[]) {FILE* f;int c, wordCnt = 0, inWord = 0;if (argc < 2) {printf("Use: %s filename\n”,argv[0]);return 1;}f = fopen(argv[1], "r");if (f == NULL) {printf("Can't open file:%s\n",argv[1]);return 1;}while ((c = fgetc(f)) != -1) {if (!isspace(c)) {if (!inWord) {++wordCnt;inWord = 1;}} else {inWord = 0;}}printf("Word count: %d\n",wordCnt);fclose(f);return 0;}Пример построения моделипрограммы#include <stdio.h>#include <stdlib.h>int main(int argc,const char* argv[]) {FILE* f;int c, wordCnt = 0, inWord = 0;if (argc < 2) {printf("Use: %s filename\n”,argv[0]);return 1;}f = fopen(argv[1], "r");if (f == NULL) {printf("Can't open file:%s\n",argv[1]);return 1;}while ((c = fgetc(f)) != -1) {if (!isspace(c)) {if (!inWord) {++wordCnt;inWord = 1;}} else {inWord = 0;}}printf("Word count: %d\n",wordCnt);fclose(f);return 0;}Пример построения моделипрограммы#include <stdio.h>#include <stdlib.h>int main() {FILE* f;int c, wordCnt = 0, inWord = 0;enum {FALSE, TRUE} P1 = any();if (P1) {return 1;}f = fopen(“sample”, "r");if (f == NULL) {return 1;}while ((c = fgetc(f)) != -1) {if (!isspace(c)) {if (!inWord) {++wordCnt;inWord = 1;}} else {inWord = 0;}}fclose(f);return 0;}Пример построения моделипрограммы#include <stdio.h>#include <stdlib.h>int main() {FILE* f;int c, wordCnt = 0, inWord = 0;enum {FALSE, TRUE} P1 = any();if (P1) {return 1;}f = fopen(“sample”, "r");if (f == NULL) {return 1;}while ((c = fgetc(f)) != -1) {if (!isspace(c)) {if (!inWord) {++wordCnt;inWord = 1;}} else {inWord = 0;}}fclose(f);return 0;}Пример построения моделипрограммыint main() {enum { FCLOSED, FOPEN, FERROR} fileState;enum { V0, V1 } inWord = V0;enum {FALSE, TRUE} P1 = any(),P2, P3;while (P2 = any()) {if (P1) {if (P3 = any()) {return 1;if (!inWord) {}inWord = V1;if(any()) {}fileState = FOPEN;} else {} else {inWord = V0;fileState = FERROR;}}}if (fileState == FERROR) {fileState = FCLOSED;return 1;return 0;}}Пример построения моделипрограммыint main() {enum { FCLOSED, FOPEN, FERROR} fileState;if(any()) {fileState = FERROR;} else if (any()) {fileState = FOPEN;while (any());fileState = FCLOSED;}return 0;}ENTRYFCLOSED1FOPENFERRORFCLOSED2EXITМоделирование• Модель – упрощѐнное описаниереальности, выполненноес определѐнной целью.• Например, карта – модель местности.Моделирование• Модель – упрощѐнное описаниереальности, выполненноес определѐнной целью.• С одним объектом может быть связанонесколько моделей.• Каждая модель отражает свой аспектреальности• Например, схемы зданий:––––поэтажный планэлектропроводкаводоснабжениеплан эвакуацииМоделирование• Модель должна быть:– Простой,быть проще, чем реальность– Корректной,не расходиться с реальностью– Адекватной.соответствовать решаемой задачеНи одно из этих качеств нельзя проверитьна основе только описания моделиМоделирование• Пример сильной абстракции:Построение модели• Формализуемые требования(постановка задачи моделирования)• Выбор языка моделирования• Абстракция системы с учѐтомтребованийМоделирование программпроцесс consumer:#include <stdio.h>#include <sys/ipc.h>#include <sys/msg.h>#define MSG_LEN 100consumerstruct msgbuf {long mtype;char mtext[MSG_LEN];};foobarBARFOOif ((qid = msgget(key,IPC_CREAT | 0666)) == -1) {perror("Error creatingmessage queue");}while (1) {size = msgrcv(qid, &msg,MSG_LEN, 1, 0);for (i = 0; i < size; ++i) {msg.mtext[i] =toupper(msg.mtext[i]);}/* send it back */if (size > 0) {msgsnd(qid, &msg, size, 0);}}int main(int argc,const char* argv[]) {key_t key;int qid, i;struct msgbuf msg;ssize_t size;key = ftok("./mc_lec2_ex3", 1);}Моделирование программпроцесс producer:#include <fcntl.h>#include <stdio.h>#include <string.h>#include <sys/ipc.h>#include <sys/msg.h>#define MSG_LEN 100struct msgbuf {long mtype;char mtext[MSG_LEN + 1];};int main(int argc,const char* argv[]) {key_t key;int qid;struct msgbuf msg;ssize_t size;msg.mtype = 1;key =ftok("./mc_lec2_ex3", 1);producerconsumerif ((qid = msgget(key, IPC_CREAT| 0666)) == -1) {msgget_error:perror("Error creatingmessage queue");}while (1) {printf("Your message: ");fgets(msg.mtext, MSG_LEN, stdin);if (msgsnd(qid, &msg,strlen(msg.mtext), 0) == -1) {perror("Error sending");continue;}size = msgrcv(qid, &msg, MSG_LEN, 1, 0);if (size > 0) {printf("Reply is: %s\n", msg.mtext);} else {printf("No reply\n");}}}Свойства правильностипроцесса producer:• msgsnd всегда вызывается только послеmsgget;• если поток управления попадает вmsgget_error, то после этого невызываются функции msgsnd и msgrcv;• ни в одном вычислении не встречаютсяmsgrcv без msgsnd между ними.Свойство №1процесс producer:#include <fcntl.h>#include <stdio.h>#include <string.h>#include <sys/ipc.h>#include <sys/msg.h>#define MSG_LEN 100struct msgbuf {long mtype;char mtext[MSG_LEN + 1];};int main(int argc,const char* argv[]) {key_t key;int qid;struct msgbuf msg;ssize_t size;msg.mtype = 1;key =ftok("./mc_lec2_ex3", 1);if ((qid = msgget(key, IPC_CREAT| 0666)) == -1) {msgget_error:perror("Error creatingmessage queue");}while (1) {printf("Your message: ");fgets(msg.mtext, MSG_LEN, stdin);if (msgsnd(qid, &msg,strlen(msg.mtext), 0) == -1) {perror("Error sending");continue;}size = msgrcv(qid, &msg, MSG_LEN, 1, 0);if (size > 0) {printf("Reply is: %s\n", msg.mtext);} else {printf("No reply\n");}}}Свойство №1процесс producer:#include <fcntl.h>#include <stdio.h>#include <string.h>#include <sys/ipc.h>#include <sys/msg.h>#define MSG_LEN 100struct msgbuf {long mtype;char mtext[MSG_LEN + 1];};int main(int argc,const char* argv[]) {key_t key;int qid;struct msgbuf msg;ssize_t size;msg.mtype = 1;key =ftok("./mc_lec2_ex3", 1);if ((qid = msgget(key, IPC_CREAT| 0666)) == -1) {msgget_error:perror("Error creatingmessage queue");}while (1) {printf("Your message: ");fgets(msg.mtext, MSG_LEN, stdin);if (msgsnd(qid, &msg,strlen(msg.mtext), 0) == -1) {perror("Error sending");continue;}size = msgrcv(qid, &msg, MSG_LEN, 1, 0);if (size > 0) {printf("Reply is: %s\n", msg.mtext);} else {printf("No reply\n");}}}Свойство №1процесс producer:#include#include#include#include#include#include<fcntl.h><stdio.h><string.h><sys/ipc.h><sys/msg.h><stubs.h>if (msgget() == -1) {msgget_error:pass();}while (1) {pass();pass();if (msgsnd() == -1) {int main(int argc,const char* argv[]) {pass();continue;}pass();if (any()) {pass();} else {pass();}pass();pass();}}Свойства правильностипроцесса producer:• msgsnd всегда вызывается только послеmsgget;• если поток управления попадает вmsgget_error, то после этого невызываются функции msgsnd и msgrcv;• ни в одном вычислении не встречаютсяmsgrcv без msgsnd между ними.Свойство №2процесс producer:#include <fcntl.h>#include <stdio.h>#include <string.h>#include <sys/ipc.h>#include <sys/msg.h>#define MSG_LEN 100struct msgbuf {long mtype;char mtext[MSG_LEN + 1];};int main(int argc,const char* argv[]) {key_t key;int qid;struct msgbuf msg;ssize_t size;msg.mtype = 1;key =ftok("./mc_lec2_ex3", 1);if ((qid = msgget(key, IPC_CREAT| 0666)) == -1) {msgget_error:perror("Error creatingmessage queue");}while (1) {printf("Your message: ");fgets(msg.mtext, MSG_LEN, stdin);if (msgsnd(qid, &msg,strlen(msg.mtext), 0) == -1) {perror("Error sending");continue;}size = msgrcv(qid, &msg, MSG_LEN, 1, 0);if (size > 0) {printf("Reply is: %s\n", msg.mtext);} else {printf("No reply\n");}}}Свойство №2процесс producer:#include <fcntl.h>#include <stdio.h>#include <string.h>#include <sys/ipc.h>#include <sys/msg.h>#define MSG_LEN 100struct msgbuf {long mtype;char mtext[MSG_LEN + 1];};int main(int argc,const char* argv[]) {key_t key;int qid;struct msgbuf msg;ssize_t size;msg.mtype = 1;key =ftok("./mc_lec2_ex3", 1);if ((qid = msgget(key, IPC_CREAT| 0666)) == -1) {msgget_error:perror("Error creatingmessage queue");}while (1) {printf("Your message: ");fgets(msg.mtext, MSG_LEN, stdin);if (msgsnd(qid, &msg,strlen(msg.mtext), 0) == -1) {perror("Error sending");continue;}size = msgrcv(qid, &msg, MSG_LEN, 1, 0);if (size > 0) {printf("Reply is: %s\n", msg.mtext);} else {printf("No reply\n");}}}Свойство №2процесс producer:if (msgget() == -1) {#include <stub.h>msgget_error:pass();}while (1) {pass();pass();if (msgsnd() == -1) {int main(int argc,const char* argv[]) {pass();continue;}msgrcv();if (any()) {pass();} else {pass();}pass();pass();}}невыполняется!подходит идля проверкисвойства №3Свойства правильностипроцесса producer:• msgsnd всегда вызывается только послеmsgget;• если поток управления попадает вmsgget_error, то после этого невызываются функции msgsnd и msgrcv;• ни в одном вычислении не встречаютсяmsgrcv без msgsnd между ними.Корректная, но практическибесполезная модельint main() {enum {RUNNING, STOPPED} state;state = RUNNING;state = STOPPED;}RUNNINGSTOPPEDПостроение модели• Задачи:1.