Презентация 17 (Лекции)

Математическая логикаи логическое программированиеЛектор:Подымов Владислав Васильевичe-mail:valdus@yandex.ru2016, весенний семестрКороткое вступлениеВ чём состоит основная сложность анализа императивныхпрограмм?Короткое вступлениеВ чём состоит основная сложность анализа императивныхпрограмм?Они полны по Тьюрингу11То есть программами моделируются все вычислимые функцииКороткое вступлениеВ чём состоит основная сложность анализа императивныхпрограмм?Они полны по Тьюрингу1Значит, анализ их поведения настолько же труден, насколько идля машин Тьюринга212То есть программами моделируются все вычислимые функцииТо есть многие нетривиальные свойства программ неразрешимыКороткое вступлениеВ чём состоит основная сложность анализа императивныхпрограмм?Они полны по Тьюрингу1Значит, анализ их поведения настолько же труден, насколько идля машин Тьюринга2А что если сильно ограничить их возможности?12То есть программами моделируются все вычислимые функцииТо есть многие нетривиальные свойства программ неразрешимыКороткое вступлениеВ чём состоит основная сложность анализа императивныхпрограмм?Они полны по Тьюрингу1Значит, анализ их поведения настолько же труден, насколько идля машин Тьюринга2А что если сильно ограничить их возможности?Например, свойства такой программыπ: x ⇐ x + 500можно легко проверить12То есть программами моделируются все вычислимые функцииТо есть многие нетривиальные свойства программ неразрешимыКороткое вступлениеВ чём состоит основная сложность анализа императивныхпрограмм?Они полны по Тьюрингу1Значит, анализ их поведения настолько же труден, насколько идля машин Тьюринга2А что если сильно ограничить их возможности?Например, свойства такой программыπ: x ⇐ x + 500можно легко проверитьА что если несколько простых программ работают,взаимодействуя между собой и с внешней средой?12То есть программами моделируются все вычислимые функцииТо есть многие нетривиальные свойства программ неразрешимыКороткое вступлениеВ чём состоит основная сложность анализа императивныхпрограмм?Они полны по Тьюрингу1Значит, анализ их поведения настолько же труден, насколько идля машин Тьюринга2А что если сильно ограничить их возможности?Например, свойства такой программыπ: x ⇐ x + 500можно легко проверитьА что если несколько простых программ работают,взаимодействуя между собой и с внешней средой?(то есть образуют распределённую систему)12То есть программами моделируются все вычислимые функцииТо есть многие нетривиальные свойства программ неразрешимыВерификация распределённых системПримерvoid премия() {счёт += 1 000 000;}void зарплата() {счёт += 1 000;}Верификация распределённых системПримерvoid премия() {счёт += 1 000 000;}void зарплата() {счёт += 1 000;}Пусть все функции выплат параллельно изменяют переменную“счёт”Верификация распределённых системПримерvoid премия() {счёт += 1 000 000;}void зарплата() {счёт += 1 000;}Пусть все функции выплат параллельно изменяют переменную“счёт”Как изменится счёт после одной зарплаты и одной премии?Верификация распределённых системПримерvoid премия() {счёт += 1 000 000;}void зарплата() {счёт += 1 000;}Пусть все функции выплат параллельно изменяют переменную“счёт”Как изменится счёт после одной зарплаты и одной премии?{счёт = x}счёт ⇐ счёт + 1 000 000;счёт ⇐ счёт + 1 000{счёт = x + 1 001 000}Верификация распределённых системПримерvoid премия() {счёт += 1 000 000;}void зарплата() {счёт += 1 000;}Пусть все функции выплат параллельно изменяют переменную“счёт”Как изменится счёт после одной зарплаты и одной премии?{счёт = x}счёт ⇐ счёт + 1 000 000;счёт ⇐ счёт + 1 000{счёт = x + 1 001 000}{счёт = x}счёт ⇐ счёт + 1 000;счёт ⇐ счёт + 1 000 000{счёт = x + 1 001 000}Верификация распределённых системПримерvoid премия() {счёт += 1 000 000;}void зарплата() {счёт += 1 000;}Пусть все функции выплат параллельно изменяют переменную“счёт”Как изменится счёт после одной зарплаты и одной премии?{счёт = x}счёт ⇐ счёт + 1 000 000;счёт ⇐ счёт + 1 000{счёт = x + 1 001 000}{счёт = x}счёт ⇐ счёт + 1 000;счёт ⇐ счёт + 1 000 000{счёт = x + 1 001 000}Модель императивных программ утверждает, что всё работаеткорректноВерификация распределённых системПримерvoid премия() {счёт += 1 000 000;}void зарплата() {счёт += 1 000;}Пусть все функции выплат параллельно изменяют переменную“счёт”Как изменится счёт после одной зарплаты и одной премии?{счёт = x}счёт ⇐ счёт + 1 000 000;счёт ⇐ счёт + 1 000{счёт = x + 1 001 000}{счёт = x}счёт ⇐ счёт + 1 000;счёт ⇐ счёт + 1 000 000{счёт = x + 1 001 000}Модель императивных программ утверждает, что всё работаеткорректноНо так ли это?Верификация распределённых системПримерvoid премия() {счёт += 1 000 000;}премиясчёт = счёт + 106void зарплата() {счёт += 1 000;}счёт0зарплатасчёт = счёт + 1000Верификация распределённых системПримерvoid премия() {счёт += 1 000 000;}премиясчёт = счёт + 106счёт = 0 + 106void зарплата() {счёт += 1 000;}счёт0зарплатасчёт = счёт + 1000Верификация распределённых системПримерvoid премия() {счёт += 1 000 000;}премиясчёт = счёт + 106void зарплата() {счёт += 1 000;}счёт0зарплатасчёт = счёт + 1000счёт = 0 + 106счёт = 0 + 1000Верификация распределённых системПримерvoid премия() {счёт += 1 000 000;}премиясчёт = счёт + 106void зарплата() {счёт += 1 000;}счёт0зарплатасчёт = счёт + 1000счёт = 0 + 106счёт = 0 + 1000счёт = 106106Верификация распределённых системПримерvoid премия() {счёт += 1 000 000;}премиясчёт = счёт + 106void зарплата() {счёт += 1 000;}счёт0зарплатасчёт = счёт + 1000счёт = 0 + 106счёт = 0 + 1000счёт = 1061061000счёт = 1000Верификация распределённых системПримерvoid премия() {счёт += 1 000 000;}премиясчёт = счёт + 106void зарплата() {счёт += 1 000;}счёт0зарплатасчёт = счёт + 1000счёт = 0 + 106счёт = 0 + 1000счёт = 1061061000счёт = 1000Где мой миллион?!Верификация распределённых системПримерvoid премия() {счёт += 1 000 000;}премиясчёт = счёт + 106void зарплата() {счёт += 1 000;}счёт0зарплатасчёт = счёт + 1000счёт = 0 + 106счёт = 0 + 1000счёт = 1061061000счёт = 1000Где мой миллион?!Такая ошибка возникает крайне редко, и потому считаетсятруднообнаружимой и невоспроизводимойВерификация распределённых системК чему приводят такие ошибки?11Карпов.

