Document Type

Conference Proceeding

Department

Computer Science (HMC)

Publication Date

3-1981

Abstract

This paper presents a technique for specifying and verifying properties of "sentinels," a high-level language construct for synchronizing access to shared resources. Statements in the specification language possess formal temporal semantics. As a prelude to proving the correctness of sentinels, the semantics of constructs used in sentinels is given. The proof technique involves showing that the temporal behavior of a sentinel conforms to that defined by the specification. The methodology is illustrated by applying it to a typical synchronization problem.

Comments

Previously linked to as: http://ccdl.libraries.claremont.edu/u?/irw,352.

Pdf created from the Proceedings of the 5th International Conference on Software Engineering, (IEEE, Mar. 1981).

Rights Information

© 1981 Institute of Electrical and Electronics Engineers (IEEE). Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE. This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Terms of Use & License Information

Terms of Use for work posted in Scholarship@Claremont.

Download

Share

COinS