Adding liveness properties to coupled finite-state machines

ABSTRACT

Informal specifications of protocols are often imprecise and incomplete and are usually not sufficient to ensure the correctness of even very simple protocols. Consequently, formal specification methods, such as finite-state models, are increasingly being used. The selection/resolution (S/R) model is a finite-state model with a powerful communication mechanism that makes it easy to describe complex protocols as a collection of simple finite-state machines. A software environment, called SPANNER, has been developed to specify and analyze protocols specified with the S/R model. SPANNER provides the facility to compute the joint behavior of a number of finite-state machines and to check if the “product” machine has inaccessible states, states corresponding to deadlocks, and loops corresponding to livelocks. So far, however, SPANNER has had no facility to systematically deal with liveness conditions. For example, one might wish to specify that, although a communication channel is unreliable, a message will get through if it is sent infinitely often, and to check that the infinite behavior of the protocol viewed as an infinite sequence will always be in some &ohgr;-regular set (possibly specified in terms of a formula in temporal logic or as an &ohgr;-automata). In this paper we show that with very minor modifications to the implemented system it is possible to substantially extend the type of properties that can be specified and checked by SPANNER. This is done by extending the S/R model to include acceptance conditions found in automatons on infinite words, which permits the incorporation of arbitrary liveness conditions into the model. We show how these extensions can be easily incorporated into SPANNER (and into essentially any finite-state verification system) and how the resulting system is used to automatically verify the correctness of protocols.

REFERENCES

• 1: AGGARWAL, S., AND COURCOUBETIS, C. Distributed implementation of a model of communication and computation. In Proceedings of the 18th Hawaii Information Conference on System Sciences (Hawaii, Jan. 1985), pp. 206-218.
• 2: S. Aggarwal , Z. Har'el, Simulation analysis of protocols in an integrated software environment, Computer Networks and ISDN Systems, v.16 n.3, p.197-215, Jan. 1989 [doi>10.1016/0169-7552(89)90068-8]
• 3: Sudhir Aggarwal , Daniel Barbará , Kalman Z. Meth, Spanner: a tool for the specification, analysis, and evaluation of protocols, IEEE Transactions on Software Engineering, v.13 n.12, p.1218-1237, December 1, 1987 [doi>10.1109/TSE.1987.232877]
• 4: S. Aggarwal , D. Barbaŕ , K. Z. Meth, A Software Environment for the Specification and Analysis of Problems of Coordination and Concurrency, IEEE Transactions on Software Engineering, v.14 n.3, p.280-290, March 1988 [doi>10.1109/32.4649 ]
• 5: AGGARWAL, S., KURSHAN, R. P., AND SABNANI, K.g. A calculus for protocol specification and validation. In Protocol Specification, Testing and Verification, HI, H. Rudin, and C. H. West, Eds. North-Holland, Amsterdam, 1983, pp. 19-34.
• 6: AGGARWAL, S., KURSHAN, R. P., AND SHARMA, D. A language for the specification and analysis of protocols. In Protocol Specification, Testing and Verification, III, H. Rudin, and C. H. West, Eds. North-Holland, Amsterdam, 1983, pp. 35-50.
• 7: K. A. Bartlett , R. A. Scantlebury , P. T. Wilkinson, A note on reliable full-duplex transmission over half-duplex links, Communications of the ACM, v.12 n.5, p.260-261, May 1969 [doi>10.1145/362946.362970]
• 8: B0CHI, J.R. On a decision method in restricted second order arithmetic. In Proceedings of the International Congress on Logic, Method and Philosophical Science 1960. Stanford University Press, Stanford, Calif., 1962, pp. 1-12.
• 9: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.117-126, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567080]
• 10: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 11: Brent Tzion Hailpern, Verifying concurrent processes using temporal logic, 1980
• 12: HAILPERN, B.T.,ANDOWICKI, S.S. Modularverificationofcomputercommunicationprotocols. IEEE Trans. Commun. COM-31, I (Jan. 1983).
• 13: KURSHAN, R.P. Modelling concurrent processes. In Proceedings of the American Mathematical Society Symposium on Applied Mathematics 31. American Mathematical Society, Providence, R.I., 1985.
• 14: KURSHAN, R. P., AND GOPINATH, B. The selection/resolution model for concurrent processes. Unpublished.
• 15: Orna Lichtenstein , Amir Pnueli, Checking that finite state concurrent programs satisfy their linear specification, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-107, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318622]
• 16: MANNA, Z., AND PNUELI, A. Verification of concurrent programs: The temporal framework. In The Correctness Problem in Computer Science, Boyer and Moore, Eds. Academic Press, New York, 1981.
• 17: Zohar Manna , Amir Pnueli, Verification of Concurrent Programs: Temporal Proof Principles, Logic of Programs, Workshop, p.200-252, May 01, 1981
• 18: Zohar Manna , Pierre Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.68-93, Jan. 1984 [doi>10.1145/357233.357237]
• 19: MCNAUGHTON, R. Testing and generating infinite sequences by a finite automata. Inf. Control 9 (1966), 521-530.
• 20: PNUELI, A. The temporal logic of programs. In Proceedings of the 18th Symposium on Foundations of Computer Science (Providence, R.I., Nov. 1977). 1977, pp. 46-57.
• 21: SABNANI, K. An algorithmic technique for protocol verification. IEEE Trans. Commun. To be published.
• 22: SABNANI, K., WOLPER, P., AND LAPONE, A. An algorithmic technique for protocol verification. In Proceedings of the IEEE GIobecom (New Orleans, La., Dec. 1985). IEEE, New York, 1985.
• 23: SUNSHINE, C. A., ED. Communication Protocol Modeling. Artech House, Dedham, Mass., 1981.
• 24: VARDI, M. V., AND WOLPER, P. An automata-theoretic approach to automatic program verification. In Proceedings of the Symposium on Logic in Computer Science (Cambridge, Mass., June 1986). pp. 322-331.
• 25: Pierre Leon Wolper, Synthesis of communicating processes from temporal logic specifications, 1982
• 26: WOLPER, P. Temporal logic can be more expressive. Inf. Control 56, 1-2 (Jan. 1983), 72-99.
• 27: Pierre Wolper, Expressing interesting properties of programs in propositional temporal logic, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.184-193, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512661]
• 28: WOLPER, P., VARDI, U. V., AND S1STLA, A.P. Reasoning about infinite computation paths. In Proceedings of the 24th IEEE Symposium on Foundations of Computer Science (Tucson, Ariz.). IEEE, New York, 1983, pp, 185-194.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol verification

Additional Classification:
  C. Computer Systems Organization
  C.4 PERFORMANCE OF SYSTEMS
      Subjects: Modeling techniques

  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

General Terms:
Algorithms, Verification