TY - JOUR

T1 - Formal Sequentialization of Distributed Systems via Program Rewriting

AU - Bertran, Miquel

AU - Babot, Francesc

AU - Climent, August

N1 - Funding Information:
1 Work partially supported by the CICYT under project TIN2006-14738-C02-02, and by General Systems Development, www.gsystemsd.com 2 Email:miqbe@salle.url.edu 3 Email:fbabot@salle.url.edu 4 Email:augc@salle.url.edu

PY - 2007/7/16

Y1 - 2007/7/16

N2 - 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 sequentialization process. The main contribution of this work is the extension of these results to encompass the formal elimination of both synchronous communications embedded within a subclass of selection statements, and of non-disjoint synchronous communication pairs. None of these cases has been treated in the literature before, and their solution considerably widens the application domain of formal sequentialization.

AB - 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 sequentialization process. The main contribution of this work is the extension of these results to encompass the formal elimination of both synchronous communications embedded within a subclass of selection statements, and of non-disjoint synchronous communication pairs. None of these cases has been treated in the literature before, and their solution considerably widens the application domain of formal sequentialization.

KW - Formal communication elimination

KW - distributed programs

KW - formal sequentialization

KW - formal verification

KW - laws of distributed programs

KW - parallel programs

KW - rewriting

UR - http://www.scopus.com/inward/record.url?scp=34447274753&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2007.05.038

DO - 10.1016/j.entcs.2007.05.038

M3 - Article

AN - SCOPUS:34447274753

SN - 1571-0661

VL - 188

SP - 53

EP - 75

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

ER -