И.В. Шошмина, Ю.Г. Карпов - Введение в язык Promela и систему комплексной верификации Spin (1161239), страница 3
Текст из файла (страница 3)
Именно эту технику Spinиспользует при верификации. Отметим, например, что большинство ошибок, выявленных спомощью Spin при верификации бортовой системы управления космического аппарата DeepSpace 1, были ошибками, допущенными разработчиками этой системы в силунепредвиденных взаимодействий и перекрытий выполнений параллельных процессов.1.1.Графическая оболочка XSpin и модель “Hello world”Программное средство Spin можно использовать в командной строке, указывая различныеключи. Однако мы рекомендуем воспользоваться графической оболочкой XSpin.
ЗапуститеXSpin (установка и запуск программы XSpin описаны в Приложении 1 “Установка инастройка системы Spin c GUI XSpin”).7Основное окноИстория командОсновное окно XSpin является простым текстовым редактором. В меню Edit доступныобычные опции для работы с текстом: Copy, Cut, Paste. С помощью меню View можноизменять размеры шрифта в основном окне. Под основным окном находится окно с историейкоманд (command-log). В дальнейшем все выполняемые команды будут отображаться вокне команд.Рассмотрим пример простейшей программы на языке Promela. Наиболее частовстречающимся первым примером в руководствах по языкам программирования являетсяпрограмма, которая печатает строку hello world на терминал пользователя.
Традицияначалась с руководства для языка программирования С (1978), авторами которого былиКерниган и Ритчи. С тех пор этот пример кочует по руководствам языков программирования.Специфицируем эту маленькую программу как модель на языке Promela:active proctype example(){printf("MSC: hello world\n")}Модели на Promela используются для описания поведения систем потенциальновзаимодействующих процессов, т.е.
нескольких асинхронно выполняемых потоков. Поэтомупервичная единица выполнения в Spin – это процесс. В отличие от C, здесь нет основнойпроцедуры main. Служебное слово proctype описывает в этом примере новый типпроцессов с названием example. Префикс active говорит о том, что один экземплярпроцесса типа example должен быть создан сразу в начале работы модели. Если префиксопущен, то экземпляр процесса не будет создан при таком объявлении. Созданиеэкземпляров процессов, объявленных с помощью служебного слова proctype, можетбыть выполнено другими средствами.Введем текст модели в основное окно XSpin. Сохраним модель в файле hello при помощименю File. Можно воспользоваться и другим текстовым редактором, обновляя файл спомощью опции ReOpen в меню File XSpin.Для того чтобы проверить синтаксические ошибки в файле с моделью на Promela, выберите вменю Run пункт Run Syntax Check.
В нашем файле hello синтаксических ошибок нет, и вкомандном окне выведется сообщение “no syntax errors”.8Spin может продемонстрировать один из возможных вариантов поведения модели – такойрежим работы Spin называется симуляцией (пункт (Re)Run Simulation меню Run).До запуска симуляции необходимо проверить параметры этого режима (пункт Set SimulationParameters меню Run).В окне параметров симуляции на панели режима отображения (Display Mode) задаются окна,которые необходимо выводить при симуляции – панель диаграммы взаимодействия MSCPanel, режим вывода событий отдельных процессов Time Sequence Panel, панель дляпросмотра значений данных Data Values Panel и панель выполненных шагов моделиExecution Bar Panel (о параметрах симуляции см.
Приложение 1).В нашей первой модели присутствует вывод на панель диаграммы взаимодействия, о чемсвидетельствует синтаксис оператора printfprintf("MSC: ")поэтому необходимо установить флаг MSC Panel.На панели Simulation Style устанавливается тип симуляции. Возможны три вида симуляции:случайная Random – все недетерминированные решения определяются случайным образом,управляемая Guided, интерактивная Interactive – все недетерминированные решениязапрашиваются у пользователя в интерактивном режиме. Установим случайный типсимуляции Random simulation.
Запустим модель на симуляцию, нажав кнопку Start.9При симуляции Spin найдет некоторое возможное вычисление модели. В окне выводасимуляции (Simulation Output) отображаются все события модели, произошедшие во времяэтого конкретного вычисления. Нажмите Run, запустив тем самым режим симуляции.
Вданном конкретном примере на шаге 1 был выполнен оператор printf.Вывод в главном окне симуляции является исчерпывающим, в том смысле, что по немуможно точно установить всю последовательность событий конкретного вычисления. Однакоформат представления не удобен для пользователя.Второе окно, открывшееся при запуске панель диаграммы взаимодействия, Sequence Chart,наглядно демонстрирует результат симуляции нашего первого примера. Единственныйпроцесс типа example с идентификатором 0 вывел сообщение hello world.1.2.Типы объектов языка PromelaПрограмма, написанная на Promela, состоит из трех основных типов объектов: процессы(processes), каналы сообщений (message channels) и переменные (data objects). Процессызадают поведение, каналы и глобальные переменные определяют окружение, в которомвыполняются процессы.Типы процессовТипы процессов описываются при помощи объявления proctype.
Для разумногоиспользования модели на Promela должно быть хотя бы одно объявление типа процесса ихотя бы один экземпляр процесса какого-нибудь типа. Процессы всегда объявляютсяглобально.Существует несколько способов создания экземпляров типа процесса. В приведенном нижепримере создается 2 экземпляра типа процесса you_run с помощью префикса active:active [2] proctype you_run(){printf("MSC: my pid is: %d\n", _pid)}Каждый запущенный процесс имеет уникальный идентификатор, значение которогонеотрицательно.
Идентификатор процесса хранится в зарезервированной локальнойпеременной _pid.10Тело процесса может состоять из объявлений данных и операторов, оно может быть ипустым. Состояние переменной или канала сообщений изменяется или проверяется только впроцессах. Точка с запятой является разделителем операторов в теле процесса (но неуказателем конца оператора, поэтому после последнего оператора точка с запятой можетотсутствовать). Лишние точки с запятой не являются ошибкой, поскольку в Promelaдопускается пустой оператор.В программах на Promela существует два различных разделителя операторов: стрелка “->” иточка с запятой “;”.
Эти два разделителя эквивалентны. Стрелка иногда используется какнеформальный способ указания на причинно-следственное отношение между двумяоператорами: если предыдущий оператор выполняется, то управление передается навыполнение второго оператора (что, собственно, соответствует и семантике точки с запятой).В главном окне симуляции отобразится информация о том, что было создано два процессатипа you_run.На шаге 1 процесс с идентификатором 0 выполнил оператор printf, на шаге два процесс сидентификатором 1 выполнил оператор printf, после чего оба процесса завершили работу.Поскольку процессы асинхронны, то очевидно, что последовательность выполненияоператоров printf могла бы быть противоположной. На панели диаграммы взаимодействий(Sequence Chart) каждый столбец отображает один запущенный процесс.Процесс также можно запустить, воспользовавшись оператором run.proctype you_run(byte x){printf("MSC: x is %d\n", x);printf("MSC: my pid is = %d\n", _pid)}init {run you_run(0);run you_run(1)}11В этом примере процесс init запускает два процесса типа you_run и передает каждому изних входной параметр.
Все запущенные процессы работают параллельно. Процесс init –базовый процесс в Promela, который всегда активируется в начальном состоянии модели.Процессу init нельзя передать параметры или создать его копию. Если он есть в модели, тоего идентификатор всегда равен 0.Данное решение имеет недостаток, связанный с созданием лишнего процесса (процессаinit), что увеличивает размер модели.
Размер модели не влияет на режим симуляции, ноотражается на времени верификации.Операторы run используются в любых процессах для того, чтобы породить новый экземплярпроцесса заданного типа, т.е. он может встретиться не только в процессе init.Выполняющийся процесс завершается, когда достигает конца тела описания своего типапроцесса, но не позже своего процесса-родителя. Количество процессов, которое может бытьсоздано в Spin ограничено числом 255.Типы данныхТипы данных Promela близки к данным языка C (см.
табл. 1) .Табл. 1. Типы данных и диапазоны значений для компьютера с длиной слова 32 бит.Тип данныхbitboolbytechanmtypepidshortintunsignedДиапазон0,1false,true0..2551..2551..2550..255–215 .. 215 – 1–231 .. 231 – 10 .. 232 – 1ПояснениеЧисло каналовЧисло значений перечислимого типаЧисло возможных процессовВ Promela существует два уровня доступа к объектам: локальный и глобальный. Объект,объявленный глобально, будет доступен всем процессам.Используются ли переменные для хранения глобальной информации о системе в целом, илиинформации, касающейся конкретного процесса, зависит от того, где помещается объявлениепеременной. Переменная является глобальной, если она объявлена вне описания процесса, и12локальной, если она объявлена в описании процесса.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
