Reachability Analyser for Algebraic System Nets.

摘要

Concurrent and distributed systems are difficult to manage without using formal analysis methods. The user of formal methods has to find a balance between expressive power and tractability. A formalism with small expressive power may not suit well to describing all real-life systems, but on the other hand, performing exhaustive reachability analysis on a system defined using a highly expressive formalism may be an unsolvable problem. Using extended many-sorted algebras, this work defines the data type system and the set of algebraic operations that the author has implemented in a reachability analyzer intended for modeling computer software based communications protocols. The work also introduces the modeling formalism of the analyzer, algebraic system nets. The report discusses some implementation details of the reachability analyzer both from a theoretical and from a software technology point of view. Finally, the work shows how some constructions difficult for other tools can be modeled using the new formalism, and describes how different programming language constructions can be transformed to parts of a model by a semi-automated compiler.