Abstract:
The article deals with the problem of proving observational equivalence for the class of computational processes called the processes with message passing. These processes can execute actions of the following forms: sending or receiving the messages, checking the logical conditions, and updating the values of internal variables of the processes. The main result is the theorem that reduces the problem of proving observational equivalence of a pair of processes with message passing to the problem of finding formulas associated with pairs of states of these processes, satisfying certain conditions that are associated with transitions of these processes. This reduction is a generalization of Floyd's method of flowchart verification, which reduces the problem of verification of flowcharts to the problem of finding formulas (called intermediate assertions) associated with points in the flowcharts and satisfying conditions, corresponding to transitions in the flowcharts. The method of proving the observational equivalence of processes with message passing is illustrated by an example of sliding window protocol verification.
Keywords:verification; processes with message passing; observational equivalence; sliding window protocol.
Fulltext:
PDF file (333 kB)