Лекция 2. Моделирование программ (Лекции)

НАДЁЖНОСТЬ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯЛекция 2:Моделирование программВМиК МГУ им. М.В. Ломоносова,Кафедра АСВК, Лаборатория Вычислительных КомплексовАссистент Волканов Д.Ю.План лекции• Формальные методы проверкиправильности программ: место вжизненном цикле ПО, автоматизируемость• Верификация программ на моделях:области применения, общая схема• Моделирование программ: моделируемыесвойства, состояние программы, процесспостроения модели2Формальные методыпроверки правильностипрограмм(место в жизненномцикле ПО, вопросыавтоматизации)3Итоги предыдущей лекцииАнализПроектированиеТребованияРеализацияПроектЭксплуатацияКодВалидацияТестированиеСтатическийанализ кодаДоказательство теоремВерификацияна моделяхДинамическаяверификация4Автоматизируемостьметодов верификации• Тестирование: автоматическое иавтоматизированное,• Доказательство теорем: существенное участиечеловека,• Статический анализ: полностьюавтоматический для заданной области и свойства,• Верификация на моделях: участие человекапри построении модели и при анализеконтрпримеров,• «Комбинаторный взрыв».5Верификация программна моделях(области применения,общая схема,проверяемые свойства)6Области примененияверификации на моделях••••••Сетевые и криптографические протоколы,Протоколы работы кэш-памяти,Интегральные схемы,Стандарты (напр.

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

свойства линейного времени• Модель генерирует трассы, по которым можнопроверить свойства,СистемаМодельСвойства• Абстракция от лишних состояний.12Состояние программы• Состояние программы – совокупность значенийобъектов данных и счётчика управления,• Как правильно оценить количество состояний?Специфика Исходныйцияпрограммы код наязыкевысокогоуровняАтомы,Данные –Данные –ячейки памяти ячейки памяти электроны,в адресномразличных ЗУ, спины …пр-векэш, буферапроцессора и выборки,регистры,состояниесчётчик -конвейеров,Счётчикс –некоторойПонятие состояниярегистрвсегда связанокомандадресмоделью13последнейпроцессоракомандыМожет вообщене бытьсостояний(statelessпротоколы)•Исполняем Программн Работающиый кодйо(ASM)компьютераппаратнаясистемаДанные –переменныеязыка,счетчик –номервыполняемогооператораСостояние программы(на уровне языка С)0:1:2:3:4:5:6:7:int compare(int a, int b) {int res;if (a <b){res = -1;}elseif(a>=b){res = 1;}else{return resres;= 0;}}Потенциально –8*296состояний3 целочисленных переменных,|int| = 232,7 операторов языка +терминальный оператор.14Состояние программы(на уровне языка С)0:1:2:3:4:void foo(int a) {int x= 5;if(a < x) {x = x-a;}}void bar(int b) {0:int x;1:x = b;2: }Потенциально –15*2128состояний4 целочисленных переменных,|int| = 232,2 потока управления, в foo – 5операторов, в bar – 3.15Достижимыесостояния• Состояние называется достижимым, еслисуществует вычисление программы, вкотором оно присутствует• формализация – позже• Достижимость состояния в программе вобщем случае алгоритмически неразрешима.• неразрешима даже достижимость точки программы16Число достижимых состояний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;}8*4*264переменная resможетприниматьтолько4значения7*3*264return res;}5-й оператор недостижим17Пример построениямоделипрограммы• Программа подсчёта количества слов вфайле• Проверяемое свойство – всегда липрограмма закрывает открытый файл?• См.

