TY - GEN
T1 - A static communication elimination algorithm for distributed system verification
AU - Babot, Francesc
AU - Bertran, Miquel
AU - Climent, August
PY - 2005
Y1 - 2005
N2 - A schema of communication elimination laws for distributed programs and systems is mathematically justified in a new equivalence, which was introduced in a recent work. A complete set of applicability conditions is derived for them. A formal communication elimination algorithm, applying the laws as reductions, is mathematically justified for an important class of distributed programs and systems, whose communications are outside the scope of selections. The analysis provides the basis for extensions to general statements. State-vector reduction stands as one of the motivations for this static analysis approach. It has already been applied in an equivalence proof of a non-trivial pipelined distributed system, reported in prior works. The state-vector reduction obtained in this proof, yielding a reduction factor of 2 -607 for the upper-bound on the number of states, is presented in this communication.
AB - A schema of communication elimination laws for distributed programs and systems is mathematically justified in a new equivalence, which was introduced in a recent work. A complete set of applicability conditions is derived for them. A formal communication elimination algorithm, applying the laws as reductions, is mathematically justified for an important class of distributed programs and systems, whose communications are outside the scope of selections. The analysis provides the basis for extensions to general statements. State-vector reduction stands as one of the motivations for this static analysis approach. It has already been applied in an equivalence proof of a non-trivial pipelined distributed system, reported in prior works. The state-vector reduction obtained in this proof, yielding a reduction factor of 2 -607 for the upper-bound on the number of states, is presented in this communication.
UR - http://www.scopus.com/inward/record.url?scp=33646809010&partnerID=8YFLogxK
U2 - 10.1007/11576280_26
DO - 10.1007/11576280_26
M3 - Conference contribution
AN - SCOPUS:33646809010
SN - 3540297979
SN - 9783540297970
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 375
EP - 389
BT - Formal Methods and Software Engineering - 7th International Conference on Formal Engineering Methods, ICFEM 2005, Proceedings
T2 - 7th International Conference on Formal Engineering Methods, ICFEM 2005
Y2 - 1 November 2005 through 4 November 2005
ER -