供热混合系统的抽象及其形式化验证

代理获取

页面导航

摘要
著录项
相似文献
相关主题

摘要

本文采用了两者结合的方法，先对供热混合系统用基于定性推理的方法，将其转变为离散的抽象系统，并用Matlab中的图形化建模工具Stateflow建立了离散状态模型图，再采用符号模型验证工具SMV(Symbolic Model Verification)进行自动验证。针对供热混合系统形式化验证中状态空间爆炸问题，本文利用在定性推理的方法上进行扩展，基于实数域求n阶导数进行数据抽象，将复杂的混合系统，简化为抽象离散系统，不但有效地降低系统复杂程度，简化后的系统更容易被分析，而且仍然充分地保留了系统的安全特性。此外，本文利用符号模型验证工具SMV对供热系统抽象后的离散模型实现了自动验证。SMV基于OBDDs的搜索算法确定系统是否满足用计算树逻辑CTL描述的被验证性质。符号化表示对于数字电路设计的建模十分自然,而且能够验证具有极大状态空间的系统。由于混合系统验证的重点是状态空间的划分，故在文章的最后对其它几种混合系统的形式化验证方法做了比较。同其它方法相比，本文计算抽象迁移系统的方法更加精确而且计算更加简单，适用范围更加广泛。

著录项

作者
王莉;
展开▼
作者单位

华中科技大学;

展开▼
授予单位华中科技大学;
学科检测技术与自动化装置
授予学位硕士
导师姓名孔力;
年度 2004
页码
总页数
原文格式 PDF
正文语种中文
中图分类自动控制、自动控制系统;
关键词
供热混合系统; 形似化自动验证; 数据抽象; 符号模型检验;

相似文献

中文文献
外文文献
专利

1. 基于流管道过近似的混合系统形式化验证技术 [J] . 李辉 ,方敏 . 合肥工业大学学报（自然科学版） . 2008,第001期
2. 混合投影时序逻辑与混合系统的形式化验证 [J] . 张海宾 ,段振华 . 计算机科学 . 2007,第011期
3. 混合系统的形式化验证 [J] . 高建平 ,陈宗基 . 北京航空航天大学学报 . 1999,第002期
4. 基于层次组合抽象的智能系统形式化验证 [J] . 周益龙 ,韩斌 . 计算机与数字工程 . 2019,第008期
5. VSOS-HAM:基于Isabelle/HOL的OS内核硬件抽象模型和形式化验证方法研究 [J] . 钱振江 ,黄皓 ,宋方敏 . 南京大学学报：自然科学版 . 2017,第3期
6. 抽象距离引导的半形式化验证方法 [C] . 张弢 ,吕涛 ,李晓维 . 第十三届全国容错计算学术会议 . 2009
7. 混合系统的形式化验证 [A] . 张海宾 . 2007

供热混合系统的抽象及其形式化验证

摘要

著录项

相似文献

相关主题

期刊订阅