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

Верификация программна моделяхЛекция №2Моделирование программКонстантин Савенков (лектор)Контрольная работа•  15 минут•  3 вопроса: 1 сложный (10 баллов) + 2простых (по 5 баллов)•  Эти баллы не связаны с баллами практикума•  Оценка–  0..9 баллов – не засчитывается, доп. вопросы потеме на экзамене; если так по большинствуконтрольных, то -1 балл к оценке за курс,–  10..19 баллов (формально правильные краткиеответы) – ОК,–  20 баллов (развёрнутый ответ, демонстрирующийпонимание) +1 балл; если таких много, то +1 коценке за курс => автоматПлан лекции•  Формальные методы проверкиправильности программ: место вжизненном цикле ПО, автоматизируемость•  Верификация программ на моделях:области применения, общая схема•  Моделирование программ: моделируемыесвойства, состояние программы, процесспостроения моделиФормальные методыпроверки правильностипрограмм(место в жизненном цикле ПО,вопросы автоматизации)Итоги предыдущей лекцииАнализПроектированиеТребованияВалидацияТестированиеСтатическийанализ кодаДоказательствотеоремВерификацияна моделяхДинамическаяверификацияРеализацияПроектЭксплуатацияКодАвтоматизируемостьметодов верификации•  Тестирование: автоматическое иавтоматизированное,•  Доказательство теорем: существенное участиечеловека,•  Статический анализ: полностьюавтоматический для заданной области и свойства,•  Верификация на моделях: участие человекапри построении модели и при анализеконтрпримеров,•  «Комбинаторный взрыв».Верификация программ намоделях(области применения, общаясхема, проверяемые свойства)Области примененияверификации на моделях• • • • • • Сетевые и криптографические протоколы,Протоколы работы кэш-памяти,Интегральные схемы,Стандарты (напр.

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

свойства линейного времени•  Модель генерирует трассы, по которым можнопроверить свойства,СистемаМодель•  Абстракция от лишних состояний.СвойстваСостояние программы•  Состояние программы – совокупность значенийобъектов данных и счётчика управления,•  Как правильно оценить количество состояний?СпецификацияпрограммыИсходный кодна языкевысокогоуровняИсполняемыйкод (ASM)ПрограммноаппаратнаясистемаРаботающийкомпьютерМожет вообще небыть состояний(statelessпротоколы)Данные –переменныеязыка, счетчик –номервыполняемогооператораДанные –ячейки памяти вадресном пр-вепроцессора ирегистры,счётчик -регистр командпроцессораДанные – ячейкипамятиразличных ЗУ,кэш, буферавыборки,состояниеконвейеров,Счётчик – адреспоследнейкомандыАтомы,электроны,спины …•  Понятие состояния всегда связано с некотороймодельюСостояние программы(на уровне языка С)0:1:2:3:4:5:6:7:int compare(int a, int b) {int res;if (a < b) {res = -1;} else if (a >= b) {res = 1;} else {res = 0;}return res;}Потенциально –8*296состояний3 целочисленных переменных,|int| = 232,7 операторов языка +терминальный оператор.Состояние программы(на уровне языка С)0:1:2:3:4:void foo(int a) {int x = 5;if (a < x) {x = x-a;}}0:1:2:void bar(int b) {int x;x = b;}Потенциально –15*2128состояний4 целочисленных переменных,|int| = 232,2 потока управления, в foo – 5операторов, в bar – 3.Достижимые состояния•  Состояние называется достижимым, еслисуществует вычисление программы, вкотором оно присутствуетформализация – позже•  Достижимость состояния в программе вобщем случае алгоритмическинеразрешима.неразрешима дажедостижимость точкипрограммыЧисло достижимых состояний0:1:2:3:4:5:6:7:int compare(int a, int b) {int res;if (a < b) {res = -1;} else if (a >= b) {res = 1;} else {res = 0;}return res;}8*4*264переменная resможет приниматьтолько 4 значения7*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;}Пример построения моделипрограммы#include <stdio.h>#include <stdlib.h>int main() {FILE* f;int inWord = 0;enum {FALSE, TRUE} P1 = any(),P2, P3;if (P1) {return 1;}f = fopen(“sample”, "r");if (f == NULL) {return 1;}while (P2 = any()) {if (P3 = any()) {if(inWord)inWord = 1;}} else {inWord = 0;}}fclose(f);return 0;}Пример построения моделипрограммы#include <stdio.h>#include <stdlib.h>int main() {FILE* f;int inWord = 0;enum {FALSE, TRUE} P1 = any(),P2, P3;if (P1) {return 1;}f = fopen(“sample”, "r");if (f == NULL) {return 1;}while (P2 = any()) {if (P3 = any()) {if(inWord)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.  Постановка задачи моделированияне все требования кпрограмме формализуемы2.  Формализация описания программыописание программы предназначено дляудобства разработки и компиляции, ноне для проверки её свойств3.  Абстракцияуменьшение пространствасостояний программыСпасибо за внимание!Вопросы?.