北京航空航天大学学报 ›› 1999, Vol. 25 ›› Issue (2): 146-150.

• 论文 • 上一篇    下一篇

混合系统的形式化验证

高建平, 陈宗基   

  1. 北京航空航天大学 自动控制系
  • 收稿日期:1997-11-07 出版日期:1999-02-28 发布日期:2010-09-28
  • 作者简介:男 29岁 博士生 100083 北京
  • 基金资助:

    国家"八六三"高技术计划(863-306-05-07)资助项目

Formal Verification of Hybrid System

Gao Jianping, Chen Zongji   

  1. Beijing University of Aeronautics and Astronautics,Dept. of Automatic Control
  • Received:1997-11-07 Online:1999-02-28 Published:2010-09-28

摘要: 结合混合系统的研究对余度管理系统进行了形式化的分析和验证.采用的手段是时段演算技术及其扩展.首先进行形式化的需求分析,需求及其假设用时段演算表示,其次严格化地描述算法和参数的选取.在验证过程中,首先应用程序逻辑验证算法,算法的不变量以时段演算表示,最后在时段演算中验证整个系统的行为满足给定的需求.

Abstract: As a case study of hybrid system, a redundancy management system in flight control system is formally investigated and its specification and verification are presented using an approach incorporating program logic into duration calculi. Firstly, the requirement with some assumptions is captured in duration calculi, then the algorithm is specified in mixed-term hybrid descriptions and a parameter selection is given. During the verification phase,the program invariant is reasoned about with Hoare logic and specified by duration formulae. Finally, the whole verification is finished in the duration calculus framework.

中图分类号: 


版权所有 © 《北京航空航天大学学报》编辑部
通讯地址:北京市海淀区学院路37号 北京航空航天大学学报编辑部 邮编:100191 E-mail:jbuaa@buaa.edu.cn
本系统由北京玛格泰克科技发展有限公司设计开发