2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 48
Текст из файла (страница 48)
Именно зто пр(меряется здесь оператором ащесс. (т */ 4/ 7.4. Заключвние Приведенные в этой паве примеры показывают, квк некио в инструментальной системе Зрй верифнцировать параллельные программы и протоколы. Этот инструмент, как и многие другие, реалиэующ(м алгорипны верификации на основе техники шобе! сйссйпй, был использован лля верифнкещш нножества систем для критических применений значительной сложности и доказал сжио эффекгнвнос)ь. Существует несколько проблем, с которыми сталкивал)сл любой профессионал, выполняющий верификацшо с помощью )ехники проверки модели.
Перечислим основные нз ннк. (З Кюклая система автоматической верификации (Зрш, БМ4/, Рй)ЕМ н лр.) имеет свой собственный язык описания поведению верифнцнруемых снс- Гавел г тем. Построение адекватной модели на входном юыке инструмента верификации требует квалификации, искуссша и опьпх, Справедливо следую. щее утверждение; "йерификаюш стюшамы ла основе мепюда лрсееряи модели нояезял яасшагьяс:, ялсяаяько адекватна лострагняая для анализе модель свсмгмм".
Часто очень непросто дать гарипню того, что постро. енная модель лействишльно адекватна, что она корректно представляет анализируемую систему. С) То же относшся и к спецификации требований. Кшкдмй инструмент верификации имеет евою собственную нотацшо для записи проверяемых свойств. Обычно эта нотация предсгавляст собой взык для построения формул некоторого подмножеспн темпоральных логик С'П., СТЬ» или Е'П.. Свойства систем, коюрые желательно проверить, не всегда возможно выразить в этой нотации. Вырвкение многих свойств также требует достаточно высокой квалификации и опыта. О Очень часто число состояний анализируемых моделей слишком велико, н результатом запуска инструмента верификации может быть его останов из.за нехватки памяти. В этом случае лля верификации системы необходима дополнительная работа по ее абстрагированию, отбрасыванию второстепенных деталей, ограничению числа параметров илн области принимаемых ими значений.
В сложных случаях может оказаться необходимым уменьшить число верифицируемых модулей, илн проводки верификацию модулей независимо. ГУ Если при верификации найдена ошибка н выдан кшпрпрнмер, то часто нелегко установшь причину ошибки: выдаваемые трассы могут окюаться очень ллиннымн и слшкными, их анализ может потребснать глубокого проникновения в существо проверяемых алгоритмов. Иногла причиной ошибки может явитьсв именно ограниченность модели, а вовсе не некорректность верифицируемой системы. 7.5. Замечания Система верификации брш для верификации протоколов передачи данных стала использоваться с начала 90-х годов прошлого века С тех лор с помощью этой сисшмм были проверены многие промышленные разработки для критических применений, в частности, модули бортовой снстемы управления Веер брасе 1.
Многие уннверситепя используют бр)п в учебном процессе ие только в курсах верификации, но и в курсах, изучающих параллельные и распределенные влгорнгмы для мсцедироввннв и наглядного представления взвнмолействующнх процяссок 7.6. 7.1. Г ключ гзы итн Спеш а) Без б) Жи О( т~, п~ на язы ьеоз ьюе асште »»»»гс »саге: г с ( и г е~ г. У > г~е г ~ вери- МД!НО- ни мочаяпза являет нт веаемых сенин е или эможмбуст зко.
н таков обхо! Вто- рининмым виню часто аться экого (иной екор- нных : по. н для ения дво- ение 7.В. Задачи к главв У 7.1. Проверьте коррекпюсгь другой формулировки, п[ютокола вюимпого (ю- ключаиия Пеюрсона: Г1:: во: ПС1г в1: у1: ~пм! з2 Ф С 3 Ге1еез вэ: не!с ( у2оз!г вз; С31! вэ: у1: Гз1зег вю досо воз пы у2: Свм! п2: С: сваг пз; за11 (-~у1ч с(! паг СВ2г пэ: у2 : гессен пб: сосо пег г Спецификация этой программы: а) Беэопасность (вэаимное исключение всегда выполюмтса)! П (Р[фтсп Р2®п4) б) Живость (прогресс процессов): сз(Р[флйвз РРУЩю4) С(Р2фиЗ ю ТР2фле) 7.2. Проверьте корректность алгоритма ювимного искюочения, папнсанноуо на аэыке Ргоюе[а: поо1 сшп, 21зд[2!! пухе псс1с! пес[те рсоссуре[2! пзег(! ( зззесс ( рпа О (( рьа ч 1 1! зсахс: Саад[ р[а ! - Ю Пвв рха! гя[зд и- ры1 о (! сохо 1 — рса[! поз[Сея! зззесс Оюс1С 1(! / ох111оа1 зеос1оп '/ остях — г 11зд ! рЫ 1 Ог досо зсзхсз рляяе г гл 7.4.
Проверьте коррекпюсть епю олной формулировки протокола взаимного исключения Петерсомк Под~ для ~ лы.. витс в кю ных лози Ггссеез1г: Ггавг Г-1Г С:-ОГ евхга ггзасо впа опъ ог ееясг С ШОК1весгзосп1г Г1а91 :-Ог Ггосеяес: ~ Гзесс:-Ы С ъ г-зг ьи 1пе91 ° и ссгп - Ц еяег С зезсвзве 1 Ог яз зо:-ог Про[ помс ких ~ сова| КОТО) лить тиже Каха бой ~ доку зволг му г телы Бизн раба.
ми в 7З. Алгоригм взаимного исключения с нвзввююм ТПске64е, приведенный в П04[, опнсыввстсв тмс 'Разделяемая переменная содержит пару сквлярою <гмп, йгаигсг[з, кмкаый из которых принимает значения [1,2, ..., иК Вначале се значение <1, 1>. Компонент асхг этой переменной представляет собой следующий "пропуск" в критическую секцию, компонент йгаигеФ вЂ” это последний выданный "пропуск" в критическую секцию. Когда процесс хочет войти в свао критическую секцию, он "берет пропуск", т. е.
копирует себе компонент лехг разделяемой переменной н увеличивает его по модулю л. Когда номер процесса равен значению компонента йтанмг7, процесс входит в крнгнческую секцию. Когда про. месс выходит из критичеакой секции, он увеличивает значение компонента йпзигсгг по молулю л". Проверьте корректность этого алгоритма. лаев 7 енный ГЛАВА 8 нного ~ый из омно. е криауск" о секзй Ре гначез про- нента Применения апгоритма гпобе! сйесйпц Подход к верификации иа основе метода мсгмг' сдесвглй состоит в том, чю лля модели системы формально проверяется выполнение логической формулы. Полученные в области верификации фуцдаментвльные результаты удивительным обрюом оказались востребованы в огромном числе приложений, в которых идеи воде! сйескгпй применяются шж решения смеых разнообразных задач. В данном рюделе мы рассмотрим только некоторые нз этих приложений.
8Л. Анализ бизнес-процессов Проблема формального анализа требуемых от бивне-ппроцессо свойств с помощью метода пнмЫ сйесЫпй явилась предметом исследования нескольких научных групп. Компания а этих исследованиях рассматривается не как совокупность отделов и групп, а как мншкество бизнес-процессов, вокруг которых реалнзуетса деятельность коыпаимм. Бизнес-процесс можно определить как набор связанных операций, выполнение которых направлено на достижение целей компании.
Кмкаая компания создаетю для выполнения некоторых целей, поэтому в любой компании существуют бизнес-процессы, шоке если они не описаны и ие локументироааны. Внедрение формального описания бизнес-процесса позволяет построить системы управления качеством компании, решить проблему построения эффективной структуры управления, оптимизировать деятельность на основе ключевых показателей. Бизнес-процесс — это не обязательно последовательность действий одного работника.
Бизнес-процесс макет реализовываться несколькимн рабогннкамн в пределах одного подразделения компании, охватывать несколько ес Гпееа 3 подрвзделений нлн дюкс несколько нодраэлвлений различных компаний. Поэтому бизнес-процессы цредставляются как параллельно протекжощие активности многих исполнителей, последовательно выполняющих свои функции. Здесь возникшот известные в параллельном щюграммировании проблемы доступа к ресурсам, блокировки, ограниченна живости, и поэтому результаты и решения в области верификации параелельных цроцсссов востребованы и в области бизнес-процессов. Приведем один нз примеров исследования в этой области.
Наличие большого числа взаимодействующих бизнес-нроцессов ставит задачу формальной проверки нх правильности, что молит быть выполнено методом пюре( сйсс(г)пб Однако бизнес-иронессы слецифицируются менеджерами, которые не имеют подготовки в области формальных моделей н информатики, а для формального анализа бизнес-процессов необходимо детальное представление модели пронесса на формальном азыке, которое трудно построить и которое нелегко понять менеджерам. Для разрешения этой проблемы авторы работы (ЗЗ) нредлм вют иснользовать для спецификации бизнес-процессов простой графический формализи, который близок графическому изобрюкению параллельных жггнвностей картами состояний (звцесйагш) Харела и сетями Петри, а также диаграммами активностей языка ((М(. (ба.
асбюгу б(айцвиз). Транслятор с этого языка в язык Ргоше!а — входной юык системы верификации Бр|а — позволяет проверить свойства бизнес-процессов. Предлагаемый авторами графический шык, названный АшЬег (Аюй(магога( Мобе(йлй Вох рог Евгегрпш дезгйп), позволяет представить бизнес-процессы, агенты, участвующие в процессах, и данные, с которыми процессы оперируют. Поведение структурировано в виде процессов, взаимодействующих с помощью синхронной коммуниющин (хэндшейка). Свойства процессов соецнфнцируются с помощью формул Ь'П, Авторы разработали формы, позволяющие упростить такую снецификацию, поскольку формулы логики ЕТ(., но нх мнению, также явлмотгл слишком сложными дла использования менеджерами. Язын Апйш позволяет выразить действия, которые выполняются в бизнеспроцессах, н отношения межлу этими действиями.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
