A Scheduling Approach to Verifying Safety in Real-Time Systems

Abstract

A general method for reasoning about the behavior of real-time systems is presented using hierarchical multi-state (HMS) machines. The method is based on a parametric scheduling approach that reduces the problem of verification of safety properties of concurrent systems to the solution of a set of inequalities. The method is applied to obtain a very simple solution to the problem of safety of a real-time concurrent mutual exclusion protocol that has been studied by a number of authors recently.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1992
Accession Number
ADA251644

Entities

People

  • Armen Gabrielian

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Automata
  • Automata Theory
  • Computations
  • Computer Science
  • Inequalities
  • Intervals
  • Language
  • Machines
  • Notation
  • Petri Nets
  • Scheduling (Production)
  • Software Development
  • Specifications
  • Standards
  • Time Domain
  • Transitions
  • Verification

Fields of Study

  • Computer science

Readers

  • Mathematical Modeling and Probability Theory.
  • Software Engineering.