2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 90
Текст из файла (страница 90)
введением временных границ на действие темпорального оператора Плй! и выводимых из него операторов. Формулы логики ТСТ(. (Т(шег( СП.) иитпрпретирукпсл на деревьях вычислений временного автомата. Верификация временного автомата относительно формулы логики ТСТАВ сводитса к верификации соответствующего графа регионов относительно некоторой СТ1 формулы с введением дополнительных "формульных" часов, устанавливаемых в 0 в состоянии, в котором проверяется формула.
Поэтому алгоритм пюде1 сйеск1пй для проверки выполнения формулы Ф логики ТСТАВ лля графа регионов состоит в последовательном выделении подформул формулы Ф и нахождении такого множества состояний графа. на которых эти подформулы выполняются. При этом, фактически, используется та же идея пометок состояний автомата подформулами формулы Ф, по и при верифиющни структур Кринке. Сложность твких алгоритмов при использовании графа регионов весьма велика. Временные зоны позволяют аналнзироешь свойства временного автомата, манипулируя только неравенствами из описания временного автомата и сн вр нь Рг 19 бь ве сь и, ш~ М сх ш~ (з Л1 вр м~ нг кг И~ пс ря В1 ре д( м~ И~ св нз символически задажпь огромные мнолиства регионов.
Для предстааяешш временных зон можно исполюовать матричное представление набора линейных неравенств в виде Пйуешпсе Вонпб Мвцгк — форму, исследованную еще Ричардом Беллманом в его книге "Динамическое программирование" в 1957 г. Для этого представления символьных состояний временного автомата были разработаны н алгоритмы верификации, в частности, алгоритмы проверки выполнимости формул логики ТСТВ для временных автоматов.
Несмотря на то, чзо эта область еще находится в слюни интенсивных исследований, уже разработаны опытные инструментальные сметены (Кюпоэ, ()ррва) и др.) лля анвлюа количественных свойств повеления систем в рамках расширений темпоральных логик. Существуют примеры промышленного применения изложенных здесь теоретических результатов.
Многие проблемы верификшши дча систем реального времени алгоритмически неразрешимы. Например, проблема тоде! сйесапй становится неразрешимой при следующих расширениях модели временного автомата: О ограничения на переходах (защизы) представлены линейными неравенствами (например, 2х > Зу); ъ ь. Ф Э 3 ь Ф М2.1?. Замечания Временные автоматы, как формальная модель для предсшвления систем реального времени, были введены в (2, 4, 5) и нсследовалнсь в множестве других работ. В работе (71] была предложена более интуитивная форма временного автомата с инвариантами в состояниях, обеспечивающими прогресс. Именно зта модель рассмотрена нами в двиной главе: она используется в нескольких инструментах верификации для анализа снесем реаяьного времени, например, ()ррва! н Клики.
(7 используются защиты переходов, в которых показания часов сравнивают с нерационвльнмми числами; (7 на переходах присутствуют юменения часов вида х.= х -1; 0 присугствуют операторы остановки часов. Проблема проверки модели для формул логики (.Т(., расширенной указанием временных интервалов действия темпоральных операторов, также ялгорщмически неразрешима. Если во временной логике ВТВ запретить использование сингулярных интервалов (Вш), то в такой постановке проблема прошрки модели является разрешимой.
Исследования в этой области продолжанпся. В основном онн направлены на поиск мсуодов более компакпюго представления временньпс автоматов н разработку более эффективных алгоритмов проаврки их свойств. глава тг Но временные автоматм — это тслыго одни из формализмов, разработанных для моделирования поведения и верификации систем реального времени. Разработано большое число формализмов для анализа подобных систем [70]. Другие формализмы из этого класса: временные сети Петри (Т(шеб Регп' Нем) [15], временная алгебра процессов (Т!шы] Ргосезз А18еЬга) [13 Ц н др.
Операция параллельной композиции временных автоматов также может быть определена по-разному. Здесь используется, фактически, операция параллельной композиции из исчисления ССБ Р. Милнера, которая принята в языках модер «Орраа] и К Техника, при которой пространство состояний графа регионов не строится для верификации, а вместо этого множество сссгояний этого графа предстввлвегся неявно, символически, с помощью манипуляций множествами неравенств, наложенных на значения локальных часов, была предложена в [7Ц. Временные зоны показаны в работе [8]. Логика ТСП. (Т!пмд Сошрнгайопа( Тгее Сей!с) предложена в 199! г. Алуром как расширение СТ1, В работе [70] был исследован вопрос использования логики ТОТИ для верификации систем реального времени.
Разрешимость верификации временных автоматов относительно формул ТСТ!. была показана в [2] и [3]. В работе [152] описывается опыт авторов по использованию символьного подхода к реализации системы анализа свойств реального времени в рамках подхода "проверка модели". Протокол РОП1, модель которого представлена в форме временного автомата, описан в [8Ц. Описания систем верификации Урраа! н Кюпоз можно найти в первом томе журнала )опгпа! оп бойттаге Тоо!з (ог Тесйпо1ойу Тпюзгег за 1997 г. ([102], [153]). Разнсстные решающие диаграммы, проблемы, возникающие при нх шхтроении, и их применение для проверки некоторых свойств систем реального времени описаны в [1! Ц. Подробное и четкое изложение принципов верификации длл систем реального времени дано в [19]. 12.18. Задачи к главе 12 12.1. Постройте граф регионов для временного автомата с тремя локацнями и одним таймером с потолком 3.
12.2. Постройте структуру регионов с двумя часами х и у, ограниченными константами С„=2 и Сх = 3. ИВ. Пострпйте траекторию изменения значений таймеров х и у при выполнении некоторой последовательности шагов лля графа. регионов лэ (ем. Рис. 12.13).
12ий Пусть во временном автомате разрешено действие х: у — присаанва.- ине значений одного таймера другому таймеру. Покамите на структуре регионов дая двух часов, как зто прнсааиаание изменяет регидн, в котором находится граф репюнов. 12.5. Для временного автомата, показанного на рис. 12.29, постройте граф регионов. Проверьте, выполняется лн в этом автомате формула АР(а, л х 1) логики СТ1.. Рис.
12.29 12.6. Проверьте, выполняется лн формула Ф = ЕРк,л для временного автомата А, прелставлеиного на рнс. 12.30. Рис. 1239 о Улвхннив Замените формулу Ф логики ТСТЕ на формулу ЕР((х и1) лл) логики СП. и постройте граф регионов для автомата А Ф х. 12.7. Обзвоните по рис. 1223, почему протокол Фишера корректен. 12.3. Дайте формальное определение зон нв рис. 12.23. (тмее 12 22.Р, Достройте граф зон прстокока Фищера (рис.
12.26). 12.1й. Постройте канонические матрицы разноевй границ кка скщ(у(ощих Зои: 2,=2йу<5луйхлх-2йу '2т=х-у<2луй2лх<1 В~ н( п1 Д( К( О п( ч( п1 О р( Б т( с( ф ф Щ к( ю (1 т( Заключение Встроенные программно-аппаратные снсшмы, на проверку которых в основном направлены опнсанные в монографии подходы, попользуются в областях применений, критических с точки зрения безопясностн: меднцннсксе оборудованне, системы уоравлення в автомобилях, бортовое оборудованне спугннков, авнацнонной, кссмнческой н военной техники, мобильные системы. Ошибки в таяня системах прннатня решений могут иметь катастрофнческне последствия. Многочнсленнью примеры последствий ошнбок автоматнческнх снстем принятия решений, от "дружественного огня" в военных действнях до ошибок в снстемах управлення космическими аппаратами, показывают необходнмость повышения уровня надежностн разрабатываемых программных н аппаратных сметем.
Обеспеченне правнльного функцноннровання таких систем является вюкнейшей проблемой прн нх разработке. Основным средством поаышення ншгшкностн таких систем авляеюя нх аернфнкацня. Еще несколько лет нюад еернфнквцня бмла искусством, логическим дедуктнвным рассуяошннем, требоаавшнм значительного времени — многих месяцев работы квалнфнцнрованных спецналнстов для проверки правнльностн функцноннровання дюкс небольших программ. Представленный в монографнн метод шага сдесйлй превратил верификацию программных н аппаратных систем нз нскусспш, которым были первые шаги дедуктивной вернфнкацнн, в пронзводственную технслогню, которая дсстнгла высокой степени автоматизации, факгнческн, уровня "накатка кнопки".
Описанные в этой книге методы вернфнкацнн днскрстных сметем, обьеднненные под общим нвзваннем тоде! с!зес!г!пй, с успехоы прнменяются как для вернфнкацнн программнмх н аппаратных снстем, так н во многих других областях. Многие основные компании по разработке ПО н аппаратуры в настоящее время ннтенснвно нспользуюг верификацию на основе пюре! сйес!и!и!р Использшанне вернфнкашш для проектов в фнрмах-рвзработчнках программных систем привело к многократному уменьшению ошибок в их продукпщ, сокращению времени выведения продуктов на рынок, снижению их стоимости. повышению производительности при их разработке.
Изложенные в тексте алгоритмы позволяют полностью автоматизировать процесс верификации, хотя и требуют от разработчика достаточно высокой квалификации при построении модели провервемой системы, прн формулировке проверяемых свойств на взыке темпоральной логики, а также при интерпретации результатов верификации. Хотя представленный в монографии материал лишь в незначительной степени покрывает те элегантные теоретические результаты, а также эффективные технические приемы и алгоритмм, которые получены к настоящему времени в области верификации методом щобе! сйесЫпй, автор надеется, что ему удалось показать, как формальные методы можно продуктивно использовать в анализе программных систем анавогичио тому, как формальные методы и математика в целом используются в июкенерном деле.
И здесь и таи разрабатываются символические модели существенных свойств обьекгов н средства анализа этих моделей. В строительстве используется сопротивление матерналов, в авиастроении — аэродинамика, в электроэнергетике строятся модели генеркгоров н линий передач. Зтн разделы прикладной математики црниеняются июкенерами-разработчиками дпя построения систем с гарантированным выполнением пми требуемых функций. Поскольку программные снсгемы щцают специфические динамические процессы, инженеры-разработчики программных средств должны уметь строить модели дискретных систем, использовать формальную логику дпя спецификации свойств поведения таких систем и разрабатывать алгоритмы для проверки выполнения этих свойств в своих разработках.
12. Т. ВаИ, Е. Вопи!пюга, ег а1. ТЬспюИЬ Бипк Апв1укв оГ Оес!се Ог/чегз П Е Буз 2006. 13. Р. Воиуег, Р. СЬегаИег, Н. Мвйеу. Оп йе ехрюзвгеепезв оГ ТРТ1. апд МТ1 // 12ССБ, го1. 3821, 2005. 14. Ю. И. Впюв, Е М. С!юЬе, К. 1.. МсМИ1ап, ез а!. БуюЬоИс пкн1е1 сЬЕсЫп8; 10 запев апд Ьеуопд П 1и: 1ЕЕЕ Буюр: оп Глбк гп Соврав. Бс/., 1990, 1пИпюадоп апд Союригк1оп, к 98, Н2. 1992. 15. В.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
