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