Patent ID: 8484009

Claim:
A method for performing timing analysis of an embedded system comprising: providing a system description; providing an analysis specification for the system; automatically generating a formal model of the system from the system description and the analysis specification using a model generator; wherein the formal model includes a calendar automaton model and instrumentation; analyzing the formal model of the system using a model checker; optimizing the calendar automaton model by at least one of: computing a spill time associated with a task; and dynamically computing response time of the task using the spill time; wherein w = spill + E j + ∑ l ∈ hp ⁡ ( j ) ⁢ ⌈ w - O l ′ T l ⌉ * E l where w represents the computed response time of τ j , E j is the worst case execution time of τ j , hp(j) is the set of all tasks with higher priority than τ j , O′ l represents the next activation offset of τ l from current time, T l represents the period of τ l and E l , represents the worst case execution time of τ l , Spill, for a given task activation instance, is defined as the remaining execution time of an immediate higher priority task that is in the state of execution; and providing results of the analysis.