2 - Моделирование программ (1161366)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

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

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:5:0:1:2:void foo(int a) {int x = 5;if (a < x) {x = x-a;}}void bar(int b) {int x;x = b;}Потенциально –18*2128состояний4 целочисленных переменных,|int| = 232,2 потока управления, в foo – 6операторов, в 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;}Пример построения моделипрограммы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. Абстракцияуменьшение пространствасостояний программыСпасибо за внимание!Вопросы?.

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов лекций