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

Hybrid System Performance Evaluation Language Based on Fixed Point Logic

作　　者：李晴 曹子宁[1,2,3] 黄涛 LI Qing;CAO Zi-ning;HUANG Tao(School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China;Science and Technology on Electro-optic Control Laboratory,Luoyang 471023,China;Collaborative Innovation Center of Novel Software Technology and Industrialization,Nanjing 210023,China)

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

出　　处：《计算机技术与发展》2022年第12期69-73,122,共6页Computer Technology and Development

基　　金：航空科学基金(20185152035);国家自然科学基金(61572253);中央高校基本科研项目(NJ2020022,NJ2019010)。

摘　　要：混成系统是一类连续与离散行为紧密结合的复杂动态系统,目前广泛地应用在医疗和国防等安全关键领域。安全关键系统要求自身具有较高的安全性与可靠性,以减少系统故障引起的生命和财产方面的灾难性后果。而形式化方法是保障系统可靠性的一种常用方法,其中模型检测应用最为广泛。由于模型检测只能给出系统是否满足某个性质的真或假逻辑值,通过将其与性能评价相结合,以描述系统与实值计算相关的一些性质。现有的性能评价语言CTML可以描述系统与概率和平均期望相关的性质,μ演算则可以通过最小和最大不动点运算符描述迁移系统的某些性质。在基于μ演算的模型检测和CTML的基础上,提出一种面向混成系统的基于不动点的新的性能评价语言MLBoF以及MLBoF公式的性能评价算法。针对CTML的子逻辑,给出与其语义等价的MLBoF公式表示以及二者等价的证明过程。通过飞机起飞系统实例说明,提出的性能评价语言MLBoF不仅将基于μ演算的模型检测结果从{0,1}扩展到实数区间,具有验证系统概率等实值性质的能力;而且通过扩展经典的计算不动点的改进算法,保证了MLBoF的性能评价算法的效率。Hybrid system is a complex dynamic system with continuous and discrete behavior,which is widely used in various safety critical fields,such as medical treatment and national defense.Such safety critical system requires high safety and reliability to reduce the catastrophic consequences of life and property caused by system failures.Formal method is a common method to guarantee system reliability,and model checking is the most widely used.Since model checking can only give the true or false logical value whether the system satisfies a certain property,it is combined with performance evaluation to describe some properties related to real value calculation of the system.The existing performance evaluation language CTML can describe the properties of the system related to probability and average expectation,andμ-calculus can describe some properties of the migration system through the minimum and maximum fixed point operators.Based onμ-calculus and CTML,a new performance evaluation language MLBoF for hybrid system based on fixed point and an performance evaluation algorithm are proposed.For the sublogic of CTML,the MLBoF formula representation equivalent to its semantics and the proof process of their equivalence are given.The example of aircraft taking off control system shows that the MLBoF extends the verification results ofμ-calculus from{0,1}to real interval,with the ability to verify the probability properties of system,but also ensure the efficiency of MLBoF performance evaluation algorithm by extending the algorithm of traditional fixed points calculation.

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]