3 - Системы переходов (LTS). Корректность и адекватность LTS модели (1161367), страница 2

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

Текст из файла (страница 2)

(Корректной)моделью 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 – нет.Схема понятийСистема(описание)корректнаМодель(описание)Система(системапереходов)корректнаМодель(системапереходов)Система(трассы)корректнаМодель(трассы)адекватнаадекватнаТребованияСвойствалинейноговремениСпасибо за внимание!Вопросы?.

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

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