Лабораторные работы по курсу Методы анализа и обеспечения качества ПО

Верификация параллельных программ на основе проверки моделей (SPIN)

Программа работы

  1. Получить вариант задания с описанием программы
  2. Написать на языке PROMELA модель программы
  3. Определить проверяемые свойства исходя из логики работы системы (2-3 свойства)
  4. Записать свойства в виде формул LTL/assert
  5. Выполнить верификацию в системе iSpin
  6. Модифицировать модель таким образом, чтобы одно из проверяемых свойств выполнялось / не выполнялось
  7. Проанализировать контр-пример и объяснить, почему не выполняется свойство.

Варианты заданий

  1. Три процесса обмениваются сообщениями, П1 посылает по одному сообщению 2-му и 3-му, 2-й принимает сообщение и посылает два сообщения П3 и одно П1. П3 получает одно соообщение от П1 и одно сообщение от П2 и отправляет сообщение в П1. П1 получив ответы от П2 и П3 генерирует следующее сообщение.

  2. Хэндшeйк двух процессов через сигналы ack/rdy/data, оба процесса имеют случайную задержку на генерацию/обработку данных.

  3. Установление TCP соединения.

  4. Разрыв TCP соединения.

  5. Производитель и потребитель обменивающиеся сообщениями через FIFO, каждое сообщение подтверждается через рандеву.

  6. Алгоритм взаимного исключения Питерсона для двух процессов.

  7. Алгоритм взаимного исключения Лампорта (можно для двух процессов).

  8. Доступ к разделяемой памяти защищенной мьютексом.

  9. Работа с разделяемой памятью - 1 процесс пишет, два читают, используется SeqLock (http://rus-linux.net/MyLDP/BOOKS/Moduli-yadra-Linux/06/kern-mod-06-22.html).

  10. Три обедающих философа.

  11. Система управление лифтом. Лифт вызывается с любого этажа вниз или вверх и останавливается проходя этажи с вызовом, если количество человек не превышает максимально допустимое. Сформулировать и проверить справедливость обслуживания пассажиров.

Используемые средства

Верификация программ с помощью SatAbs

Программа работы

  1. Настроить переменные окружения ($export PATH=$PATH:~/satabs)
  2. Получить из репозитория вариант задания
  3. Проанализировать программу с помощью satabs
  4. используя опции --show-claims, --claim
  5. используя подмножество опций --bounds-check, --pointer-check, --overflow-check
  6. Проинтерпретировать результаты анализа и попытаться устранить ошибку, если она истинная.

Варианты заданий

  1. 01
  2. 02
  3. 03
  4. 04
  5. 05
  6. 06
  7. 07
  8. 08

Используемые средства