基于进程代数和模型检验的系统建模与评价

摘要

性能评价的目的是描述和分析系统的动态及与时间有关的行为。尽早将功能、时序行为检验与设计相结合，可以在很大程度上消除不必要的错误，提高设计质量。评价模型常采用变迁模型描述系统的动态行为。在实时系统性能(包括可靠性)的分析中，连续时间马尔可夫链模型被得到广泛应用。但目前软件系统和硬件系统的规模和复杂度增长迅速，企图直接获得系统的马尔可夫模型极为繁琐且易出错，这就需要一种合适的建模技术，能形式化地描述系统且易获得系统的马尔可夫模型。而进程代数面向行为，提供了结构化操作语义，可借助自动推理展开状态空间，无需直接面对状态，同时具有很自然的合成和抽象的能力，能有效压缩状态空间，更可将进程代数模型映射到带标号的变迁系统，从而可方便地获得马尔可夫模型，因此进程代数成为复杂系统性能评价的建模利器。 在进行性能评价时，获取如失效时间、系统吞吐量和利用率等性能指标是一件很棘手的工作，且基本上是非形式化的、非专用的方法，因此通常只有一些基于状态的度量相对简单一点。基于时序逻辑的模型检验可以很好地解决这个问题。模型检验是一种自动验证方法，避免建立复杂的证明过程，并在规格说明不满足系统模型的要求时能提供反例。目前很多实时系统性能评价的工作基于连续时间马尔可夫链，直接分析实时系统获得性能参数是非常困难的事情，因此需要在建模和性能评价之间搭建一个桥梁，能很好地结合实时系统的形式化建模和实时系统的性能评价分析这两种技术，降低性能评价复杂度，提高效率。将进程代数与模型检验相结合，可以解决传统性能评价工作中若干难点，例如：建模困难且易出错，描述不规范，缺乏合成和抽象的能力，难以进行基于路径的度量等等，本文就并发系统的进程代数建模与实时随机系统的模型检验作了一定的研究。 ⑴使用进程代数描述了Ada会合机制，Ada保护对象及Java多线程机制，并提出了一种基于进程代数的Ada并发程序静态死锁检测方法。文中详细分析了会合通信，在每条导向同步的控制边附加一个代理同步通信过程的通信原子动作，从而构造了进程代数会合机制模型。再根据会合通信进程代数模型原理对源程序逐层扫描，提出了一种新的扫描源程序的层操作算法，实现了Ada并发程序到进程代数形式化描述的转换，并在转换过程中，通过进程代数的自动等价推导代数表达式以模拟运行，找出系统中可能触发死锁的死通信，进一步结合控制依赖分析死通信的各类组合情况，检测出潜在的死锁环路。这种Ada并发程序的静态死锁检测方法的最大优势是能利用进程代数的形式化建模和自动等价推理，并在需要时通过合成和抽象降低状态空间。由于进程代数具有很强的处理抽象、过程合成及隐藏内部细节的能力，因此以进程代数形式化系统为基础，可支持我们在可达性分析、依赖性分析、通信关系分析、切片分析及控制流分析等领域的研究。 ⑵提出一种带动作标号的随机变迁系统ALSTS(Action Labeled Stochastic Transition System)及其扩展ALSTS<'*>，并对ALSTS<'*>系统进行随机进程代数建模与隐马尔可夫模型分析应用。文中提出的带动作标号的随机变迁系统(ALSTS)包含动作和随机时间信息，可用于表达系统的变迁行为、时序信息、概率特征及随机性，ALSTS的每个状态可对应连续时间马尔可夫链(CTMC)的一个节点，状态之间的变迁对应CTMC节点之间的弧，从而可获得用于性能评价的转换速率矩阵。由于系统往往会因各种缺陷或误差等而失效，因此将ALSTS系统扩展为ALSTS<'*>系统，允许状态内原子命题服从一定的概率分布，使得系统包含双重随机特性。随后使用随机进程代数对ALSTS<'*>系统进行了建模。本文还依据ALSTS<'*>系统的概率特性和随机性进行了隐马尔可夫模型的分析，提供的随机分析参考可辅助测试人员对实时系统进行黑盒观测，例如，在设计测试用例时，根据若干次观测，可以估得该测试用例对路径的覆盖率，进而调整测试用例，修正覆盖率，对重点模块增强覆盖；也可根据若干次观测，估得下一次系统最可能的执行路径，从而能加快调试定位。正因为建立了这样的隐马尔可夫模型，使得很多分析测试成为可能或更为便捷。且对于非常复杂的黑盒系统，可以结合进程代数的合成能力采用逐步分解的方法来进行观测分析。 ⑶提出了一种基于迹的连续随机时序逻辑tCSL(Trace based Continous Stochastic Logic)，并给出了ALSTS<'*>系统从随机进程代数建模到tCSL模型检验的性能评价方法。CSL(Continuous Stochastic Logic)时序逻辑不含动作的概念，因此无法针对变迁动作进行分析，aCSL(action labeled Continuous Stochastic Logic)虽然可以分析变迁过程中的动作，但不能分析动作的执行顺序，本文在CSL和aCSL的基础上增加了动作的概念、关键路径的概念及迹关键动作的概念，描述了tCSL的词法和语义，对不限时与限时的“Next”和“Umil”时序操作给出了基于关键路径和关键动作的稳态概率分析，重点阐述了针对路径的tCSL模型检验的方法，并通过实例分析，结合ALSTS<'*>系统的随机进程代数建模，实现了对关键动作序列有要求的路径相关的系统性能评价。并给出了tCSL模型检验平台支撑工具原型。 ⑷借助迹关键动作和瞬时内部动作，给出了一种非确定性随机系统向ALSTS<'*>系统转换的方法，从而可使用tCSL模型检验方法对重构后的非确定性系统进行路径相关的系统性能评价。本文还提出了迹互模拟等价的概念，给出了迹互模拟等价性定理。利用迹互模拟等价性，可对系统的状态空间进行压缩，并能保留关键路径和关键动作的信息。

