METHOD AND APPARATUS FOR THE FORMAL SPECIFICATION AND ANALYSIS OF TIMING PROPERTIES IN SOFTWARE SYSTEMS
A method and apparatus is disclosed herein for formal specification and analysis of timing properties. In one embodiment, the method comprises receiving a software design that includes timing behaviors expressed in a specification language; analyzing the timing behaviors; and using abstract interpretation based static analysis to detect misuses of one or more timing constructs.
1 . A method comprising:
receiving a software design that includes timing behaviors expressed in a specification language;
analyzing the timing behaviors; and
using abstract interpretation based static analysis to detect misuses of one or more timing constructs.
2 . The method defined in claim 1 wherein analyzing the timing behaviors is based on abstracting timer values for model-checking.
3 . The method defined in claim 2 further comprising using a timed model checker to verify timing properties of specifications.
4 . The method defined in claim 1 wherein analyzing the timing behaviors is performed using abstract interpretation based static analysis.
5 . The method defined in claim 1 wherein the timing behaviors are derived from at least one timer, the timer being a data structure associated with a timer value and being set and released via separate operations, the timer value being modified based on clock ticks, and further wherein the timer is consumable after expiration.
6 . The method defined in claim 1 wherein misuses of one or more timing constructs comprises mishandling of one or more timers.
7 . The method defined in claim 6 wherein mishandling of one or more timers are due to one of a group consisting of: an unreachable or superfluous code having a timer, code having extra release commands associated with a timer; and code having an unhandled timer.
8 . The method defined in claim 1 wherein the static analysis computes, at each point in a specification, a set of one or more timers that may not have been handled properly on a path to that point in the specification.
9 . The method defined in claim 1 wherein the static analysis is performed using a control flow graph representing a specification.
10 . The method defined in claim 9 further comprising building a graph with a set of nodes and directed edges grouped together and specifying computation of fixed points.
11 . An article of manufacture having one or more storage media storing instructions thereon which, when executed by a system, cause the system to perform a method comprising:
receiving a software design that includes timing behaviors expressed in a specification language;
analyzing the timing behaviors; and
using abstract interpretation based static analysis to detect misuses of one or more timing constructs.
12 . The article of manufacture defined in claim 11 wherein analyzing the timing behaviors is based on abstracting timer values for model-checking.
13 . The article of manufacture defined in claim 12 wherein the method further comprises using a timed model checker to verify timing properties of specifications.
14 . The article of manufacture defined in claim 11 wherein analyzing the timing behaviors is performed using abstract interpretation based static analysis.
15 . The article of manufacture defined in claim 11 wherein the timing behaviors are derived from at least one timer, the timer being a data structure associated with a timer value and being set and released via separate operations, the timer value being modified based on clock ticks, and further wherein the timer is consumable after expiration.
16 . The article of manufacture defined in claim 11 wherein misuses of one or more timing constructs comprises mishandling of one or more timers.
17 . The article of manufacture defined in claim 16 wherein mishandling of one or more timers are due to one of a group consisting of: an unreachable or superfluous code having a timer, code having extra release commands associated with a timer; and code having an unhandled timer.
18 . The article of manufacture defined in claim 11 wherein the static analysis computes, at each point in the specification, a set of one or more timers that may not have been handled properly on a path to that point in the specification.
19 . The article of manufacture defined in claim 11 wherein the static analysis is performed using a control flow graph representing the specification.
20 . The article of manufacture defined in claim 19 wherein the method further comprises building a graph with a set of nodes and directed edges grouped together and specifying computation of fixed points.
21 . An apparatus comprising:
a memory to store executable instructions and data; and
a processor coupled to the memory, to execute the instructions to perform a method that includes
receiving a software design that includes timing behaviors expressed in a specification language;
analyzing the timing behaviors; and
using abstract interpretation based static analysis to detect misuses of one or more timing constructs.