Automatic Verification of Serializers.

Abstract

This thesis is concerned with the problem of controlling concurrent access to shared data. A language construct is proposed to enforce such control; a specification language is defined to describe the formal requirements of such control; and verification techniques are given to prove that instances of the construct satisfy their specifications. The techniques are justified in terms of the definition of the construct and the definition of the specification language. Results are given for a program that implements a number of the techniques, illustrated by verifying several versions of the readers-writers problem. Interactions between instances of the construct are discussed in the context of a simple file system. (Author)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 01, 1980
Accession Number
ADA082885

Entities

People

  • Russell Roger Atkinson

Organizations

  • Massachusetts Institute of Technology

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Algorithms
  • Artificial Intelligence
  • Computations
  • Computer Programming
  • Computer Science
  • Computers
  • Databases
  • Language
  • Military Research
  • Models
  • Network Protocols
  • New York
  • Programming Languages
  • Semantic Models
  • Software Development
  • Structured Programming
  • Test And Evaluation

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Parallel and Distributed Computing.