摘要：随着软件复杂度的迅速增长,传统的基于测试的方法逐渐难以满足航天器操作系统的可靠性和安全性需求,形式化方法逐渐成为航天器操作系统安全可靠性的有效保障.基于Rodin平台,采用Event-B形式化语言,通过需求和设计重写、制定精化策略并逐步精化的方法,对航天嵌入式操作系统SpaceOS2的中断管理模块建立了需求层和设计层形式化模型,将模型检验和定理证明相结合,验证模型的正确性并且满足安全性质.
分类：期刊> 自然科学与工程技术> 工程科技II> 航空航天科学与工程
收录：北大期刊(中国人文社会科学期刊) > CSCD 中国科学引文数据库来源期刊(含扩展版) > 统计源期刊(中国科技论文优秀期刊) > 知网收录(中) > 维普收录(中) > 万方收录(中) > JST 日本科学技术振兴机构数据库(日) > 国家图书馆馆藏 > 上海图书馆馆藏
关键词：中断管理 形式化验证 精化
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
