Derivation of Sequential, Real-Time, Process-Control Programs

Abstract

The use of weakest precondition predicate transformers in the derivation of sequential, process control software is discussed. Only one extension to Dijkstra's calculus for deriving ordinary sequential programs was found to be necessary: function-valued auxiliary variables. These auxiliary variables are needed for reasoning about states of a physical process that exist during program transitions.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 01, 1991
Accession Number
ADA238877

Entities

People

  • Fred B. Schneider
  • Keith Marzullo
  • Navin Budhiraja

Organizations

  • Cornell University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Actuators
  • Calculus
  • Computer Science
  • Computers
  • Control Systems
  • Coordinate Systems
  • Corporations
  • Equations
  • Fault Tolerance
  • Military Research
  • New York
  • Railroad Tracks
  • Railroads
  • Reasoning
  • Specifications
  • Transformers

Readers

  • Mathematical Modeling and Probability Theory.