A Scheduling Approach to Verifying Safety in Real-Time Systems
Armen Gabrielian · Defense Technical Information Center (DTIC) · 1992
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.