Development of real-time system specifications through the refinement of duration interval Petri nets

This paper aims at the development of an engineering technique for the construction of systems through the refinement of duration interval transitions. The theoretical system model is based on so-called interval time Petri nets. Duration interval transitions turn out to be a syntactical abbreviation for a certain structure of interval time Petri nets. The kind of refinement technique preserves the safety property and guarantees that the refined system behaves neither slower nor faster than the unrefined one. The application of our approach lies in the development of time correct system specifications.