This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
L.0: A Truly Concurrent Executable Temporal Logic Language for Protocols
April 1993 (vol. 19 no. 4)
pp. 410-423

The semantics L.0, a programming language designed for the specification and simulation of protocols that assumes a true concurrency model, is given in terms of predicate linear temporal logic, and the restricted universe of models assumed in L.0 programs is defined. The execution algorithm for L.0 constructs a model in this universe. The restricted subset of temporal logic exploited permits a nonbacktracking execution algorithm. Fundamental to the semantics of L.0 is a frame assumption, which generalizes the frame assumption of standard imperative programming, and which eases specification of protocols. The data domain assumed in L.0 programs is sets of trees with labeled edges, and the state predicates permitted include existence and nonexistence predicates, as well as the more traditional assignment and equality predicates. These choices for data domain and predicates permit convenient specification of the hierarchical message structure often assumed in telecommunications protocols, for in such message structures, the existence or nonexistence of parts of the message hierarchy is determined by logical properties of the rest of the message hierarchy. A small portion of the logical layer specification of Futurebus+ is taken as the main example in this study.

[1] M. Abadi and Z. Manna, "Temporal logic programming," inProc. Int. Symp. Logic Programming, IEEE, Sept. 1987, pp. 4-16.
[2] R. Alur, C. Courcoubetis, and D. Dill, "Model-checking for real-time systems," inProc. 5th Annual IEEE Symp. Logic in Computer Science, pp. 414-425, 1990.
[3] R. Alur and D. Dill, "Automata for modeling real-time systems," inProc. 17th ICALP, 1990.
[4] R. Alur and T. Henzinger, "A really temporal logic," inProc. 30th Symp. Foundations of Computer Science, pp. 164-169, IEEE Computer Society Press, 1989.
[5] M. Ansari, L. Ness, M. Rusinkiewicz, and A. Sheth, "Executing multidatabase transactions," inAnnu. Proc. 25th Hawaii Int. Conf. Systems Sciences, Jan. 1992.
[6] H. Barringer, M. Fisher, D. Gabbay, G. Gough, and R. Owens, "Metatem: A framework for programming in temporal logic," inProc. REX Workshop Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, May 19-June 2, 1989. Mook, The Netherlands: Springer-Verlag, 1990.
[7] M. Baudinet, "Temporal logic programming is complete and expressive," inSixteenth Annu. ACM Symp. Principles of Programming Languages, Austin, TX, Jan. 1989, pp. 267-280.
[8] M. C. Browne and E. M. Clarke, "From HDL descriptions to guaranteed correct circuit designs," inSML--A High Level Language for the Design and Verification of Finite State Machines. North-Holland, 1987, pp. 269-292.
[9] J. R. Burch, E. M. Clarke, and D. E. Long, "Representing circuits more efficiently in symbolic model checking," inProc. 28th ACM-IEEE Design Automation Conf., IEEE Computer Society, June 1991.
[10] J. B. Burchet al., "Symbolic model checking: 1020states and beyond," inProc. 5th Symp. Logics in Computer Science, pp. 428-439, IEEE Computer Society Press, 1990.
[11] E. J. Cameron, D. M. Cohen, T. M. Guinther, W. M. Keese, Jr., L. A. Ness, C. Norman, and H. N. Srinidhi, "The 1.0 language and environment for protocol simulation and prototyping,"IEEE Trans. Comput., vol. 40, pp. 562-571, Apr. 1991.
[12] E. J. Cameron, L. A. Ness, A. P. Sheth, and M. Rusinkiwicz, "An executor for multidatabase transactions which achieves maximal parallelism," inProc. First Int. Workshop Interoperability in Multidatabase Systems, Apr. 7-9, 1991, pp. 268-275.
[13] E. Clarke, "Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach," inProc. 10th ACM Symp. Princ. Programming Languages, 1983, pp. 117-127.
[14] E. M. Clarke, O. Grumberg, and D. E. Long, "Model checking and abstraction," inProc. 19th Annu. Symp. Principles of Programming Languages, Jan. 1992.
[15] D. M. Cohen and E. J. Isganitis, "Automatic generation of a prototype of a new protocol from its specification," inProc. IEEE Global Telecommunications Conf., Dec. 1986.
[16] D. M. Cohen, "The 1.0 execution model and its parallel implementation," Bellcore, Tech. Rep., 1991.
[17] J. Davies and S. Schneider,An Introduction to Timed CSP, 1988.
[18] P. Degano, R. De Nicola, and U. Montanari, "Partial ordering descriptions and observations of nondeterministic concurrent processes," inProc. Workshop Noordwijkerhout, The Netherlands, (Lecture Notes in Computer Science, vol. 354). New York: Springer-Verlag, 1988, pp. 438-467.
[19] E. A. Emerson,Handbook of Theoretical Computer Science: Volume B, Formal Models and Semantics. Cambridge, MA: MIT Press, 1990.
[20] M. Fujita, S. Kono, H. Tanaka, and T. Moto-oka, "Tokio: Logic programming language based on temporal logic and its compilation to PROLOG," inThird Int. Conf. Logic Programming, 1986, pp. 695-709.
[21] D. Gabbay, "Declarative past and imperative future: Executable temporal logic for interactive systems," inProc. Colloquium Temporal Logic in Specification, B. Banieqbal, H. Barringer, and A. Pnueli, Eds., Altrincham, 1987, pp. 402-450, Springer-Verlag, LNCS vol. 398, 1989.
[22] A. Galton, Ed.,Temporal Logics and their Applications. New York: Academic, 1987.
[23] J. A. Goguen and J. Meseguer, "Models and equality for logical programming," inProc. Int. Joint Conf. Theory and Practice of Software Development, Pisa, Italy, Mar. 23-27, 1987.
[24] N. Halbwachs, D. Pilaud, F. Ouabdesselam, and A.-C. Glory, "Specifying, programming and verifying real-time systems using a synchronous declarative language," inProc. Workshop Automatic Verification of Finite State Systems, Grenoble, France, 1989.
[25] E. Harel, O. Lichtenstein, and A. Pnueli,Explicit Clock Temporal Logic, 1990.
[26] Z. Har'El and R. P. Kurshan, "Software for analytical development of communication protocols,"AT&T Tech. J., Jan. 1990.
[27] D. M. Jackson, "Specifying timed communicating sequential processes using temporal logic."
[28] J. Katznelson and R. P. Kurshan, "S/r: A language for specifying protocols and other communications software," inProc. 5th Annu. Int. Phoenix Conf. Comput. Commun., IEEE, 1986, pp. 286-292.
[29] R. P. Kurshan, "Reducibility in analysis of coordination," inDiscrete Event Systems: Models and Applications. New York: Springer-Verlag, 1988, pp. 19-39.
[30] R. P. Kurshan, "Analysis of discrete event coordination," inLecture Notes in Computer Science, vol. 430. New York: Springer-Verlag, 1990, pp. 414-453.
[31] O. Lichtenstein, A. Pnueli, and L. Zuck, "The glory of the past," inConf. Logics of Programs, LNCS 194. Springer Verlag, 1985.
[32] L. Ness, "Issues arising in the analysis of L.0," inProc. DIMACS:Computer Aided Verification Workshop. Rutgers Univ., Piscataway, NJ, June 18-21, 1990, to appear in Springer Lecture Notes.
[33] J. McCarthy and P. J. Hayes, "Some philosophical problems from the standpoint of artificial intelligence,"Mach. Intell., vol. 4, pp. 463-502, 1969.
[34] K. L. McMillan and J. Schwalbe, "Formal verification of the encore gigamax cache consistency," inProc. Int. Symp. Shared Memory Multiprocessors, Apr. 1991.
[35] K. L. McMillan, "Symbolic model checking: An approach to the state explosion problem," Ph.D. dissertation, Carnegie-Mellon Univ., May 1992.
[36] U. Montanari and F. Rossi, "Graph rewriting for a partial ordering semantics of concurrent constraint programming," inProc. Int. Logic Programming Symp., Cambridge, MA: MIT Press, Oct. 1991.
[37] B. Moszkowski,Executing Temporal Logic Programs. Cambridge, UK: Cambridge University Press, 1987.
[38] L. Ness, "A quantified synchronous model of parallel programming which permits checking of a class of extended temporal logic assertions," Bellcore, Tech. Memo., 1990.
[39] L. Ness and J. Vollaro, "Two approaches to the validation of futurebus+," inProc. Tau 92: 1992 Workshop Timing Issues in the Specification and Synthesis of Digital Systems, 1992.
[40] D. Pilaud and N. Halbwachs, "From a synchronous declarative language to a temporal logic dealing with multiform time," inProc. Symp. Formal Techniques in Real Time and Fault Tolerant Syst., Warwick, England, Sept. 1988.
[41] A. Pnueli, "The temporal logic of programs," inProc. 18th Annu. Symp. Foundations of Computer Science, 1977, pp. 46-57.
[42] A. Pnueli, "Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of CurrentTrends," inCurrent Trends in Concurrency: Overviews and Tutorials. W.-P. de Roever and G. Rozenberg, eds., Lecture Notes in Computer Science 224, Springer-Verlag, N.Y., 1986, pp. 510-584.
[43] C. Ratel, N. Halbwachs, and P. Raymond, "Programming and verifying critical systems by means of the synchronous data-flow programming language lustre," inACM-SIGSOFT'91 Conf. Software for Critical Systems, Dec. 1991.
[44] N. Rescher and A. Urquhart,Temporal Logic. New York: Springer-Verlag, 1971.
[45] J. L. Richier, C. Rodriguez, J. Sifakis, and J. Voiron, "Verification in xesar of the sliding window protocol, " inIFIP WG-6.1 7th Int. Conf. Protocol Specification, Testing and Verification. North Holland, 1987.
[46] P. Wolper, "Temporal logic can be more expressive,"Inform. Contr., vol. 56, pp. 72-99, 1983.

Index Terms:
L.0; truly concurrent executable temporal logic language; protocols; specification; simulation; true concurrency model; execution algorithm; standard imperative programming; state predicates; equality predicates; hierarchical message structure; Futurebus+; protocols; simulation languages; specification languages; temporal logic
Citation:
L. Ness, "L.0: A Truly Concurrent Executable Temporal Logic Language for Protocols," IEEE Transactions on Software Engineering, vol. 19, no. 4, pp. 410-423, April 1993, doi:10.1109/32.223807
Usage of this product signifies your acceptance of the Terms of Use.