Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computer Science
  4. Computer Science Technical Reports
  5. A Temporal-Logic Based Compositional Proof System for Real-Time Message Passing

A Temporal-Logic Based Compositional Proof System for Real-Time Message Passing

File(s)
88-919.pdf (1.76 MB)
88-919.ps (496.89 KB)
Permanent Link(s)
https://hdl.handle.net/1813/6759
Collections
Computer Science Technical Reports
Author
Hooman, Jozef
Widom, Jennifer
Abstract

We consider a model of real-time network computation in which synchronous communication events occur during (possibly overlapping) intervals along a dense time scale. A specification language for processes and networks based on real-time temporal logic is defined. We give a simple proof system for network specifications when specifications for component processes are given. The proof system is then extended for a version of real-time CSP, under the assumption that all communications take some fixed length of time. Finally, it is shown that this proof system can be modified to allow varying communication lengths. All versions of the proof system are compositional, sound, and relatively complete.

Date Issued
1988-06
Publisher
Cornell University
Keywords
computer science
•
technical report
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR88-919
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance