Checking Integral Real-Time Automata for Extended Linear Duration Invariants

Linear duration invariants are important safety properties of real-time systems. They are represented as linear inequalities of integrated durations of system states and form a decidable subclass of Duration Calculus formulas. The problem of whether a real-time automaton satisfies a linear duration invariant can be transformed into a finite number of linear programming problems. In this paper, extended linear duration invariants, which are linear inequalities of integrals of physical quantities that characterize real-time systems, are introduced. The semantics of extended linear duration invariants is defined by introducing integral real-time automata whose states are labeled with a finite number of integrable functions. The problem of checking an integral real-time automaton for an extended linear duration invariant is transformed into a finite number of nonlinear programming problems which can be solved easily. A case study of a reaction tank is discussed to demonstrate the effectiveness of the technique introduced in the paper.