Формальные спецификации в технологиях обратной инженерии и верификации программ.

Формальные спецификации в технологиях обратной инженерии и верификации программ.

И.Б. Бурдонов, А.В. Демаков, А.С. Косачев, А.В. Максимов, А.К. Петренко.

Abstract

KVEST (Kernel Verification and Specification Technology) – технология спецификации и верификации программного обеспечения, основанная на автоматизированной генерации тестов из формальных спецификаций. Эта технология была разработана в рамках контракта с Nortel Networks и базируется на опыте, полученном в результате академических исследований. К 1999 году методология и набор инструментов применялись в трех индустриальных проектах верификации телекоммуникационного ПО. Первый проект, The Kernel Verification project, дал название методологии и набору инструментов. Результаты этого проекта присутствуют в Formal Method Europe Application database [28]. Это одно из крупнейших приложений формальных методов, присутствующих в базе данных. Данная статья содержит краткое описание подхода, сравнение со сходными работами и перспективы развития.

Edition

Proceedings of the Institute for System Programming, vol. 1 (in Russian), 2000, Стр. 39-54.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

For citation

И.Б. Бурдонов, А.В. Демаков, А.С. Косачев, А.В. Максимов, А.К. Петренко. Формальные спецификации в технологиях обратной инженерии и верификации программ. . Proceedings of the Institute for System Programming, vol. 1 (in Russian), 2000, Стр. 39-54. .

Full text of the paper in pdf Back to the contents of the volume