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