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

Процессно-ориентированное программирование - перспективный подход к разработке управляющего программного обеспечения. Управляющее программное обеспечение часто требует высокой надежности. Формальные методы верификации, в частности дедуктивная верификация, используются для доказательства правильности таких программ относительно требований. Ранее был разработан язык темпоральных требований чтобы специфицировать темпоральные требования для дедуктивной верификации процесс-ориентированных программ. Было также показано, что значительная часть требований относится к небольшому числу классов. Для этих классов были разработаны шаблоны требований. В данной статье мы представляем коллекцию процесс-ориентированных программ и требований к ним. Требования формализованы на языке темпоральных требований и классифицированы в соответствии с набором шаблонов. Мы также определяем новый шаблон требований. Эти результаты могут быть использованы при исследовании формальных методов верификации процесс-ориентированных программ, в частности, при исследовании методов доказательства условий корректности.