Verification of Real-Time Systems using Linear Relation Analysis

Abstract:
Linear Relation Analysis is an abstract interpretation devoted to the automatic discovery of invariant linear inequalities among numerical variables of a program. In this paper, we apply such an analysis to the verification of quantitative time properties of two kinds of systems: synchronous programs and linear hybrid systems.

Reference:

@article{polka:fmsd:97,
author={N. Halbwachs and Y.E. Proy and P. Roumanoff},
title={Verification of real-time systems using
       linear relation analysis},
journal={Formal Methods in System Design},
year={1997},
month={August},
volume={11},
number={2},
pages={157--185},
publisher={Kluwer},