Sciweavers

Share
ENTCS
2007

Formal Sequentialization of Distributed Systems via Program Rewriting

11 years 8 months ago
Formal Sequentialization of Distributed Systems via Program Rewriting
Formal sequentialization is introduced as a rewriting process for the reduction of parallelism and internal communication statements of distributed imperative programs. It constructs an equivalence proof in an implicit way, via the application of equivalence laws as rewrite rules, thus generating a chain of equivalent programs. The variety of the possible sequentialization degrees which are attainable is illustrated with an example. The approach is static, thus avoiding the state explosion problem, has an impressive state-vector reduction in many cases, and could be combined, as a model simplification step, with model checking and interactive theorem proving in system verification. Prior grounding results needed in formal sequentialization are overviewed; more specifically, an algorithm for the automatic elimination of communications under the scope of sequential and parallel compositions, elimination laws which the algorithm applies, and a suitable equivalence criterion for the se...
Miquel Bertran, Francesc-Xavier Babot, August Clim
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Where ENTCS
Authors Miquel Bertran, Francesc-Xavier Babot, August Climent
Comments (0)
books