Подаётся сигнал в охранную контору, когда зафиксировано вторжение через окна, двери, нажата тревожная кнопка. После этого блокируются окна и двери, пока не приедет охрана или пока блокировку не отключат вручную.

Цели и задачи л/р: Верифицировать с использованием верификатора моделей TLC параллельную систему из лабораторной работы №1.

Для этого проделать следующие шаги.

1. Записать спецификацию системы на входном языке TLA+.

2. Сформулировать 3 свойства системы на языке TLA+.

3. Провести верификацию этих свойств в TLC. Требования к системе и системе и свойствам такие же как в лабораторной работе №1.

4. Провести сравнение методов моделирования и верификации в nuXmv, SPIN и TLC.

Требования к выполнению лабораторной работе:

1. Система и формальные записи свойств соответствует требованиям лабораторной работы.

2. Минимум 2 свойства выполняются при верификации. Если одно из свойств не выполняется, предоставить анализ ошибочной трассы и показать, что исправление ошибки ведёт к неприемлемой сложности системы.

• https://lamport.azurewebsites.net/video/videos.html

• https://lamport.azurewebsites.net/tla/summary-standalone.pdf

• https://lamport.azurewebsites.net/tla/book.html

• security.tla

• security.cfg