目录

文摘

英文文摘

声明

第一章 引言

1.1选题依据

1.2国内外研究现状

1.3主要研究内容

1.4论文主要成果

1.5论文结构

第二章 进程代数形式化描述并发程序

2.1基本概念

2.2 Ada任务会合的ACP描述

2.3 Ada并发程序的转换

2.3.1转换思想

2.3.2基本转换规则

2.3.3会合转换规则

2.4 Ada保护对象的进程代数建模

2.4.1 Ada95保护对象的结构化模型

2.4.2保护对象的进程代数模型

2.4.3应用

2.5 Java线程的进程代数描述

2.6本章小结

第三章 基于进程代数的Ada并发程序静态死锁检测

3.1死锁检测的基本思想

3.2 Ada并发程序的死锁检测

3.2.1基本定义

3.2.2全路径死锁环路检测

3.2.3可能死锁环路检测

3.3实例研究

3.4本章小结

第四章 实时随机系统的进程代数建模

4.1基本概念

4.1.1带标号的变迁系统

4.1.2连续时间马尔可夫链

4.2 LTS的随机扩展-ALSTS

4.3状态内原子命题服从概率分布的ALSTS

4.4 ALSTS*系统的随机进程代数建模

4.4.1随机进程代数

4.4.2 CTMC的进程代数描述

4.4.3 ALSTS*系统的随机进程代数建模

4.5 ALSTS*的隐马尔可夫模型分析

4.5.1隐马尔可夫模型

4.5.2 ALSTS*的隐马尔可夫模型定义

4.6隐马尔可夫模型的三个核心问题

4.6.1模型观察序列的概率

4.6.2最相似状态序列

4.6.3参数调整

4.7 ALSTS*系统的应用

4.8本章小结

第五章 ALSTS*系统的tCSL模型检验

5.1模型检验

5.1.1连续随机逻辑CSL

5.1.2基于迹的连续随机逻辑tCSL

5.2模型检验tCSL

5.2.1瞬时概率及稳态概率

5.2.2 ALSTS*系统的tCSL模型检验

5.2.3 tCSL模型检验的平台支撑工具

5.3迹互模拟等价

5.4非确定性系统的分析

5.5本章小结

第六章 总结与展望

6.1论文总结

6.2未来工作展望

致谢

参考文献

附录