Верификация программ с помощью языка Promela
|
Скачать 65.02 Kb.
|
| Верификация программ с помощью языка Promela Программное средство комплексной верификации spin, разработанное в исследовательском центре Bell Labs, применяется для формального анализа свойств разрабатываемых протоколов и программных систем. Пакет Spin позволяет строить модели параллельных программ и широкого класса дискретных систем, выражать требуемые свойства их поведения на языке линейной временной (”темпоральной”) логики LTL, автоматически проверить выполнение темпоральных свойств систем на их моделях. Аббревиатура Spin расшифровывается как Simple Promela Interpreter – простой интерпретатор программ на языке Promela. 1 Ссылки и установка Домашняя страница spin: http://spinroot.com/. На этой странице можно найти ссылки на руководства по системе, ссылки на труды ежегодных конференций по этому продукту. Наиболее полным описанием системы Spin является монография Gerard J. Holzmann. The Spin Model checker (основные главы доступны в сети). На русском языке есть неплохое руководство на http://dcn.infos.ru/~karpov/Model%20Checking%20Verification/Course%20Work/SPIN%20Manual.pdf Установка spin: 1) Установить ActiveTCL Скачать с http://www.softtime.ru/cpp_info/dev_cpp.php компилятор. 3) После установки компилятора в его папку bin скинуть файлы xspin.tcl, spin.exe . 4) Запустить xspin Более подробно, в следующей пошаговой инструкции по установке комплекса верификации Spin на персональный компьютер, работающий под управлением операционной системы Windows. Установка и настройка системы Spin c GUI XSpin Домашняя страничка Spin – www.spinroot.com. На этой странице присутствует описание как самой системы, так и рекомендации по её установке. На данном сайте можно, в том числе, скачать последнюю версию пакета Spin. Там она лежит в виде пакета с именем типа pc_spin***.zip, где *** - номер версии продукта. В описанной ниже последовательности действий, используется заранее собранный (и объединённый в один архив) комплект ПО for_spin_new.rar, необходимого для работы с системой. Описываемый способ настройки не единственный, есть и иные, для них рекомендуем обратиться к домашней странице пакета Spin. Шаг 1: Загрузка комплекта ПО. 1) Для загрузки архива, содержащего программное обеспечение, настройка которого описывается в данном руководстве, необходимо загрузить архив for_spin_new.rar. 2) Полученный файл необходимо распаковать в любой, выбранный пользователем каталог, для удобства ссылки на него в описании процесса установки назовем его LOCAL_PACKAGE_DIRECTORY. Шаг 2: Установка пакета Cygwin. Запустите на выполнение файл setup.exe, который произведёт инициализацию программного комплекса Cygwin, эмулирующего работу операционной системы UNIX в системах управляемых ОС Windows. (В описываемом примере – Microsoft Windows XP SP 1 build 2600.) Опишем последовательность действий, возникающих при ответах на вопросы, задаваемые в возникающих диалоговых окнах при установке Cygwin. 1) В диалоговом окне Cygwin Setup следует нажать кнопку Далее. 2) В окне Cygwin Setup – Chose Installation Type выбрать вариант Install from Local Directory. 3) Создать домашний каталог для Cygwin (рекомендовано, с:/cygwin). Назовем этот каталог условно CYGWIN_HOME_DIRECTORY. 4) В окне Cygwin Setup – Chose Installation Directory нужно указать каталог, в который будет произведена установка Cygwin, а также переставить значение кодировки текста по умолчанию в положение DOS/text. 5) В окне Cygwin Setup – Select Local Package Directory при помощи кнопки Browse следует указать путь к локальному каталогу LOCAL_PACKAGE_DIRECTORY/cygwin_distr_download, где хранится архив Cygwin. 6) setup сам сформирует сценарий установки и по завершению этого процесса перейдёт к следующему шагу. 7) Окно Cygwin Setup – Select Packages демонстрирует структурированный список компонент, установка которых будет произведена после подтверждения корректности выбранных модулей.  8) Следует открыть пункт Devel и путём переключения пунктов списка, содержащихся под надписью Skip, добиться того, что бы все файлы содержащиеся в этом разделе были выбраны для установки. В конечном итоге, список установки должен выглядеть следующим образом, то есть, все компоненты группы Devel, из представленных в архиве, должны быть выбраны для установки.  9) Далее система производит копирование модулей и настройку конфигур файлов. Эти операции сценарием и вмешательст 10) Установка завершается созданием ярлыков для установленной программы. Шаг 3: Установка пакета Spin. 1) Создайте в каталоге CYGWIN_HOME_DIRECT домашний каталог пакета Spin SPIN_HOME_DIRECTORY. Если ранее был выбран рекомендованный каталог CYGWIN_HOME_DIRECTORY, то полный адрес папки пакета Spin будет c:/cygwin/bin/ 2) Разархивируйте в папку SPIN_HOME_DIRECTORY (например, c:/cygwin/b LOCAL_PACKAGE_DIRECTORY. 3) В каталоге SPIN_HOME_DIRECTORY xspin.tcl. 4) Откройте файл xspin.tcl в текстовом редакторе, поддерживающем перенос строк в текстовых файлах, например, WordPad. 5) Измените путь, указанный в начале файла, на актуальный SPIN_HOME_DIRECTORY/xspin.tcl (с:/cygwin/bin/spin/xspin.tcl). Обратите внимание полный путь к файлу вместе с расширением .tcl. Строка в результате будет выглядеть подобным образом exec wish c:/cygwin/bin/spin/xspin.tcl -- $* 6) Найдите строку, где указан путь к интерпретатору Spin. Установите полный путь к исполняемом случае выбора названий каталогов по set SPIN "c:/cygwin/bin/spin/spin.exe"; # use a full path-name if necessary 7) Сохраните файл. Закройте редактор. 8) Замените би доступна для загрузки с сайта spinroot. for_spin_new.rar (в LOCAL_PACKAGE_DIRECTORY). Размеры этих библиотек отличаются. Шаг 4: Первый запуск программы Cygwin и Spin. Осуществить первый запуск програм расположенного на рабочем столе, либо напрямую – запуском .bat файла. Во время первого старта, Сygwin создаст конфигурационные файлы и, по завершению данной операции, выдаст приглашение на ввод команд $.  После этого откроется окно системы Spin. Обратите внимание на то, что бы в окне сообщений программы не было упоминания об ошибках.  На этом установка пакета Spin завершена. 2. Работа со spin. Общие положения С помощью системы Spin выполняется проверка не самих программ, а их моделей. Для построения модели по исходной параллельной программе или алгоритму пользователь (обычно вручную) строит представление этой программы на С-подобном входном языке пакета Spin, названном автором Promela (Protocol Meta Language). Это представление –программу на языке Promela можно считать моделью верифицируемой программы. Конструкции языка Promela просты, они имеют ясную и четкую семантику, позволяющую перевести (оттранслировать) любую программу на этом языке в систему переходов с конечным числом состояний, которая представляет собой модель переходов подлежащей верификации параллельной программы или алгоритма.. Spin может использоваться в двух режимах – как симулятор и как верификатор. При симуляции Spin выводит информацию об одной конкретной траектории выполнения построенной модели - графическое представление поведения в виде Диаграмм Последовательностей Сообщений (Message Sequence Diagrams), возникающих при функционировании параллельных процессов по данной траектории. Графический интерфейс пользователя XSpin визуализирует запуски симуляций и упрощает процесс отладки модели. Для доказательства свойств модели используется верификация – другой режим работы Spin. Верификатор пытается найти контрпример - неправильную, ошибочную траекторию поведения, опровергающую заданное пользователем свойство, анализируя все возможные поведения модели. Для этого он строит сложную конструкцию – синхронное произведение модели переходов анализируемой системы и автомата Бюхи, задающего все возможные некорректные поведения. В случае нахождения контрпримера симулятор Spin демонстрирует его пользователю в управляемом режиме симуляции. Таким образом, симуляция и верификация в Spin тесно связаны. Разработанные на языке Promela модели отличаются от верифицируемых программ, обычно написанных на языках программирования высокого уровня, например, Java или C. Программы на Promela не имеют классов, они представляют плоскую структуру взаимодействующих параллельных процессов, имеют минимум управляющих конструкций. все переменные имеют конечные области определения. Поэтому такую программу можно считать моделью анализируемой системы они представляют абстракцию системы, в которой пользователь должен отразить те аспекты и характеристики реальной проверяемой системы, которые значимы для заданных для верификации свойств. Построенная модель может содержать траектории, которые не относятся к реализации проверяемой системы в исходном языке программирования. Например, такие траектории могут включать явную спецификацию возможных ситуаций при наихудшем поведении среды, в модели может явно или неявно указываться спецификация свойств справедливости. Описание проверяемой системы на языке Promela должно сохранять существенные свойства этой системы. Можно сказать, что качество результата проверки моделей программ, представленных на Promela, полностью зависит от степени адекватности построенной модели. Верифицируемая модель может строиться на этапе начальной разработки структуры системы (при создании прототипа). Окончательная же система, как правило, отличается существенной детализацией: произвольными объемами буферов, наличием вещественных переменных, более богатым спектром управляющих конструкций, динамическим порождением произвольного числа процессов и т.п. |
Похожие:
 |
