资源描述：
《供热混合系统的抽象及其形式化验证》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。
1、华中科技大学硕士学位论文供热混合系统的抽象及其形式化验证姓名：王莉申请学位级别：硕士专业：检测技术与自动化装置指导教师：孔力20041113摘要在供热系统中水作为工作介质和热能的载体其压力高低直接影响着供热质量和系统的运行安全供热系统中既有连续系统如水压的变化又包含离散系统如水泵的开关等属于典型的混合系统面对现在对控制技术的要求和系统的复杂性日益增高,在系统设计中混合系统本身的正确性和可靠性尤为重要目前比较流行的一种验证方式是形式化验证方法,分为模型检验和利用演绎证明两种方法本文采用了两者结合的方法先对供热混合系
2、统用基于定性推理的方法将其转变为离散的抽象系统并用Matlab中的图形化建模工具Stateflow建立了离散状态模型图再采用符号模型验证工具SMV(SymbolicModelVerification)进行自动验证针对供热混合系统形式化验证中状态空间爆炸问题本文利用在定性推理的方法上进行扩展基于实数域求n阶导数进行数据抽象将复杂的混合系统简化为抽象离散系统不但有效地降低系统复杂程度简化后的系统更容易被分析而且仍然充分地保留了系统的安全特性此外本文利用符号模型验证工具SMV对供热系统抽象后的离散模型实现了自动验证SM
3、V基于OBDDsorderedbinarydecisiondiagrams的搜索算法确定系统是否满足用计算树逻辑CTLComputationTreeLogic描述的被验证性质符号化表示对于数字电路设计的建模十分自然,而且能够验证具有极大状态空间的系统本文将其用于供热系统抽象后的离散系统的自动化验证也能够验证很大的状态空间由于混合系统验证的重点是状态空间的划分故在文章的最后对其它几种混合系统的形式化验证方法做了比较同其它方法相比本文计算抽象迁移系统的方法更加精确而且计算更加简单适用范围更加广泛然而这种方法没有包含除
4、了时间顺序的其他时间的信息比如定时器的时间如何在具体实际应用中解决定时器的自动验证问题是今后努力的方向关键词供热混合系统形似化自动验证数据抽象符号模型检验IAbstractIntheheatingsystem,water,asthemediumandcarrierofheatenergy,itspressurelevelinfluencestheheatingqualityandthesafeoperationofsystemdirectly.Heatingsystemcomprisedofcontinuouss
5、ystem(suchasthechangeofwaterpressure),anddiscretesystem(suchastheturningonorturnoffofwaterpump),soheatingsystembelongtotypicalhybriddynamicsystem.InthefaceoftherequisitionforcontroltechnologyandsystematiccomplexityIncreaseddaybyday,theexactnessanddependabilit
6、yofhybridsystemareparticularlyimportant.Theformalverificationofhybridsystemincludestheautomaticverificationofmodelexaminationbyalgorithm,andartificialormachineryverificationutilizingdeductioncertification.Thisthesiscombinesthetwomethods.First,changetheheating
7、dynamicsystemintoadiscreteabstractionsystembymeansofqualitativereasoningmethod.Second,setupadiscretestatemodeldiagramwithfiguremodelingtoolStateflowinMatlab.Last,adoptthesymbolmodelverificationtoolSMVtoprovethediscretestatemodelautomatically.Duetostatespaceex
8、plosionprobleminheatinghybridsystemformalverification,thisthesisexpandsthequalitativereasoningmethod,onthebasisofnthderivationintherealspace,changetheheatingdynamicsystemintoadiscreteabst
