Курсовой проект SPIN РАЗРАБОТКА КОНТРОЛЛЕРА СВЕТОФОРОВ И ЕГО ВЕРИФИКАЦИЯ

Пример собранного SPIN: https://drive.google.com/file/d/0BxXYlwgjDSO_NWxUdWp1WXFQWGs/view?usp=sharing

Методичка во вложении.

Выдержка из методички:

В курсовой работе ставится задача разработки

контроллера светофоров для управления проездом через перекресток. Для выполнения курсовой работы необходимо, отталкиваясь от простейшего алгоритма (раздел 7.2), построить модель работы контроллера светофоров на языке Promela для индивидуального плана проезда на рис. 7.2 и верифицировать полученную модель средствами Spin относительно свойств (раздел 7.3). В этих процессах могут быть ошибки синхронизации. Все ошибки студент должен выявить и проанализировать с помощью системы верификации Spin на основе выдаваемых системой контрпримеров, демонстрирующих те сценарии движения на перекрестке, в которых процессы управляют своими светофорами неверно. Впоследствие студент должен модифицировать алгоритм работы контроллера светофоров так, чтобы удовлетворить свойствам в разделе 7.3.