| Summary: | 碩士 === 國立臺灣師範大學 === 資訊教育研究所 === 91 === Automated finite-state verification techniques have matured considerably in the past decades, but state-space explosion remains an obstacle to their use. Theoretical lower bounds on complexity imply that all of the techniques that have been developed to avoid or mitigate state-space explosion depend on models that are “well-formed” in some way, and will usually fail for other models. This further implies that, when analysis is applied to models derived from designs or implementations of actual software systems, a model of the system “as built” is unlikely to be suitable for automated analysis. In particular, compositional hierarchical analysis (where state-space explosion is avoided by simplifying models of subsystems at several levels of abstraction) depends on the modular structure of the model to be analyzed. We describe how as-built finite-state models can be refactored for compositional state-space analysis, applying a series of transformations to produce an equivalent model whose structure exhibits suitable modularity.
In this thesis, we adopt Promela the as front-end language to automate refactoring. We select a subset of Promela and add some keywords for refactoring. The extended syntax is called rc-Promela, where “r” stands for “refactor” and “c” stands for “ccs.” We build a parser for rc-Promela, and use the parser to construct AST for rc-Promela model. Finally, we apply data flow analysis on AST to generate compact CCS state graphs for refactoring.
|
|---|
