2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 32
Текст из файла (страница 32)
4Л2. Постройте ПЧ формулы, задакицие следующие свойства: 0 если сообщение и посылается неопределенно много раз перелвтчнком, оно будет принято неопределенно много рю приемником; 0 канал теряет только конечное число сообщений; 0 если процесс попал в критическую секцию, то он выйдвг нз нее,через конечное число временных шагов,' 0 если сообщение получено приемншсом, то оно было передано передатчиком по крайней мере на ! единицу времени раньше; 0 если в АШ загружена операция, то результат операции будет на выходе АИ> точно через 4 временных шага (испальзуйте двя определения шага оператор Х Х 0 ни одно шктоянне, в котором переменшш к равна 1, не будет достигнуго в процессе вычислений. 4.
13. Постройте 1Л1..формулы, описываюпше следукнцие свойства: 0 если случится р, то потом никогда не выполнигся 9; 0 всегда если р выполнится, то в будущем обюательно выполщпся 9, а зв ним сразу вышшнитсл г; 0 всегда после выполнения р когшьннбудь вмполнигсв 4, в До 9 не будет выполнено г. 4.14. Посцюйте струкгуру Кринке, нв которой формула СП. АСЕРР рыпои- нястся, а формула 1.Т!.
Срр — не выполшштся. 4.15. Постройте автомат Бюхи. допускающий цепочку (аЬ) . 4.14. Постройте автоматы Бюхн для фоРмУл РПЧ. РОьв шр Р ° рб(р л 9) по правилам, излакенным в п. 4,9. 4.17. Постройте автомат Бюхн дяв формулы яв((рл-4)5( рлр)) по пра' вилам, изложенным в п. 4.9. 4.1$.
Постройте автомат Бюхи двя формулы ьг(р л д)П6(-Р л 9) по правилам, излшкенным в п. 4.9. гл~ Ст! ка) В это МОЛЮ МОИЭЫ ирост тены, метро модеа смети В это, стрр к роль струк иые и мы,л тами. 5.1. реа Гра ООлас лом ~ форм вим глава 5 Структуры Крипке как модели реагирующих систем ° В этой главе показано, как реагирующие системы могут бмть представлены моделями с конечным числом состояний для послелующего их анализа с помощью техники воде! сйесипй, Используемая Здесь модель имеет ясную, простую и недвусмысленную семантику.
Модель всегда проще реальной системы, она строится с помощью абстрагированиа, отбрасывания части парвчегров, характеристик, особениосгей реальной сисюмы. При построении модели аюкно, побы она сохранила существенные черты исходной реальной системы. В этой главе приведены примеры представления реагнруницих систем в виде структуры Кринке. Для класса реагирующих систем, в которых основную роль играют потоки управгмния, а не потоки данных, фпрмалнзация в виде структуры Кринке зачастую полносп,ю адекватна, т. е. она отрюкает возмоягные порядки событий в исходной системе.
Протоколы, операционные сметены, логические системм управления — все зти программные системы могут естественным образом моделироваться струкэурой Кринке или ее вариантами. 6.1. Состояния и переходы реагирующей системы. Гранулярность переходов Формальному анализу при верификации с помощью метода вляЫ слесягпй подвергакпся не сами реагирукнцие сисюмьх а нх модели с конечным числом состояний — структуры Крипке. Структура Кринке — зто абстракция, формальная модель, и построение ее по реальной снотеме является важнейщим этапом процесса верификации. Структура Кринке должна адекватно Глаев 5 предспшлшь систему: если существенные свойства системы не представлены в модели, то верификация бессмысленна. Рассмотрим, как основные элементы модели Кринке — соспжния и переходы — соотносятса с состояниями и нх изменениями в реальных системах.
Понятие сссшоила существует в любой реальной системе. Состояние представляет собой мгновенный снимок (зпарзйог) всей информации о системе в каждый конкрпзпый момент времени. Кюклое состояние имеет конечное описание. Обычно это векюр значений переменных н точка управления в программе. Реальные системы часто имеют бесконечное число состояний из-за бесконечной области определений параметров.
В тех случаях, когда такие параметры не влияют на логику поведения программы, от них можно абстрагировшъся и Лля верификации строить модель системы с,конечным числом состояний. В часпюсти, в коммуникационных протоколах содержимое передаваемых сообщений не влияет на логику протокола. Во многих случаях для верификации программ область значений переменных можно ограничить. Например, потенциально бесконечный объем буфера или значения счетчиков молвю ограничить величиной 2 — 3, область значений вещественных переменных можно разлепить иа несколько классов эквивалентности.
Возникающие при таком абстрагировании дополнительные ошибки, выявленные верифнквтором, минно игнорировать после проверки найденных контрпримеров тестированием реальной системы. Мы рассматриваем дискретные системы, динамика которых представляется сменой состояний при функционировании системы в дискретные моменты времени. Смена состояний реальной системы вызывается выполнением возможных событий. Ииымн словами, дискретная система находится в некотором стабильном состоянии, и лод влиянием некоторого события (приема нли посылки сообшениа, выполнения операции, или внешнего события — например, нажатия кнопки мыши нли прихода тактового синхронизируюшего импульса) она переходит в другое состояние, тоже стабнлыюе (рис.
5.Ц. Задачей верификации является анаяиз неведения дискретной системы, динамики ее развития во времени. Поведение дискретной системы — зто бесконечная цепочка (последовательность) ее состояний, сменаюших друг друга. При верификации мы проверяем выполнение формул темпоральиой логики, истинность которых зависит от времени, хотя время явно в них не присутствует. Но как можно говорить о поведении системм во времени, не упоминая время? Удобство модели переходов в том и состоит, чго она абстрагируется от значений и понятий времени, учитывая только вжможные последовательности наступления событий и переходы системы нз одного состоянив в хрупы под воздействием этих событий. Переходы модели предстшишют изменения состояний реальной системы.
Как реаяьнва система переходит из одного своего соспжния в другое7 Какова Моды перед~ прохо, ти ш В дей мгнов спосгц ный" ~ с потел лорио паев З Члены емен- ЯМИ И Вэ ется :нгы или ° рн. им о Оп вбЛ вто юь) чак ова предеме в ' опи" про- Ю За шкне стра. СЛОМ Серег лля чить. ИКОВ мреюгю. при- ЕРОВ чна- зкоуга, гстная ВгУ протяженность перехода системы во времени."г Что происходит в реальней системе В прпгмссе перехода? Рис. К1.
Смена состояния реагирующей системы Во времени Модель соспжний и переходов абстрагируется От всех этих вопросов. Прн переходе модели нз состояния в состояние предполагаеюя, что модель не проходит промежуточных состояний в том смысле, что не существует "чпсми" перехошч система выполняет переход как бы "мгновенно". В дейстыпельности, мы не можем понимать термин ыгиоеепиый буквально: мгновенных процессов не бывает.
Кроме того, в нашем анализе мы всеми способами стараемся уйтн от явного выражения времени, а термин "мпювенный" связан именно с понятием реального времени. В реельных дискретных системах вместо понятия мгновенности обычно используется поняпщ "ашопариость" илн "неделиыосшь" изменения состояния. Атомарпосгь изменения состояния в реальной системе состоит в том, что при этом изменении реальная сисюма не проходит промежуточные этапы е следующем смысле: извне снсюма видна (наблюдаема) только либо в одном, либо в другом стабильном состоянии, но не в процессе изменения состояний.
зге Инымн словами, переходы системы будут атомарнымн, если пользователь системы и лругие активные процессм могут наблюцщь ее вежда в каком-те ее соспжнии либо до начала изменешш состояниа, либо после его завершения, но никогда во время изменения. Например, изменение значения переменной в результате выполнения оператора присваивания в реальной системе: х=5 не мажет быль частичным, мы можем лабюодлшь значение переменной з либо до, либо после выполнения операции присваивания, что абеспечиеаетса в реальных процессорах аппаратно. Таким образом, с точки зрения др иронесссе этот переход неделим, мгновенен.
Изменение значения той же переменной: я=я+5 уию не так просто. Чаще всего оно ревлнзуетса тремя неделимыми операциями: чтением старого значения х в регистр, изменением содержимого регистра и затем записью значения регистра в область памяти, отведенную для х. Если переменная х — локальная, и другие процессы не имеют к ней доступа, то в модели мы можем предспшить выполнение этого оператора одним переходом, изменяющим состояние. Если переменная х — разделяемая, то друпю процессм могут наблюдать (и изменять) промежуточные состояния, если они реально существуют при выполнении этого оператора. Поэтому в модели этот оператор следует представлять несколькими переходами с промежуточными состояниями. Если этот оператор в модели представить одним перехш дом, то построенная модель будет неадекватной и скрыжпь ошибки, существующие в системе.
Этот оператор мшкно представить в модели одним переходом в том случае, если этот оператор явно "эакрмваетса" с помощью специальных программных средств: семафоров, операций гезгчвньзег и т. п. Излишняя детализация при построении модели также вредна. Если оператор а действительности атомарный, а в модели он представлен несколькими переходами и промшкугочными состоаниямн, которые в реальности не видны лругнм процессам, то при анализе могут обнаружиться ошибки, которых ° действительности система не имеет.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
