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

摘要：

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

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

所属期刊栏目：32

分类号：TP301(计算技术、计算机技术)

资助基金：航空科学基金;国家自然科学基金;中央高校基本科研项目;中央高校基本科研项目

在线出版日期：2023-01-07（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：69-73,122