Towards Derivation of Real-Time Process-Control Programs

Abstract

The use of weakest-precondition predicate transformers in the derivation of sequential, process-control software is discussed. Only the 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. Keywords: Real-time software, Process-control software, Weakest preconditions, Auxiliary variables, Program verification.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 11, 1990
Accession Number
ADA228281

Entities

People

  • Fred B. Schneider
  • Keith Marzullo

Organizations

  • Cornell University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Actuators
  • Calculus
  • Classification
  • Computer Science
  • Computers
  • Fault Tolerance
  • Mathematics
  • New York
  • Railroad Tracks
  • Railroads
  • Reasoning
  • Security
  • Specifications
  • Transformers
  • Transitions
  • Universities

Readers

  • Database Systems and Applications
  • Mathematical Modeling and Probability Theory.