Определения по курсу Верификация моделей программ (1161287), страница 2

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 2)

Остальное выполняется, если егозначение не 0. Три типа объектовo Процессыo Глобальные и локальные объекты данныхo Каналы сообщенийЧисло состояний модели конечно, так как Число активных процессов конечно (256) У каждого процесса – ограниченное число операторов Диапазон типов данных ограничен Размер всех каналов сообщений ограниченНедетерминизмВыполнимость операторов: псевдооператоры skip – всегда выполним, без эффекта, эквивалент выражения (1) true = skip run – 0, если при создании процесса превышен лимит, _pid (ид.

процесса) в противномслучае assert – всегда выполним, не влияет на состояние системы, SPIN сообщает об ошибке, есливыражение в assert = 0Каналы сообщений Используются для передачи сообщений между процессами Бывают двух типов: буферизованные (асинхронные) и небуферизованные (синхронные,рандеву)Inline определения Среднее между макросом и процедурой Именованный фрагмент кода с параметрами Не функция – не возвращает значенияВсе варианты оператора IF должны быть описаны явно, иначе процесс блокируется.eval(x) – отображает значение x на константуAlternating Bit Protocol (ABP) Два процесса, отправитель и получатель К каждому процессу добавляется один бит Получатель сообщает о доставке сообщения, возвращая бит отправителю Если отправителю убедился в доставке сообщения, он посылает новое, изменяя значениебита Если значение бита не изменилось, получатель считает, что идет повтор от сообщения.

Характеристики

Список файлов лабораторной работы