Timed API rules for runtime verification

• US 9,519,495 B2
• Filed: 06/14/2013
• Issued: 12/13/2016
• Est. Priority Date: 06/14/2013
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Inventors: Levin, Vladimir A., Li, Juncao, Lichtenberg, Jakob Frederik
• Primary Examiner(s): Chen, Qing
• Assistant Examiner(s): THATCHER, CLINT A
• Application Number:
  US13/918,857
• Publication Number:
  US 20140372986A1
• Time in Patent Office: 1,278 Days
• Field of Search: 717/126
• US Class Current: 1/1
• CPC Class Codes: G06F 11/3612 by runtime analysis performance monitoring G06F11/3466
• CPC Class Codes: G06F 9/44589 Program code verification, e.g. Java bytecode verification, proof-carrying code high-level semantic checks G06F8/43; testing and debugging software G06F11/36

Abstract

A stateful rules verification platform is described that support timed state transitions. The verification platform implements a specification language to provide a formal definition for rules used to test target systems having a central module that provides APIs (“API provider”) and applications (“API clients”) that use the APIs. Rules may be defined in terms of transitions on state elements associated with interactions between API providers and API clients. The rules defined in accordance with the specification language enable run-time verification in which calls may be intercepted and run-time code to implement checks may automatically be generated and injected to test behaviors of the intercepted calls. The same set of rules may also be employed for static verification during compilation. Additionally, the specification language includes constructs to specify timed state transitions for at least some rules that impose time limits on state transitions specified by the rules.

Claims

1. A computing system including one or more computing devices comprising:

one or more processing systems; and

one or more computer-readable storage media storing instructions executable by the one or more processing systems to implement;

a target system for verification including an application programming interface (API) provider that exposes one or more APIs and one or more API clients that use the APIs;

a rules specification language configured to define stateful rules for runtime verification of the target system including constructs to specify timed state transitions for at least some of the stateful rules, the rules specification language supporting predictive evaluation timing in which an indication of when to evaluate the timing for the timed state transitions is included within corresponding stateful rules;

one or more of the stateful rules including one or more rules that specify timed state transitions for verification of the target system defined in accordance with the rules specification language; and

a run-time verifier module configured to apply the one or more stateful rules to generate verification checks for interactions between the API provider and the API clients for run-time verification of the target system to verify adherence to the stateful rules prescribed for the target system, the run-time verifier module comprising an interceptor module configured to intercept calls to APIs issued by the API clients or calls to the API clients from the API provider and initiate application of corresponding verification checks based on the calls that are intercepted.

2. The computing system as described in claim 1, wherein the stateful rules are defined using the rules specification language as transitions on state elements associated with the interactions between the API provider and the one or more API clients.

3. The computing system as described in claim 2, wherein the timed state transitions impose timing constraints upon corresponding transitions on the state elements associated with the interactions between the API provider and the one or more API clients.

4. The computing system as described in claim 1, wherein the timed state transitions are configured to detect situations in which expected states of finite state machines associated with corresponding stateful rules are not reached within prescribed time limits.

5. The computing system as described in claim 1, wherein the constructs to implement the timed state transitions enable explicit definition of a time limit to associate with a transition from a source state to a destination state.

6. The computing system as described in claim 1, wherein the constructs to implement the timed state transitions include a timing parameter to store a timestamp associated with a source state for comparison to a current time in relation to time limits defined for the timed state transitions.

7. The computing system as described in claim 1, wherein evaluation of the timing for the timed state transitions that are specified includes setting a different local timer for each timed state transition that increments when a thread for the local timer is allocated processing resources and is suspended when the thread is suspended.

8. The computing system as described in claim 1, wherein evaluation of the timing for the timed state transitions comprises setting a global timer for the timed state transitions and evaluating local timers associated with each timed state transition at an evaluation interval controlled according to the global timer.

9. The computing system as described in claim 1, wherein timers used to implement the evaluation of one or more of said timed state transitions are assigned a lowest available priority to prevent misrecognition of hangs due to preemptive scheduling.

10. The computing system as described in claim 1, wherein the run-time verifier module includes a checker module that is configured to:

retrieve definitions for the stateful rules that are identified as applicable to the target system; and

