基于不动点逻辑的混成系统性能评价语言

来源：计算机技术与发展杂志2022年第12期北京时间：

作者：李晴;曹子宁;';黄涛

单位：1. 南京航空航天大学 计算机科学与技术学院,江苏 南京 211106;2. 光电控制技术重点实验室,河南 洛阳 471023;3. 软件新技术与产业化协同创新中心,江苏 南京 210023

摘要：混成系统是一类连续与离散行为紧密结合的复杂动态系统,目前广泛地应用在医疗和国防等安全关键领域。 安全关键系统要求自身具有较高的安全性与可靠性,以减少系统故障引起的生命和财产方面的灾难性后果。 而形式化方法是保障系统可靠性的一种常用方法,其中模型检测应用最为广泛。 由于模型检测只能给出系统是否满足某个性质的真或假逻辑值,通过将其与性能评价相结合,以描述系统与实值计算相关的一些性质。 现有的性能评价语言 CTML 可以描述系统与概率和平均期望相关的性质, ?演算则可以通过最小和最大不动点运算符描述迁移系统的某些性质。 在基于?演算的模型检测和 CTML 的基础上,提出一种面向混成系统的基于不动点的新的性能评价语言 MLBoF 以及 MLBoF 公式的性能评价算法。 针对 CTML 的子逻辑,给出与其语义等价的 MLBoF 公式表示以及二者等价的证明过程。 通过飞机起飞系统实例说明,提出的性能评价语言 MLBoF 不仅将基于?? 演算的模型检测结果从{0,1} 扩展到实数区间,具有验证系统概率等实值性质的能力;而且通过扩展经典的计算不动点的改进算法,保证了 MLBoF 的性能评价算法的效率．

关键词：混成系统;不动点;CTML; ?演算;性能评价