L.0(ID:5513/l::008)parallel executable temporal logic language Jane Cameron, David Cohen, B. Gopinath, Linda Ness. References: Introduction The purpose of this paper is to present the subset of temporal logic, that has been found useful and accessible to programmers of communications software, and to present the additional assumptions and structuring operators which had to be added to make this subset into a viable programming language. The resulting language is called L.0. The fact that enhancements to temporal logic are necessary to make it a viable programming language should not be surprising, since a standard criticism of temporal logic is that it is: global, non-modular, and non-compositional. A somewhat restricted first version is currently in use at Bellcore as an executable specification and prototyping language. The applications of L.0 include specification of communications protocols, services, and network performance models. A brief overview of the structure of the applications of the language will be presented at the end of the paper. The design decisions of L.0, which will be discussed in this paper include: the particular subset of temporal formulas allowed, the particular restricted form of quantification used, the choice of the structure for the states, the choice of the set of atomic predicates, the introduction of structuring operators, and the particular solution to the frame problem chosen. The reason that a solution to the frame problem is needed is that an L.0 specification is viewed as forcing changes in the previous state, rather than completely specifying each state. One apparent valuable side- effect of these choices is to make temporal formulas rcadablc and writable, by industrial programmers. The close fit between L.0 and temporal logic is especially interesting because the design and development process of L.0 have been user-centered. The control and structuring constructs were designed to be compatible with a programmers intuitive operational view of the problem. Various user groups within Bellcore have used L.0, and its predecessor C&E to specify prototypes of communications software. The restrictions of the temporal constructs are directly traceable to specific problems encountered by the users. It is not surprising that a language designed for the specification of various types of communications software, which are reactive systems, should be fundamentally related to temporal logic. For the problem of specification and verification of reactive systems has been one of the principal motivations and primary applications of temporal logic. in ACM SIGSOFT Software Engineering Notes , Conference proceedings on Formal methods in software development April 1990 15(4) view details |