Программа дисциплины для направления/ специальности подготовки бакалавра/... Программа предназначена для преподавателей, ведущих данную дисциплину, учебных ассистентов и студентов направления подготовки 09.... |
|
Особенности употребления артикля в современном английском языке Говорящий обычно понимает, что он хочет сказать. Правильно донести эту информацию до слушателей – вот цель родного или иностранного... |
|
Современные способы изучения английского языка Исследовательская работа гум I Тема нашей исследовательской работы: Современные способы изучения английского языка обусловлена необходимостью применения новых информационных... |
|
Краткое содержание дисциплины Изучение основ и терминологии низкоуровнего программирования и объектно-ориентированного программирования. Изучение возможностей... |
|
Программа позволяет научиться создавать собственные презентации с... Общеразвивающая программа объединения «Инфознайка» написана на основе опыта работы в данном направлении деятельности с учетом современных... |
|
Учебно-методическое пособие по английскому языку для студентов первого... Введение. Своеобразие английского языка. Его роль в современном мире как языка международного и межкультурного общения |
|
Проблемная технология на уроках английского языка в 9 классе Автор: Закирова Татьяна Валерьевна Маоу «сош №7 с углубленным изучением английского языка» г. Перми, учитель английского языка высшей квалификационной категории |
 |
6 общая характеристика языка и пример программы на си Благодаря гибкости, выразительности и компактности своих конструкций Си завоевал наибольшую популярность в среде профессиональных... |
|
Геологическое задание на выполнение работы по теме: «Подсчет запасов... Сбор, систематизация, верификация и анализ всего имеющегося фактического геолого-промыслового материала |
|
Повышение эффективности иноязычной подготовки в вузе с помощью ит... Охватывают основные сферы жизнедеятельности человека |
|
«Углубленное изучение английского языка» по направлению подготовки... Повышение уровня культуры образования, а также культуры общения, мышления и речи. 3 Знакомство с культурой стран изучаемого языка... |
|
V 56х Руководство оператора по обработке сети станций Для всех каналов станций должны быть внесены ачх в бд wsg с помощью программы ResponseDB. Описание работы этих программ см в Рекомендациях... |
|
Программа курса Для успешного прохождения курса слушателям необходимо выполнить задания по написанию программ на Scheme. Первое задание посвящено... |
|
Доклад о ходе реализации и оценке эффективности муниципальных Программ... Программ, представленных администраторами Программ в соответствии с Порядком разработки, реализации и оценки эффективности муниципальных... |
|
Питание от компьютера Подключите устройство к компьютеру, iPad (с помощью Apple Camera Connector) или к планшету на Android по usb. Управляйте midi-совместимыми... |
|
Программами см ниже. В файле PurR sites doc С этими последовательностями Вы будете работать в первом задании. Вам необходимо найти сигнал (набор сайтов) в полученных последовательностях... |