Duration properties over real time system designs

Constraints on the accumulated sojourn time at particular system states are among the possible requirements for a real-time system. These requirements are called duration properties. The need to predict temporal behavior of critical real-time systems has encouraged the development of a useful collection of results for nln-time scheduling as well as an interesting set of formal automatic techniques based on model-checking. However no automatic technique directly supports the verification of duration requirements over physical designs of real-time software. In [6] it is presented an approach that applies known scheduling theory to automatically derive simple and compositional formal models based on timed automata [I]. In this article, we corn bine that modeling method with a conservative algorithm that extends [5] to check duration properties over the resulting timed automata.