Specification and Verification of Liveness Properties of Cyclic, Concurrent Processes

3Citations
Citations of this article
12Readers
Mendeley users who have this article in their library.

Abstract

A technique is described for software specification and verification of concurrent, distributed systems. The complete specification of a program is given in terms of a hierarchical structure of module specifications. Module external specifications are abstract; module internal specifications are descriptions of internal implementations, either in terms of submodules or actual code. The verification that an implementation satisfies its specification is language independent for the former and language dependent for the latter. Distinguishing the liveness properites provided by a module and the liveness properties required by a module (from its comodules) allows the specification and verification of a given module to be independent from the specification and verification of its comodules. © 1988, ACM. All rights reserved.

Author supplied keywords

Cite

CITATION STYLE

APA

Reed, J., & Yeh, R. T. (1988). Specification and Verification of Liveness Properties of Cyclic, Concurrent Processes. ACM Transactions on Programming Languages and Systems (TOPLAS), 10(1), 156–177. https://doi.org/10.1145/42192.42195

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free