2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 31
Текст из файла (страница 31)
Построенный автоматически кошрпрнмер является ценной информацией, которы позволют найти ошибки в разработке, представленной моделью 24. Основой этого подхода яшшстся формальная модель — автомат Бюхи, позволяющий конечным обршом задавать бесконечные шыки. Автомат Бюхи отличается от обычного конечного автомата тем, по его семантика определена на а.словах — бескоиечнык цепочках символов. м -слово допускается авто- Спея лов, рова поде зто улоб абст1 (наш проб лось, явлю ряюп аспас ретин песке слою та Бк зтоы Гилея е линями раннца гктуру пригн ф не ой ниенной яозво- хи от.
гелена ~ авто. матом Бюхн, если существует допускающее состояние автомата, которое проходится бесконечное число раз прн приеме этого слова. В этой главе бьщо покюано. что с помощью автомата Бюхи, т. е. конечной моделью, можно представить все бесконечнью траектории поведения, удовлетворяющие заданной формуле линейной темпоральной логики. Следует ясно понимать, что автомат Бюхн — это не операционное устройст'- во, которое "действует", "функционирует" под воздейсзинем входных сипшэов, как-то выбирает дальнейший путь движения, если выбор недстермнннроваи, подсчитывает число попаданий в допускающие состояния и на основе лодсчеш долускщт илн отвергает бесконечные цепочки.
Автомвт Бюхи— зто не реальное устройспю, это просто абстракция, формальнав модель, улобная для ишлния н анааизв а -языков. С этой моделью можно выполнять абстрактные операции. Многие проблемы лля автомата Бюхн неразрешимы (например, проверка эквивалентности двух автоматов Бюхи). Но некоторые проблпяы разрешимы, и длв их решения можно построить алгоритмы. Оказалось, что анализ этой формальной модели позволяет решать аюкные пракгические проблемы. В частности, для автоматов Бюхи разрешима проблема пустоты допускаемого языка Поэтому если авданы два автомвта Бюхи, один из которых, В, описывает возможное функционирование проектируемой системы (бесконечное число бесконечных траекторий поведения), а другой, "контрольный" автомат Х, описывает все те поведения, которые не удовлетворяют некоторому желаемому свойству (т.
е. допускает все "неправильные" траектории), то, выполнив операцию синхронной композиции над этими моделями, мы строим новый автомат Бюхи В ЭХ, по которому можем установить, возможны ли некорректные" траектории в будущем поведении нашей, системы, проверив непусппу языка, допускаемого автоматом В З К . Именно эта техника н описана в данной главе. Одним из этапов этой тшаящш является построение автомата Бюхн, допускающего все цепочки, удовлетворяющие задюпюй ЬП,формуле (отрицанию формулы, представляющей проверяемое требование). Этот этап являетгл одним из самых трудоемких в теоретико-автоматном подходе к верификации дискретных систем. Существует несколько подходов к процедуре такой трансляции, все они концептуально сложны н обычно проводятся в два шага.
Первый шаг — построение автомата Бюхи, гарантированно удовлспюршощего поставленным требованиям. На этом шаге обычно получается автомат, сложность которого экспоненцнальна ошссительно рассматриваемой формулы. Для того чтобы сделать зффекгивэ ными следующие эшпы процесса верификации (построение синхронной композиции автоматов и поиск в этой композиции циклов, содержшпих принимающие состояния), обычно выполняется второй швг, который заключаст- Гоша 4 4.1 4ры ! форз где ству 4.2.1 4.11. Замечания в ох ряюг сэ в миннмнэапии полученного автомата. Выше был приведен концешуальпо шшболее простой из алгоритмов, вьнишняющих первый шаг.
К настоящему времени неизвестны эффективные общие процедуры получения по формуле ПЧ. минимального автомата Бюхи: наилучшие известные мевды основаны на использовании эвристик для такой минимизации. На основе разработанной теории были построены мощные системы эерифиюшии, в частности, Соэрап (КоЬеп Р. Кишйап) и бр!и (Севгд К Но!впало), которые в настоящее время широко используются для верификации крупных црограммно-аппаратных проектов. Система верификации бр!и будет подробно рассматриваться нами палее. За ршработку теоретико.автоматного метода н практическую реализацию мощных инструментов длэ формальной верификации реагирующих систем, основанных на этом метом, четверо ученых, Птагд 1. Нойпмпп, КоЬеп Р. Кшхйап, МозЬе У. тгтд! н Р!епе 1«о(рт, а 2005 г. были награждены премией АСМ "Р.КалпеЫм 17могу апа' ргаст!се аичэтг .
В пресс-релизе АСМ, посвященном этой награде, гоэорнтся: "Ключетт щюблемой компьютерной науки яавыннп поиск методов проверки люго, что ртработанное тшаратное и программное обеспечение соотеетстеует своей снецифихации Эта нробеема особенно актуальна для реагт«зующих систем, которые взаимодействуют со своим окрулсением, такит, юпг «ифроеые сиетемы и коммунюкщнонные протаколы. Четыре лауреата премии показали как вопрос щюеерки корректности реагирующих систем относнтем но еырапгтельной спецификации молсет быть сведен к пробпемам, связанным с конечныни оегнанатаыи на бесконечнык кгодных последоеательностят. Оии показали, что на осноее этого вздхода могут быть построены эффективные алгоритмы, нозеаетощиг аетотатизироеать докапинельстнео корректности на грактике.
Разработка теоретико-автоматного подпади к аерифитщии потребовала навьи результатов как е теории аетомапию, так и е области программ ньи логик". Теоретико. мпоматиый подход к проэаркв выполнения формул СТЬ предяошен Мояйе Утд) и Р!мте «Цо)рт э [143), [145), [142). Как говорилось выше, существуют разные пути обобщения модели конечного автомата, чюбм он мог допусвпь бесконечные цепочки. Формальную модель рассмотренного нами автомата Бюхн — распознавателя м -языков — ээел Рдсйагд ВэсЫ [26).
Проблема построения автомата Бюхи по заданной формуле ЬТЬ вызвала бшвшой нншрсс, юморый не пропал н в настоящее время. Суцистауег не- скол мат При ршу тнз' тель аэто шее здес Суш боле ноет (Роб тел), ээед В хо н от мул елее 4 вльно лучел ные жфи~апа), нных щию :тем, оЬеп еми- хм,.Р- юш)маитп, 'ама Рюем бле- едаыть ашь шюиеа-, ню~ше, ~ он юго 6].
ила не- сколыю подходов к ее решению, однако все они в худшем случае лают ее!амат Бюхн, экспоненциально слвкный отношпельно панны ЬТ( формулы. Приведенный в этой главе алгорипа построения автомата Бюхи основан на результатах, изложенных в работе (М МиlаЫ 2!леаг-)Ъне Тетрага( Ьщ)с алд Вкс)л ЛшатШа, 1997), а также в [145] и [86]. В [19] приводится доказа.- тельство сложности построенного этим методом автомата Бюхи. О конечных автоматах и распознавании ими языков мшкно прочзпвть в [158].
Нанболь. шее распространение среди систем верификации, основанных на описанной здесь технике, получила система Брзп [80], [79]. Она описывается в гл. 7. Существует несколько разработок, авторы которых пьггакпся сделать еще более выразительными и удобными для практической верификации возмшкнасгн формальной спецификации на азыке (ЛЧ.. Например, язык РП (Гагбрес Тешрогв! Еой!с, [6]), разработанный в 2002 г. компанией !пю! (Интел), для более удобной спецификации свойств систем расширяет логику БТЬ введением логических и арифметических операций на битовых векгорвх. В этом юыке используется также возмолшость описвниа регулярных собмтий н отношений ммкду этими событивмн, хотя основой его остается язык фор.
мул логики (.Т(.. 4.12. Задачи к главе 4 4.1. Ка~о~ сеайапю азрукгуры Кринке с л саапжннямн (э„...зе» вырвлшезпя формулой: Е~рр! лб()ь юХП-р!)л...лир„лб(р„юХС р„)1 где р,,...р„— атомарные предикаты, причем предикат р„истинам только а состоянии зг . Постройте структуру Кршню, удавлетеоршошую этому свойству. 4,2. Какое свойство структуры Кринке выражается формуларл Е[ре лХр! лХХхч л...лХ"р„1з, пш р„,.р„— атомарные предивны, причем преликат рг испшен тольао в состоянии з„структуры Кринке.
Постройте структуру Кринке, удовлетворяющую этому авойству, 4З. Пусть задан автомат Л (а,у бе,б,зт), где Я (зе,я!,яг), Б (а,б), бе=(яе) ° 8 ((яа и яз) (зеЬФг) (ез а эз) (ягАгг) (а!Аяг)] ° и =(з!) . Гласа 4 Приведите примеры цепочек, которые допускает А, если его рюсматриеать а) как конечный автомат; б) как автомат Бюхн. 4А. Докажите, что не существует детерминированного автомата Бюхн, допусквошего все цепочки с конечным числом вхождений а и бесконечным числом вхождений Ь (недепрминированный автомат Бюхи, допускающий этот язык, представяен на рис. 4.8).
Этот пример показывает, что нслетерминированнме автоматы Бюхи имеют более широкие возможноспь чем детерминированные. 4 Укеэвнив Доквкитч, что детерминированный автомат, чтобы допустить любую цепочку с конечным числом вхожаеннй с н бесконечным числом вхождений Ь при подаче на его вход символа а, а затем конечной цепочяи ю символов Ь, должен посетить допускмощее состояние после конечного числа символов Ь.
Покажите, что зту процедуру можно повторить. 4,5. На рнс. 4.7 представлен автомат Бюхзь распознавший мщлкестяо Ь та- ких бесконечных цепочек над Е =(а,Ь(, которые включают бесконечное чис- ло симвиоа Ь. Дополнение этого е-юыка — а-язык Е/Е, цепочки к<иоро- го включают только конечное число символов Ь. Постройте автомат Бюхн, который распознает юык Е1Е. 4.6. Постройте формулу ЕТ)„выражающую свойство: "состояние, удавле- яморлюлзсе р, встречается самое баеыиее адни роз яа кахдом еычислеиия". Постройте струкгуру Кринке, на которой эта формула выполняется.
4.7. Постройте минимальный конечный автомат, распознаккций язык Ь" се. Какой язык допускает этот автомат, если его раасматрнватысак автомат Бюхи7 4.8. По проязвсльно заданной структуре Кринке К и формуле Ф ЕТ3. про- верьте вручную, удовлетворяется лн формула Ф на структуре Кринке К. Дла этого постройте автоматы Бехи Ак и В„е, постройте их композицию и проверьте, пусто ли пересечение языков Ьк и Е ь. 4.9. Постройте автомат Бюхи, распознмощий все цепочки, задаваемые ЬТ! формулой Ср для входных алфавитов Е=(р! и Е (р,с(. 4.19, Постройш автоматы Бюхн, распознающие все цепочки, задаваемые !.Т! формулами Ср, рг,ХС-яЬС(рмзрУд~)РСр,СР р,р(р л(юг), р1)Ф (1%р) иь (СР 1), ХХР 4.11.
пост! 4.12. О ес О ка О сс не О ес ко О есз А! оп О ии вг 4.13. ~ О есз нн О всг вм 4Л4.! плети 4Л5. 1 4.17. ! вилам 4.18. ! вилам 'лаев е и, дошлым ющий 1МФют юбую а вхо- ипочге ко- ювтоторо. йохи, виля.нии". ьаь. охи2 прое К. шюи БТ! 4.11. По обобщенному автомату Бюхи л (о,Б,Яе,б,г"), где: У=(зо,з~) Б=(л Ь) Бе=(яе) б ((зе,а,зе),(ле,Ь,Я!),(Я,,Ь,Я~), (выа,зе)), в=Две) (л~Ц постройте зквивалеигный автомат Бюхн.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
