Using NuSMV to check a model of a semaphore
- Семафор
Имеется 5 процессов, желающих получить доступ к общей памяти.
Необходимо создать модель семафора и 5 процессов.
Проверяемые свойства:
-
При инициализации семафора значением 1 убедиться, что в критической секции не может быть больше одного процесса
-
Убедиться, что каждый процесс в конце концов получит доступ к критической секции
-
При инициализации семафора значением 3 убедиться, что в критической секции может быть 1, 2 или 3 процесса
-
При инициализации семафора значением 3 убедиться, что в критической секции не может быть 4 процесса