Title :
Static analysis and dynamic steering of time-dependent systems
Author_Institution :
Dept. of Syst. & Inf., Florence Univ., Italy
fDate :
8/1/2001 12:00:00 AM
Abstract :
An enumerative technique is presented which supports reachability and timeliness analysis of time-dependent models. The technique assumes a dense model of time and uses equivalence classes to enable discrete and compact enumeration of the state space. Properties of timed reachability among states are recovered through the analysis of timing constraints embedded within equivalence classes. In particular, algorithms are given to evaluate a tight profile for the set of feasible timings of any untimed run. Runtime refinement of static profiles supports a mixed static/dynamic strategy in the development of a failure avoidance mechanism for dynamic acceptance and a guarantee of hard real-time processes
Keywords :
Petri nets; equivalence classes; program diagnostics; reachability analysis; real-time systems; compact enumeration; dense model; dynamic acceptance; dynamic steering; enumerative technique; equivalence classes; failure avoidance mechanism; feasible timings; hard real-time processes; mixed static/dynamic strategy; reachability; runtime refinement; state space; static analysis; static profiles; tight profile; time-dependent models; time-dependent systems; timed reachability; timeliness analysis; timing constraints; untimed run; Computer Society; Petri nets; Polynomials; Real time systems; Runtime; Scheduling; State-space methods; Testing; Time factors; Timing;
Journal_Title :
Software Engineering, IEEE Transactions on