Новости
Формальные спецификации в технологиях обратной инженерии и верификации программ.
Аннотация
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).
Для цитирования
Полный текст статьи в формате pdf