следующий слайд.18Пример построения моделипрограммы#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]);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;return 1;}f = fopen(argv[1], "r");if (f == NULL) {printf("Can't open file:%s\n", argv[1]);return 1;}}19Пример построения моделипрограммы#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]);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;return 1;}f = fopen(argv[1], "r");if (f == NULL) {printf("Can't open file:%s\n", argv[1]);return 1;}}20Пример построения моделипрограммы#include <stdio.h>#include <stdlib.h> int main() {FILE* f;int c, wordCnt = 0, inWord = 0;while ((c = fgetc(f)) != -1) {enum {FALSE, TRUE} P1 = any();if (P1) {return 1;}f = fopen(“sample”, "r");if (!isspace(c)) {if (!inWord) {++wordCnt; inWord =1;}} else {inWord = 0;}}fclose(f); return0;if (f NUL {==L)}ret 1;urn}21Пример построения моделипрограммы#include <stdio.h>#include <stdlib.h> int main() {FILE* f;int c, wordCnt = 0, inWord = 0;while ((c = fgetc(f)) != -1) {enum {FALSE, TRUE} P1 = any();if (P1) {return 1;}f = fopen(“sample”, "r");if (!isspace(c)) {if (!inWord) {++wordCnt; inWord =1;}} else {inWord = 0;}}fclose(f); return0;if (f NUL {==L)}ret 1;urn}22Пример построения моделипрограммы#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 NUL {==L)}ret 1;urnwhile (P2 = any()) {if (P3 = any()) {if(inWord)inWord = 1;}} else {inWord = 0;}}fclose(f); return 0;}23Пример построения моделипрограммы#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 NUL {==L)}ret 1;urnwhile (P2 = any()) {if (P3 = any()) {if(inWord)inWord = 1;}} else {inWord = 0;}}fclose(f); return 0;}24Пример построения моделипрограммыint main() {en { FCLOSED,fileStum FOPEN, FERROR} ate;P2, P3;{ V0,V1 }enif (P1) {inWord = V0;returnum 1;}{FALSE, TRUE}if(any()){enP1fileState = =any(),FOPEN;um}else {fileState}= FERROR;if (fileState == FERROR) {return 1;}while (P2 = any()) {if (P3 = any()) {if (!inWord) { inWord =V1;}} else {inWord = V0;}}fileState = FCLOSED;return 0;}25Пример построения моделипрограммыint main() {enum { FCLOSED, FOPEN, FERROR} fileState;if(any()) {fileState = FERROR;} else if (any()) {fileState = FOPEN;while (any());fileState = FCLOSED;}return 0;}ENTRYFCLOSED1FOPENFERRORFCLOSED2EXIT26Моделирование• Модель – упрощённое описаниереальности, выполненноес определённой целью.• Например, карта – модель местности.27Моделирование• Модель – упрощённое описаниереальности, выполненноес определённой целью.• С одним объектом может быть связанонесколько моделей.• Каждая модель отражает свой аспектреальности• Например, схемы зданий:––––поэтажный планэлектропроводкаводоснабжениеплан эвакуации28Моделирование• Модель должна быть:– Простой,быть проще, чем реальность– Корректной,не расходиться с реальностью– Адекватной.соответствовать решаемой задачеНи одно из этих качеств нельзя проверить на основетолько описания модели29Моделирование• Пример сильной абстракции:30Построение модели• Формализуемые требования(постановка задачи моделирования)• Выбор языка моделирования• Абстракция системы с учётомтребований31Моделирование программпроцессconsumer:consumerfoobar#include <stdio.h>#include <sys/ipc.h>#include <sys/msg.h>#define MSG_LEN 100BARstruct msgbuf { mtype;mtext[MSG_LEN];longchar};FOOif ((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);}}32int main(int argc,const char* argv[]) {key_t key;int qid, i;struct msgbuf msg;ssize_t size;key = ftok("./mc_lec2_ex3", 1);}Моделирование программ#include <fcntl.h>#include <stdio.h>#include <string.h>#include <sys/ipc.h>#include <sys/msg.h>#define MSG_LEN 100struct msgbuf {longmtype;charmtext[MSG_LEN + 1];};процесс producer:producerint main(int argc,const char* argv[]) {key_t key; intqid;struct msgbuf msg;ssize_t size;msg.mtype = 1;key =ftok("./mc_lec2_ex3", 1);consumerif ((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");}33}}Свойства правильностипроцесса producer:• msgsnd всегда вызывается только послеmsgget;• если поток управления попадает вmsgget_error, то после этого не вызываютсяфункции msgsnd и msgrcv;• ни в одном вычислении не встречаютсяmsgrcv без msgsnd между ними.34#include <fcntl.h>#include <stdio.h>#include <string.h>#include <sys/ipc.h>#include <sys/msg.h>#define MSG_LEN 100struct msgbuf {longmtype;charmtext[MSG_LEN + 1];};Свойство №1процесс producer: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");}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);}}35#include <fcntl.h>#include <stdio.h>#include <string.h>#include <sys/ipc.h>#include <sys/msg.h>#define MSG_LEN 100struct msgbuf {longmtype;charmtext[MSG_LEN + 1];};Свойство №1процесс producer: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");}36}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);}#include#include#include#include#include#include<fcntl.h><stdio.h><string.h><sys/ipc.h><sys/msg.h><stubs.h>Свойство №1процесс producer: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();}}37Свойства правильностипроцесса producer:• msgsnd всегда вызывается только послеmsgget;• если поток управления попадает вmsgget_error, то после этого не вызываютсяфункции msgsnd и msgrcv;• ни в одном вычислении не встречаютсяmsgrcv без msgsnd между ними.38#include <fcntl.h>#include <stdio.h>#include <string.h>#include <sys/ipc.h>#include <sys/msg.h>#define MSG_LEN 100struct msgbuf {longmtype;charmtext[MSG_LEN + 1];};Свойство №2процесс producer: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");}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);}}39#include <fcntl.h>#include <stdio.h>#include <string.h>#include <sys/ipc.h>#include <sys/msg.h>#define MSG_LEN 100struct msgbuf {longmtype;charmtext[MSG_LEN + 1];};Свойство №2процесс producer: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");}40}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);}Свойство №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();}}невыполняется!подходит идля проверки41свойства №3Свойства правильностипроцесса producer:• msgsnd всегда вызывается только послеmsgget;• если поток управления попадает вmsgget_error, то после этого не вызываютсяфункции msgsnd и msgrcv;• ни в одном вычислении не встречаютсяmsgrcv без msgsnd между ними.42Корректная, но практическибесполезная модельint main() {enum {RUNNING, STOPPED} state;state = RUNNING;state = STOPPED;}RUNNINGSTOPPED43Построение модели• Задачи:1.

Постановка задачи моделированияне все требования к программе формализуемы2. Формализация описания программыописание программы предназначено дляудобства разработки и компиляции, но не дляпроверки её свойств3. Абстракцияуменьшение пространства состоянийпрограммы44Спасибо за внимание!45.