Формальные методы спецификации, верификации и доказательства правильности систем

Одной из важных задач проектирования систем является разработка спецификаций отдельных элементов, включая описание семантики и функциональной структуры системы, спецификацию входных и выходных данных программы. Основу формальных методов спецификаций составляет задание определенных свойств программ с помощью математических методов, которые потом доказываются. Особенность использования спецификаций состоит в определении понятий системы и установлении связей между заказчиком и проектировщиком, между проектировщиком и разработчиком, а также между разработчиком и тестировщиком. Также спецификация выступает как документация к программному коду системы.

Одним из методов разработки ПС являются UML (Unified Modeling Language) и соответствующие CASE-инструменты (Rational Rose, MS Visio, Rational Software и др.). Эти инструменты поддерживают разработку ПС на всех этапах ЖЦ (см. Приложение 1). Результатом будет представление ПС с помощью графических диаграммных элементов use case, не обладающих формальной семантикой. Это может привести к неоднозначности толкования функций системы. Проектирование в системе UML, а также в языках MSC, SDL наглядно, но в них отсутствуют средства доказательства свойств элементов системы и системы в целом.

Спецификации основываются на аппарате математической логики, способстующей описанию программы как математических объектов, содержащих формальное описание семантики на одном из формальных языков RSL, VDM, Z, В и др. Элементы системы, описанные на этих языках, требуется обрабатывать с помощью специально разработанных математических средств, обеспечивающих доказательство определенных свойств программ и правильности семантики.