Functional specification and proof of correctness for time dependent behaviour of reactive systems
Tóm tắt
A functional formalism for describing and reasoning about the time dependent behaviour of reactive systems is presented. The model is event based and can describe the histories of events with finite duration. It is a generalisation of the model of Caspi and Halbwachs (1986). A set of tools with their operations are introduced in the formalism and structure theorems characterising the algebra of events are proved. The power of this extended model is illustrated through the formal specification and correctness proof for a problem chosen from robotics.
Từ khóa
Tài liệu tham khảo
Alagar V. S. and Ramanathan G.: Formal Environment and Tools Description for the Analysis of Real-Time Concurrent Systems. Workshop on the Specification and Verification of Concurrent Systems 1988. Also appears in BCS-FACS Workshop Series 1 (1989) and in Specification and Verification of Concurrent Systems C. Rattray (ed.) Springer Verlag 1990.
Capsi P., 1986, Functional Model for Describing and Reasoning about Time Behaviour of Computing Systems, Acta Inforamtica, 22, 595, 10.1007/BF00263648
Fishburn P. C.: Interval Orders and Interval Graphs: a Study of Partially Ordered Sets John-Wiley 1985.
Koymans R. and de Roever W. P. Examples of Real-time Temporal Logic Specification. Workshop on the Analysis of Concurrent Systems 1983.
Liu L. Y., 1988, Technical Report
Ould Kaddour N. and Courvoisier M.: Issues for Concurrent Programming Real-Time Systems. IEEE Int. Conf. on Robotics and Automation pp. 1469–1474 1987.
Pnueli A.: Aplications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends . Lecture Notes in Computer Science 224 pp. 511–584 Springer-Verlag 1986.
Ramanathan G., 1988, Ph.D. Thesis
Sanchis L. E., 1977, Data Types as Lattices: Retractions, Closures and Projection, RAIRO Theoretical Computer Science, 11, 329
Wiener N., 1914, A Contribution to the Theory of Relative Positions, Proc. Camb. Philos. Soc., 17, 441
Winskel G.: Event Structures. In: Petri Nets: Applications and Relationship to other Models of Concurrency Lecture Notes in Computer Science 255 pp. 325–392 Springer-Verlag 1986.