Using Parallelism and Randomness in the Analysis of Large- Scale Real-Time Systems

9311622 Lee这个项目的目标是开发高效的算法，用于通信系统和分布式实时系统的自动分析。我们的研究基于一个通用的框架，称为通信概率时间状态机(CTSMP)。CTSMP是通过一对多通道同步通信消息的状态机。此外，CTSMP还支持几个在描述实时计算机系统时有用的功能。这些特征的例子包括局部变量、定时状态传输和概率状态转换。CTSMPS的组合语义允许将复杂系统指定为相互通信和同步的简单机器的集合。计时状态转换和概率状态转换的包含允许在同一框架中对故障和计时属性进行建模。通信系统自动分析的基本问题是可达状态空间的有效生成。对于有限状态系统，问题是状态爆炸。对于无限状态系统，不可能生成所有的状态；相反，我们需要找到一种组合状态集的方法。解决状态爆炸和探索问题的方法有两种：1)通过有效的编码或通过对等价状态集进行聚类来减少状态空间；2)使用概率产生或探索更少的空间。该研究采用了这两种方法，包括以下几个相关部分：1)CTSMP状态最小化算法的设计；2)概率状态生成和搜索算法的发现；3)使用CTSMP设计高效的模型检测算法，并与基于二叉决策图的算法进行比较；4)利用并行化和随机化来提高上述算法的效率。本项目将实现这些算法，并对它们的有效性进行实验评估。***

9311622 Lee The goal of this project is to develop efficient algorithms for the automated analysis of communicating systems and distributed real-time systems. We base this research on a general framework, called a Communicating Timed State Machine with Probability (CTSMP). CTSMPs are state machines that communicate messages synchronously over one-to-many channels. In addition, CTSMPs support several features that are useful in describing real-time computer systems. Examples of such features include local variables, timed state transmissions, and probabilistic state transitions. The compositional semantics of CTSMPs allows a complex system to be specified as a collection of simple machines that communicate and synchronize with one another. The inclusion of both timed state transitions and probabilistic state transitions allows the modeling of faults and timing properties in the same framework. The fundamental issue in the automated analysis of communicating systems is the efficient generation of the reachable state space. For finite state systems, the problem is state explosion. For infinite state systems, it is not possible to generate all the states; instead, we need to find a way of combining sets of states. There are two approaches to address the state explosion and exploration problem: 1) reduce the state space either through efficient encoding or by clustering sets of equivalent states; and 2) generate or explore less space using probability. This research employs both of these approaches and consists of several related parts: 1) design of CTSMP state minimization algorithms; 2) discovery of probabilistic state generation and exploration algorithms; 3) design of efficient model checking algorithms using CTSMP and comparison with binary decision diagram based algorithms; and 4) improving the efficiency of the above algorithms using parallelism and randomization. This project will implement these algorithms and evaluate their effectiveness exper imentally. ***