automatically derive corresponding verification checks from the definitions of the stateful rules that are retrieved, the verification checks including code to implement the timed state transitions defined by the stateful rules.

18. The computing system as described in claim 1, the run-time verifier module further configured to fire an event to trigger a corresponding reaction responsive to APIs of the target system failing to execute within the timed state transitions specified by the rules.

11. A method implemented by one or more computing devices comprising:

implementing a rules specification language to define rules for application programming interface (API) run-time verification of target systems in terms of transitions for state machines associated with events and that supports timed state transitions for the rules, the rules specification language supporting predictive evaluation timing in which an indication of when to evaluate the timing for the timed state transitions is included within corresponding rules;

creating one or more of the rules for run-time verification of the target systems that specify the timed state transitions in accordance with the rules specification language;

performing the API run-time verifications of the target systems using the one or more rules that specify the timed state transitions, the timed state transitions imposing timing constraints upon corresponding transitions for the state machines associated with interactions between API providers and one or more API clients of the target systems;

monitoring conditions in which an API of the target systems fails to execute within constraints imposed by the specified timed state transitions; and

responsive to the API of the target system failing to execute within the timed state transitions specified by the rules, firing an event to trigger a corresponding reaction.

12. A method as described in claim 11, wherein performing the API run-time verifications of the target systems using the one or more rules that specify the timed state transitions comprises:

instantiating one or more timers for the timed state transitions to track timing of the interactions in the target system; and

evaluating the one or more timers to verify compliance with the timing constraints imposed by the one or more rules upon the transitions for the state machines.

13. A method as described in claim 11, wherein the API run-time verifications comprise verifications of drivers that interact with system APIs provided by an operating system of the computing device.

20. A method as described in claim 11, wherein performing the API run-time verifications of the target systems comprises:

intercepting calls to the APIs issued by the one or more API clients or calls to the one or more API clients from the API providers.

14. One or more computer-readable storage media storing instructions that, when executed by one or more components of a computing system, implement a verification platform configured to perform operations including:

deriving verification checks for run-time verification of a target system from stateful rules including at least some rules that impose time limits on state transitions defined by the rules;

initiating timers for one or more state transitions upon which time limits are imposed in connection with run-time verification of a target system, at least one of the time limits being hardware specific and based on protocols defined for interaction involving the specific hardware;

express the stateful rules in relation to application programming interface (API) interactions of API clients with an API provider of the target system in terms of the one or more state transitions that occur for state machines associated with the API interactions, the stateful rules defined in accordance with a specification language that supports predictive evaluation timing in which an indication of when to evaluate the timing for timed state transitions is included within corresponding stateful rules;

evaluating the timers initiated for the one or more state transitions relative to corresponding time limits; and

responsive to the one or more state transitions failing to execute within the corresponding time limits specified by the rules, firing an event to trigger a corresponding reaction.

15. One or more computer-readable storage media as recited in claim 14, wherein the stateful rules are further defined in accordance with the specification language configured to at least:

provide constructs to specify the time limits imposed on the state transitions; and

implement a formalized description and comment structure for the stateful rules to facilitate specification of the corresponding reaction occurring responsive to the one or more state transitions failing to execute within the time limits imposed on the state transitions.

16. One or more computer-readable storage media as recited in claim 14, wherein deriving verification checks for run-time verification of the target system comprises:

identifying stateful rules implicated by interactions of components of the target system;

deriving run-time code to implement the verification checks for the identified stateful rules from definitions of the identified rules, the definitions specifying the time limits to impose on state transitions defined by the rules; and

injecting the run-time code to implement the verification checks into the target system.

17. One or more computer-readable storage media as recited in claim 14, wherein:

initiating the timers includes instantiating one or more local timers for each of the one or more state transitions upon which the time limits are imposed and a global timer to implement a periodic interval for evaluation of the local timers to check compliance with corresponding time limits; and

evaluating the timers includes comparing the one or more local timers to corresponding time limits at the periodic interval implemented by the global timer.

19. One or more computer-readable storage media as recited in claim 14, wherein evaluating the timers includes:

intercepting calls to APIs issued by the API clients or calls to the API clients from the API provider; and

applying the one or more stateful rules to generate verification checks for interactions between the API provider and the API clients for run-time verification of the target system to verify adherence to the stateful rules prescribed for the target system.