Model checking. 2010Верификация распределённых системК чему приводят такие ошибки?1I11996 взорвалась ракета “Ариан 5”; причина: ошибка в навигационнойпрограмме бортового компьютера; прямой ущерб: 7 млрд.$Карпов. Model checking. 2010Верификация распределённых системК чему приводят такие ошибки?1I1996 взорвалась ракета “Ариан 5”; причина: ошибка в навигационнойпрограмме бортового компьютера; прямой ущерб: 7 млрд.$I1994 массовая замена дефектных процессоров компанией Intel;причина: ошибка в программе деления; ущерб: сотни миллионов $I2009 банк UBS чудом избежал потери 31 млрд.$: из-за системнойошибки к заказу на 310 тыс.$ добавилось 5 нолей1Карпов. Model checking. 2010Верификация распределённых системК чему приводят такие ошибки?1I1996 взорвалась ракета “Ариан 5”; причина: ошибка в навигационнойпрограмме бортового компьютера; прямой ущерб: 7 млрд.$I1994 массовая замена дефектных процессоров компанией Intel;причина: ошибка в программе деления; ущерб: сотни миллионов $I2009 банк UBS чудом избежал потери 31 млрд.$: из-за системнойошибки к заказу на 310 тыс.$ добавилось 5 нолейI1982 при лечении аппаратом облучения раковой опухоли Therac-25погибло 2 человека, несколько остались инвалидами; причина:ошибка программы управления облучением, очень редкоинтенсивность облучения возрастала на 2 порядкаI1995 крушение самолёта “Боинг-757”, 159 погибших; причина: ошибкав одном символе программной системы управления полётом1Карпов.

