| Summary: | 碩士 === 國立臺灣師範大學 === 資訊教育研究所 === 91 === In the recent years, many techniques for analyzing concurrent systems have been proposed. Among them, finite-state verification technique is attractive because it is simple and relatively straightforward to automate. However, its performance is limited by the well-known state explosion problem. Many techniques have been proposed to address the problem. Among which, compositional analysis which divides a full system into subsystems and analyzes the system in a divide and conquer manner is more promising for large-scale concurrent systems.
In practice, compositional techniques are inapplicable to many systems because their as-built structures may not be suitable for compositional analysis. A structure suitable for compositional analysis must contain loosely coupled components so that every component can be replaced by a simple interface process. However, an ideal structure like that seldom exists in practice.
In [6], Cheng proposed an ad hoc approach, called refactoring, to translate as-built architectures to improve compositional analysis. However, the transformations described are performed manually by ad hoc basis.
In this thesis, we implement a system to automate the refactoring. We translate rc-Promela [17], a design language, into finite state graphs in CCS semantics [4]. If refactoring is enabled, the behaviors of processes will be translated into some smaller units, called segments. Next, we derive and implement unified transformations transform the segments into new processes. In the transformations, the behaviors of the whole system remain equivalent. As a result, the new structure allows compositional analysis to exploit new composition hierarchy to avoid state explosion.
|
|---|
