典型文献
基于不动点逻辑的混成系统性能评价语言
文献摘要：
混成系统是一类连续与离散行为紧密结合的复杂动态系统,目前广泛地应用在医疗和国防等安全关键领域.安全关键系统要求自身具有较高的安全性与可靠性,以减少系统故障引起的生命和财产方面的灾难性后果.而形式化方法是保障系统可靠性的一种常用方法,其中模型检测应用最为广泛.由于模型检测只能给出系统是否满足某个性质的真或假逻辑值,通过将其与性能评价相结合,以描述系统与实值计算相关的一些性质.现有的性能评价语言CTML可以描述系统与概率和平均期望相关的性质,μ演算则可以通过最小和最大不动点运算符描述迁移系统的某些性质.在基于μ 演算的模型检测和CTML的基础上,提出一种面向混成系统的基于不动点的新的性能评价语言MLBoF以及MLBoF公式的性能评价算法.针对CTML的子逻辑,给出与其语义等价的MLBoF公式表示以及二者等价的证明过程.通过飞机起飞系统实例说明,提出的性能评价语言MLBoF不仅将基于μ演算的模型检测结果从{0,1}扩展到实数区间,具有验证系统概率等实值性质的能力;而且通过扩展经典的计算不动点的改进算法,保证了MLBoF的性能评价算法的效率.
文献关键词：
混成系统;不动点;CTML;μ演算;性能评价
中图分类号：
作者姓名：
李晴;曹子宁;黄涛
作者机构：
南京航空航天大学 计算机科学与技术学院,江苏 南京 211106;光电控制技术重点实验室,河南 洛阳 471023;软件新技术与产业化协同创新中心,江苏 南京 210023
文献出处：
引用格式：
[1]李晴;曹子宁;黄涛-.基于不动点逻辑的混成系统性能评价语言)[J].计算机技术与发展,2022(12):69-73,122
A类：
CTML,MLBoF
B类：
不动点,混成系统,系统性能评价,评价语言,复杂动态系统,全关,关键领域,关键系统,系统要求,安全性与可靠性,系统故障,灾难性,形式化方法,保障系统,系统可靠性,常用方法,模型检测,检测应用,某个,逻辑值,演算,运算符,等价,起飞,实例说明,实数,验证系统,改进算法
AB值：
0.253831
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
