Informatics and Applications
2014, Volume 8, Issue 2, pp 5569
A METHOD OF PROVING THE OBSERVATIONAL EQUIVALENCE OF PROCESSES WITH MESSAGE PASSING
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.
[+] References (24)
 Milner, R. 1980. A calculus of communicating systems. Lecture
notes in computer science ser. Berlin–Heidelberg–
New York: SpringerVerlag. 92. 172 p.
 Larsen, K.G., and A. Skou. 1991. Bisimulation through
probabilistic testing. Inform. Comput. 94(1):1–28.
 arsen, K.G., and Y.Wang. 1997. Timeabstracted bisimulation:
Implicit specifications and decidability. Inform.
Comput. 134(2):75–101.
 Milner,R. 1999. Communicating andmobile systems:The.
calculus. Cambridge: Cambridge University Press. 162 p.
 Hoare, C.A.R. 1985. Communicating sequential processes.
Prentice Hall. 256 p.
 Clarke, E.M., O. Grumberg, and D. Peled. 1999. Model
checking.MIT Press. 314 p.
 Petri, C.A. 1980. Introduction to general net theory. Lecture
notes in computer science ser. Ed.W. Brauer. Berlin–
Heidelberg: SpringerVerlag. 84:1–19.
 Bergstra, J.A., A. Ponse, and S.A. Smolka, eds. 2001.
Handbook of process algebra.NorthHolland,Amsterdam.
1357 p.
 Brand, D., and P. Zafiropulo. 1983. On communicating
finitestate machines. J. ACM 30(2):323–342.
 Floyd,R.W. 1967. Assigning meanings to programs. Mathematical Aspects
of Computer Science: Symposiumon Applied
Mathematics Proceedings. Ed. J. T. Schwartz. American
Mathematical Society. 19:19–32.
 Tanenbaum, A. 2002. Computer networks. 4th ed. Prentice
Hall. 674 p.
 Badban, B.,W. J. Fokkink, and J.C. van de Pol. 2008. Mechanical
verification of a twoway slidingwindow protocol
(full version including proofs). Twente: Centre for Telematics
and Information Technology, University of Twente.
Internal Report TRCTIT0845. 55 p.
 Hailpern, B. 1982. Verifying concurrent processes using
temporal logic. Lecture notes in computer science ser.
Berlin–Heidelberg: SpringerVerlag. 129. 216 p.
 Holzmann, G. 1991. Design and validation of computer
protocols. Prentice Hall. 558 p.
 Holzmann, G. 1991. The model checker Spin. IEEE
Trans. Software Eng. 23(5):279–295.
 Kaivola, R. 1997. Using compositional preorders in the
verification of sliding window protocol. Computer aided
verification. Lecture notes in computer science ser.
Ed. O. Grumberg. Berlin–Heidelberg: SpringerVerlag.
1254:48–59.
 Godefroid, P., andD. Long. 1999. Symbolic protocol verification
with Queue BDDs. Formal Methods Syst. Design
14(3):257–271.
 Stahl, K., K. Baukus, Y. Lakhnech, andM. Steffen. 1999.
Divide, abstract, and modelcheck. Theoretical and practical
aspects of SPIN model checking. Lecture notes in
computer science ser. Eds. D. Dams, R. Gerth, S. Leue,
and M. Massink. Berlin–Heidelberg: SpringerVerlag.
1680:57–76.
 Latvala, T. 2001.Model checking LTL properties of highlevel
Petri nets with fairness constraints. Applications and
theory of Petri nets. Lecture notes in computer science ser.
Eds. J.M. Colom and M. Koutny. Berlin–Heidelberg:
SpringerVerlag. 2075:242–262.
 Schoone, A. 1991. Assertional verification in distributed
computing. Utrecht University. Ph.D. Thesis. 191 p.
 Chkliaev, D., J. Hooman, and E. de Vink. 2003. Verification
and improvement of the sliding window protocol.
Tools and algorithms for the constriction and analysis
of systems. Lecture notes in computer science ser.
Eds. H. Garavel and J. Hatcliff. — Berlin–Heidelberg:
SpringerVerlag. 2619:113–127.
 Vaandrager, F. 1986. Verification of two communication
protocols by means of process algebra. Amsterdam: Centrum
voor Wiskunde en Informatica. Technical Report
CSR8608. 76 p.
 Van Wamel, J. 1992. A study of a one bit sliding window
protocol in ACP. Amsterdam: University of Amsterdam.
Technical Report P9212. 59 p.
 Bezem,M., and J. Groote. 1994. A correctness proof of a
one bit sliding windowprotocol in ìCRL. The Computer J.
37(4):289–307.
[+] About this article
Title
A METHOD OF PROVING THE OBSERVATIONAL EQUIVALENCE OF PROCESSES WITH MESSAGE PASSING
Journal
Informatics and Applications
2014, Volume 8, Issue 2, pp 5569
Cover Date
20140331
DOI
10.14357/19922264140206
Print ISSN
19922264
Publisher
Institute of Informatics Problems, Russian Academy of Sciences
Additional Links
Key words
verification; processes with message passing; observational equivalence; sliding window protocol
Authors
A. M. Mironov
Author Affiliations
Institute of Informatics Problems, Russian Academy of Sciences, 442 Vavilov Str., Moscow 119333, Russian
Federation
