lect03 (К. Савенков - Верификация программ на моделях (2010)), страница 2
Описание файла
Файл "lect03" внутри архива находится в папке "К. Савенков - Верификация программ на моделях (2010)". PDF-файл из архива "К. Савенков - Верификация программ на моделях (2010)", который расположен в категории "". Всё это находится в предмете "надёжность программного обеспечения" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 2 страницы из PDF
(2 )фокусируемся на «наблюдаемом» поведенииПримеры трассвычисление(1.1,2.1),0трасса a p 0трасса 2a!a !ba!a !b!aa b!aa ba!a !ba!a !bp < 2(1.2,2.1),0p += 1(1.1,2.1),1p > 0(1.1,2.1),1p -= 1(1.1,2.1),0p < 2(1.2,2.1),0p += 1...a p 0 bp1Свойства линейного времени• Атомарные высказывания:a - «находимся в точке отправки запроса»b - «находимся в точке приёма ответа»• Свойство:«после отправки запроса рано или поздно получим ответ»• Пример допустимых трасс:aØØØØØbØ…ØØØØØØØ…• Пример недопустимых трасс:aØØØØØØØ…aØØØØbaØ…Свойства линейного времени• Свойство φ определяет набор допустимыхтрасс,AP (2 )• Свойство φ выполнимо на трассе σ: • Система переходов TS удовлетворяетсвойству линейного времени φ:TS Traces(TS ) TS ( P) P Схема понятийСистема(описание)корректнаМодель(описание)Система(системапереходов)корректнаМодель(системапереходов)Система(трассы)корректнаМодель(трассы)адекватнаадекватнаТребованияСвойствалинейноговремениАбстракция трасс• Представим трассу в форме интерпретации I:I (tr) Ν, , где N – множество натуральных чисел, – отношение порядка на N , а : N AP {T, } , и при этомn 0, p AP ( n , p ) T p L( s )Абстракция трасс• Рассмотрим трассы tr и tr’ такие, что:I (tr) Ν, , I (tr' ) Ν, , ' : N AP {T, } ' : N AP' {T, }• Будем говорить, что tr’ является(корректной) абстракцией tr ( tr tr'), еслиAP' AP : N N : n, k N n k (n ) (k ) n N , p AP' (n, p ) ' ( (n ), p ) Пример абстракции трассp=q=r=p=q=r=p=q=r=p=q=r=p=q=r=AP={p,q,r}p=q=p=q=p=q=p=q=p=q=AP’={p,q}p=q=p=q=p=q=AP’={p,q}Схема понятийСистема(описание)корректнаМодель(описание)Система(системапереходов)корректнаМодель(системапереходов)Система(трассы)корректнаМодель(трассы)адекватнаадекватнаТребованияСвойствалинейноговремениУсловие корректности модели• Пусть P – система, φ – произвольноесвойство линейного времени.
(Корректной)моделью P называется такое М, что:если свойство выполняется на модели, тооно выполняется и на системе• Это выполняется тогда и только тогда, когда:для любой трассы исходной системы вмодели найдётся её корректная абстракцияУсловие корректности модели• Пусть P – система, φ – произвольноесвойство линейного времени. (Корректной)моделью P называется такое М, что:M P позволяет проверять свойствапрограммы на её моделиопределение• Это выполняется тогда и только тогда, когда:tr Traces(TS ( P))tr' Traces(TS ( M )) :tr tr'для проверки такого условия нужно рассмотреть всетрассы исходной системыдопускает, что в моделибольше состоянийнеобходимое и достаточное условиеДостаточное условие корректности• Какими же свойствами должна обладать TSмодели, чтобы быть корректной?– действиям и атомарным высказываниям моделидолжны быть сопоставлены действия и атомарныевысказывания системы,– каждому состоянию системы должно бытьсопоставлено состояние модели,– модель должна корректно сохранять множествоначальных состояний,– если в системе есть переход между двумясостояниями, в модели должен быть переход помежду соотв.
состояниями по соотв. действию,– соотв. состояния в модели и системе должны бытьразмечены атомарными высказываниями моделиодинаково.Достаточное условие корректности• Какими же свойствами должна обладать TSмодели, чтобы быть корректной?aTS S , Act , , I , AP, LTS ' S ' , Act ' , ' , I ' , AP' , L'aAct ' ActAP' AP : S S ' , s0 ' ( s0 )aas1 s2 ( s1 ) ( s2 )s S , L' ( ( s )) L( s ) AP'достаточное условиеПример корректной абстракциисистемы переходовp = ,q =q=q=aap = ,q =aq=q=bbp = ,q =bq=dp = ,q =q=cdefq=(P)fq=fτeeq=p = ,q =dq=q=p = ,q =cττ(M1)(M2)cСхема понятийСистема(описание)корректнаМодель(описание)Система(системапереходов)корректнаМодель(системапереходов)Система(трассы)корректнаМодель(трассы)адекватнаадекватнаТребованияСвойствалинейноговремениАдекватность модели• Модель называется адекватной, если:1.
Атомарные высказывания, в терминахкоторых задаются свойства, присутствуют вразметке модели2. Из нарушения свойства на модели следует,что оно нарушается и на исходной системеАдекватность модели• Модель называется адекватной, если:1.AP APMнеобходимое условие (можно вычислить)2.M P достаточное условие (нельзя вычислить)• Определить адекватность при построениинельзя, можно лишь обнаружитьнесоответствие и исправить модельПример корректной абстракциисистемы переходовp = ,q =q=q=aap = ,q =aq=q=bbp = ,q =bq=dp = ,q =q=cdefq=(P)fq=fτeeq=p = ,q =dq=q=p = ,q =cττ(M1)(M2)cПример – проверяемые свойства• В любом вычислении встречается состояние, когдаp= ∧q= – ни одна из моделей не адекватна,• Для любого пути верно, что за любым q= раноили поздно встретится q= – все моделиадекватны,• Между двумя состояниями с q= встречается неболее чем 3 состояния с q= – модель М1адекватна, М2 – нет.Схема понятийСистема(описание)корректнаМодель(описание)Система(системапереходов)корректнаМодель(системапереходов)Система(трассы)корректнаМодель(трассы)адекватнаадекватнаТребованияСвойствалинейноговремениСпасибо за внимание!Вопросы?.