Formal Specification and Verification of Concurrent Programs

Abstract

This module introduces formal specification of concurrent software and verification of the consistency between concurrent programs and their specifications. First, what one might want to be able to prove about a concurrent program is discussed. Then, a number of formal descriptions of the concept are presented. These vary in their coverage of the phenomena, and some can be used as the bases of formal specification of programs. Next, techniques for carrying out the proof of consistency between the specification and the program are described. Finally, it is noted that some of these techniques have automated tools such as verifiers associated with them.... Concurrent programs, Multiprocessing, Formal specification, Multitasking, Formal verification, Semantics of concurrency

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 01, 1993
Accession Number
ADA265201

Entities

People

  • Daniel M. Berry

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • C4I
  • Energy and Power Technologies
  • Human Systems

DTIC Thesaurus Topics

  • Birds
  • Communication Channels
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Electronic Mail
  • Information Science
  • Lisp Programming Language
  • Network Science
  • Operating Systems
  • Personnel Management
  • Programming Languages
  • Robotics
  • Software Development
  • User Interface
  • Web Browsers

Fields of Study

  • Computer science
  • Engineering

Readers

  • Computer Science.
  • Mathematical Modeling and Probability Theory.
  • Parallel and Distributed Computing.