A Transformational Method for Verifying Safety Properties in Real Time Systems

Abstract

The behavior of systems with hard real-time constraints can be specified in terms of Hierarchical Multi-State (HMS) abstract machines, which are generalizations of finite-state automata. In this paper, a two-step method is presented for verifying that safety properties are not violated by an HMS specification fo a system. In the first step, the safety verification question is recast as a reachability problem in an extension of the HMS machine. In the second step, reachability is determined by the use of correctness-preserving and partial correctness-preserving transformations. The method is shown to be complete, and it is illustrated by verifying that a safety property holds for a simple railroad-crossing system if all of its deadlines are met.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 01, 1989
Accession Number
ADA211925

Entities

People

  • Armen Gaberielian
  • Matthew K. Franklin

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Automata
  • Computer Programming
  • Computer Science
  • Computers
  • Consistency
  • Crossings
  • Invariance
  • Language
  • Machines
  • Military Research
  • Modular Construction
  • Petri Nets
  • Programming Languages
  • Railroads
  • Sequences
  • Software Development
  • Specifications

Fields of Study

  • Computer science
  • Engineering

Readers

  • Environmental Engineering.
  • Mathematical Modeling and Probability Theory.
  • Software Engineering.