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

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

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

Аннотация

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

Издание

Труды Института системного программирования РАН, том 1, 2000, стр. 39-54.

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

Для цитирования

И.Б. Бурдонов, А.В. Демаков, А.С. Косачев, А.В. Максимов, А.К. Петренко. Формальные спецификации в технологиях обратной инженерии и верификации программ. . Труды Института системного программирования РАН, том 1, 2000, стр. 39-54. .

Полный текст статьи в формате pdf Вернуться к содержанию тома