Model checking. 2010Верификация распределённых системКак обнаруживать такие ошибки?Верификация распределённых системКак обнаруживать такие ошибки?Например, если все компоненты распределённой системыпростые, то что мешает явно перебрать все сценарии работы идля каждого из них убедиться в отсутствии ошибок?Верификация распределённых системКак обнаруживать такие ошибки?Например, если все компоненты распределённой системыпростые, то что мешает явно перебрать все сценарии работы идля каждого из них убедиться в отсутствии ошибок?Пусть в системе параллельно работают 70 программ, каждая изкоторых совершает одно действие и завершаетсяТогда всевозможных сценариев работы будет 70!Гугол(и даже немного больше)Верификация распределённых системКак обнаруживать такие ошибки?Например, если все компоненты распределённой системыпростые, то что мешает явно перебрать все сценарии работы идля каждого из них убедиться в отсутствии ошибок?Пусть в системе параллельно работают 70 программ, каждая изкоторых совершает одно действие и завершаетсяТогда всевозможных сценариев работы будет 70!Гугол(и даже немного больше)При этом разные последовательности действий могут приводитьк совершенно разным и неожиданным результатамВерификация распределённых системКак обнаруживать такие ошибки?Например, если все компоненты распределённой системыпростые, то что мешает явно перебрать все сценарии работы идля каждого из них убедиться в отсутствии ошибок?Пусть в системе параллельно работают 70 программ, каждая изкоторых совершает одно действие и завершаетсяТогда всевозможных сценариев работы будет 70!Гугол(и даже немного больше)При этом разные последовательности действий могут приводитьк совершенно разным и неожиданным результатам(где мой миллион?!)Верификация распределённых системКак обнаруживать такие ошибки?IтестированиеIверификацияВерификация распределённых системКак обнаруживать такие ошибки?IIтестирование: исполнять программу на заданных наборахвходных данных и искать отклонения от ожидаемыхрезультатовверификацияВерификация распределённых системКак обнаруживать такие ошибки?IIтестирование: исполнять программу на заданных наборахвходных данных и искать отклонения от ожидаемыхрезультатов— не подходитверификацияВерификация распределённых системКак обнаруживать такие ошибки?IIтестирование: исполнять программу на заданных наборахвходных данных и искать отклонения от ожидаемыхрезультатов— не подходит (почему?)верификацияВерификация распределённых системКак обнаруживать такие ошибки?IIтестирование: исполнять программу на заданных наборахвходных данных и искать отклонения от ожидаемыхрезультатов— не подходит (почему?)верификация:Iпостроить адекватную модель программыВерификация распределённых системКак обнаруживать такие ошибки?IIтестирование: исполнять программу на заданных наборахвходных данных и искать отклонения от ожидаемыхрезультатов— не подходит (почему?)верификация:IIпостроить адекватную модель программызаписать требования к программе на формальном языкеВерификация распределённых системКак обнаруживать такие ошибки?IIтестирование: исполнять программу на заданных наборахвходных данных и искать отклонения от ожидаемыхрезультатов— не подходит (почему?)верификация:IIIпостроить адекватную модель программызаписать требования к программе на формальном языкестрого доказать соблюдение требований для всехвычислений моделиВерификация распределённых системКак обнаруживать такие ошибки?IIтестирование: исполнять программу на заданных наборахвходных данных и искать отклонения от ожидаемыхрезультатов— не подходит (почему?)верификация:IIIпостроить адекватную модель программызаписать требования к программе на формальном языкестрого доказать соблюдение требований для всехвычислений моделиСамый известный метод верификации распределённых систем —метод проверки моделей (model checking)Верификация распределённых системКакие свойства распределённых систем проверяются методомmodel checking?Верификация распределённых системКакие свойства распределённых систем проверяются методомmodel checking?В требованиях, предъявляемых к работе распределённойсистеме, часто так или иначе присутствует времяВерификация распределённых системКакие свойства распределённых систем проверяются методомmodel checking?В требованиях, предъявляемых к работе распределённойсистеме, часто так или иначе присутствует времяНапример:void премия() {счёт += 1 000 000;}void зарплата() {счёт += 1 000;}Верификация распределённых системКакие свойства распределённых систем проверяются методомmodel checking?В требованиях, предъявляемых к работе распределённойсистеме, часто так или иначе присутствует времяНапример:void премия() {счёт += 1 000 000;}void зарплата() {счёт += 1 000;}Требование: если мне положены одна зарплата и одна премия,то на счету появятся миллион и тысячаВерификация распределённых системКакие свойства распределённых систем проверяются методомmodel checking?В требованиях, предъявляемых к работе распределённойсистеме, часто так или иначе присутствует времяНапример:void премия() {счёт += 1 000 000;}void зарплата() {счёт += 1 000;}Требование: если мне положены одна зарплата и одна премия,то на счету появятся миллион и тысячаИными словами: при любом развитии событий (во времени)после завершения работы функций “премия” и “зарплата” ксчёту добавится 1 001 000Верификация распределённых системЕщё один пример:Имеется несколько компьютеров, не взаимодействующих междусобой, но имеющих доступ к сетевому принтеруВерификация распределённых системЕщё один пример:Имеется несколько компьютеров, не взаимодействующих междусобой, но имеющих доступ к сетевому принтеруКак корректно организовать взаимодействие компьютеров спринтером?Верификация распределённых системЕщё один пример:Имеется несколько компьютеров, не взаимодействующих междусобой, но имеющих доступ к сетевому принтеруКак корректно организовать взаимодействие компьютеров спринтером?Считаем, что принтер работает последовательно и может бытьзанят (какой-либо компьютер передаёт на него данные) илисвободен (никакие данные не передаются)Верификация распределённых системКорректное взаимодействие компьютеров с принтеромудовлетворяет следующим требованиям:Верификация распределённых системКорректное взаимодействие компьютеров с принтеромудовлетворяет следующим требованиям:1.