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

扫码查看

原文链接

万方数据
维普

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

外文标题：Hybrid System Performance Evaluation Language Based on Fixed Point Logic

作者：

李晴、曹子宁、黄涛

展开 >

作者单位：

南京航空航天大学计算机科学与技术学院,江苏南京 211106

光电控制技术重点实验室,河南洛阳 471023

软件新技术与产业化协同创新中心,江苏南京 210023

关键词：

混成系统不动点 CTML μ演算性能评价

基金：

航空科学基金国家自然科学基金中央高校基本科研业务费专项中央高校基本科研业务费专项

项目编号：

2018515203561572253NJ2020022NJ2019010

出版年：

2022

DOI：

10.3969/j.issn.1673-629X.2022.12.011

计算机技术与发展

陕西省计算机学会

计算机技术与发展

CSTPCD

影响因子：0.621

ISSN：1673-629X

年,卷(期)：2022.32(12)

参考文献量5