We present a program analysis for verifying quantitative robustness properties of programs, stated generally as: "If the inputs of a program are perturbed by an arbitrary amount epsilon, then its outputs change at most by (K . epsilon), where K can depend on the size of the input but not its value." Robustness properties generalize the analytic notion of continuity---e.g., while the function ex is continuous, it is not robust. Our problem is to verify the robustness of a function P that is coded as an imperative program, and can use diverse data types and features such as branches and loops.

Constraint automata as acceptors of timed data streams are the semantic models of component connectors specified in the language of Reo. In this paper, we investigate the augmentation of the theory of constraint automata by live- ness and fairness requirements. We define the notion of liveness for constraint automata as a set of infinite runs and show that our definitions of weak and strong fairness requirements, as we expect, satisfy the liveness requirements. It is shown that live or fair constraint automata can be composed using extended versions of the join operator for ordinary constraint automata such that, the resulted automaton itself be live or fair, respectively. Also, we present a linear temporal logic interpreted over infinite strings of transitions of constraint automata as a specification language for their properties. This temporal logic can be used as the specification language in the field of model checking. We show that our defined fairness conditions can be expressed not only by sets of computations but also by temporal formulas in the proposed linear temporal logic of steps.