Программные продукты и системы

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

 Для представления моделей технических систем авторы статьи используют язык асинхронных функциональных схем (АФС), в котором программе в качестве семантического значения сопоставляется множество вычислительных последовательностей (ВП) (путей) выполнения распределенной АФС-программы. Далее семантическое значение представляется в виде системы рекурсивных уравнений. Полученная система является удобной формой представления семантических значений программ для анализа различных свойств программ.

Для создания автоматизированных програм мных средств проверки моделей необходимы формальные методы верификации. Одним из них является метод, использующий темпоральную логику линейного времени (linear-time temporal logic – LTL). В этом методе техническая система, представленная в виде структуры Крипке, и отрицание проверяемого свойства преобразуются в автоматы Бюхи. Далее по ним строится композиция автоматов для проверки выполнимости проверяемого свойства на технической системе.

Подробное описание дается в статье «Анализ моделей программ на языке асинхронных функциональных схем средствами темпоральной логики линейного времени», авторы: Кораблин Ю.П., Косакян М.Л. (Российский государственный социальный университет, г. Москва).