实时系统的形式化验证

实时系统的设计对系统设计人员而言是一个巨大挑战。在缺乏严格的验证环境时 ,要避免设计错误是很困难的。本文将一种带时戳的时序逻辑及用于描述具体实时系统的时间变迁系统编码到 HOL定理证明器中 ,并实现了一个基本的规则策略库 ,从而实现了一个简单的交互式辅助验证环境L RP。实例 Fisher算法的互斥性在 IRP中得到了验证。

On Formal Verification of Real-Time Systems

The design of real time systems poses severe challenge to system designers.In the absence of a rigorous verification environment,it seems diffcult to avoid design errors as desired.In this paper,we report our work in embedding a temporal logic(TLг)and representing real time systems in HOL(Higher Order Logic)theorem prover.Also,we have encoded and proved a set of basic proof rules and strategies.We have implemented a simple interactive prototype verification environment which we call IRP.A famous case study on Fisher's exclusion algorithm is verified mechanically in IRP.