在供热系统中水作为工作介质和热能的载体,其压力高低直接影响着供热质量和系统的运行安全。供热系统中既有连续系统(如水压的变化),又包含离散系统(如水泵的开、关等),属于典型的混合系统。面对现在对控制技术的要求和系统的复杂性日益增高, 在系统设计中,混合系统本身的正确性和可靠性尤为重要。目前比较流行的一种验证方式是形式化验证方法, 分为模型检验和利用演绎证明两种方法。本文采用了两者结合的方法,先对供热混合系统用基于定性推理的方法,将其转变为离散的抽象系统,并用Matlab中的图形化建模工具Stateflow建立了离散状态模型图,再采用符号模型验证工具SMV(Symbolic Model Verification)进行自动验证。 针对供热混合系统形式化验证中状态空间爆炸问题,本文利用在定性推理的方法上进行扩展,基于实数域求n阶导数进行数据抽象,将复杂的混合系统,简化为抽象离散系统,不但有效地降低系统复杂程度,简化后的系统更容易被分析,而且仍然充分地保留了系统的安全特性。 此外,本文利用符号模型验证工具SMV对供热系统抽象后的离散模型实现了自动验证。SMV基于OBDDs(ordered binary decision diagrams)的搜索算法确定系统是否满足用计算树逻辑CTL(Computation Tree Logic)描述的被验证性质。符号化表示对于数字电路设计的建模十分自然,而且能够验证具有极大状态空间的系统。本文将其用于供热系统抽象后的离散系统的自动化验证,也能够验证很大的状态空间。由于混合系统验证的重点是状态空间的划分,故在文章的最后对其它几种混合系统的形式化验证方法做了比较。同其它方法相比,本文计算抽象迁移系统的方法更加精确而且计算更加简单,适用范围更加广泛。然而,这种方法没有包含除了时间顺序的其他时间的信息,比如定时器的时间。如何在具体实际应用中解决定时器的自动验证问题,是今后努力的方向。