Formal Methods to Support the Design of Distributed Systems; Final technical memo. Jun-Sep 07

摘要

This work contributes to a formal framework to support the development of distributed systems: a specification serves to document a system; it can be executed to simulate the system; and it can be subjected, either directly or after some modular extension or transformation, to various kinds of formal analyses. Two on-the-fly techniques to reduce the state space were developed: one a symmetry reduction; the other a partial-order reduction. These are implemented as simple transformations of the specification of the system. A third transformational technique allows the verification of nontrivial properties not readily expressible in linear temporal logic.