Методика построения событийно-управляемых программных систем с использованием языка спецификации CIAO

Событийно-управляемые программные системы в научной литературе относят к классу систем со сложным поведением, называемых реагирующими системами (reactive systems), то есть систем, которые на одно и то же входное воздействие реагируют по-разному в зависимости от своего состояния и предыстории. Такие системы удобно описывать с помощью автоматных моделей с использованием специальных языковых средств – как графических, так и текстовых. Представлена методика автоматизированного построения систем со сложным поведением с использованием разработанного авторами языка CIAO (Cooperative Interaction of Automata Objects), который позволяет на основе неформального описания реагирующей системы формально специфицировать требуемое поведение. Описание реагирующей системы может быть задано словесно на естественном языке или иным способом, принятым в конкретной предметной области. Далее по этой спецификации на языке CIAO специальным преобразователем генерируется программная система взаимодействующих автоматов на языке программирования С++. Сгенерированная программа реализует поведение, гарантированно соответствующее заданной спецификации и исходному неформальному описанию. Для языка CIAO предусмотрена как графическая, так и текстовая нотация. Графическая нотация основана на расширенной нотации диаграмм автомата и диаграмм компонентов унифицированного языка моделирования UML, которые хорошо зарекомендовали себя в описании поведения управляемых событиями систем. Текстовый синтаксис языка CIAO описан контекстно-свободной грамматикой в регулярной форме. Автоматически генерируемый код на языке С++ допускает использование как библиотечных, так и любых внешних функций, написанных вручную. При этом доказательное соответствие формальной спецификации и сгенерированного кода сохраняется при условии соответствия внешних функций своим спецификациям. В качестве примера предложено оригинальное решение задачи Д. Кнута о реагирующей системе управления лифтом. Продемонстрирована действенность предлагаемой методики, поскольку сам автомат-преобразователь, генерирующий код на С++, представлен как реагирующая система, специфицирован на языке CIAO и реализован методом раскрутки. Проведено сравнение предлагаемой методики с другими известными формальными методами описания систем со сложным поведением.