科研之友
微信
新浪微博
Facebook
分享链接
摘要
本发明公开了一种基于Event-B方法的微内核操作系统进程间通信机制的形式化建模和验证方法,包括：需求设计分析,根据基于Event-B方法的微内核操作系统进程间通信机制,结合订阅者发布者模式,设计分析符合Event-B建模的原始需求。根据基于Event-B方法的微内核操作系统进程间通信机制以及原始需求的结果,设计分析符合Event-B建模的重写需求；建模精化验证,根据重写需求,设计建立验证基于Event-B方法的微内核操作系统进程间通信机制的模型。该模型需要验证的证明义务包括模型功能性不变式以及模型性质不变式和安全性质相关不变式。
- 单位
