Behavioral analysis for message-passing application programs

• US 20030204570A1
• Filed: 04/30/2002
• Published: 10/30/2003
• Est. Priority Date: 04/30/2002
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: Rajamani, Sriram K., Rehof, Jakob
• Granted Patent: US 7,203,924 B2
• Time in Patent Office: Days
• US Class Current: 709/207
• CPC Class Codes: G06F 11/3608 using formal methods, e.g. model checking, abstract interpretation theorem proving G06N5/013
• CPC Class Codes: G06F 9/546 Message passing systems or structures, e.g. queues
• CPC Class Codes: H04L 67/10 in which an application is distributed across nodes in the network software deployment G06F8/60; multiprogramming arrangements G06F9/46
• CPC Class Codes: H04L 67/133 Protocols for remote procedure calls [RPC]
• CPC Class Codes: H04L 69/329 in the application layer [OSI layer 7]
• CPC Class Codes: H04L 9/40 Network security protocols

Abstract

A system and method for modeling a message-passing program module using type annotations is disclosed. The message-passing program module is constructed with operations that communicate with operations of other message-passing program modules in an asynchronous computing environment. Type annotations are communication protocols that represent processes of input and/or output actions that the program module developer expects each operation to perform or take on a selected set of communication channels. During development of the program module, the type annotations are declared at each operation of the program module. Soundness of the type annotations and whether implementation of the program module conforms to the type annotations is checked using a type system. If the program module is well-typed and well-implemented, the type system abstracts a behavioral module of the message-passing program module that reflects the relevant processes expressed by the type annotations. A model checker determines whether the behavioral module is in fact a valid abstraction of the implementation, and if so, evaluates one or more properties of the behavioral module to render a conclusion about these properties for the program module.

Claims

1. A system for modeling behavior of a message-passing program module wherein the message-passing program module communicates with other program modules and wherein intended message-passing behavior of the message-passing program module is specified by a type annotation, the system comprising:

typing rules defining a conformance relationship between the message-passing program module and the type annotation; and

a type system applying a reasoning tool to the conformance relationship to render a conclusion on whether actions of the message-passing program module satisfy the intended behavior expressed by the type annotation.

2. A system as defined in claim 1, wherein the conformance relation is open simulation.

3. A system as defined in claim 2, wherein the reasoning tool uses an assume-guarantee principle.

4. A system as defined in claim 1, wherein the message-passing program module is declared as a pi-calculus mathematical expression.

5. A system as defined in claim 4, wherein the type annotation is declared as a calculus communicating system expression.

6. A system as defined in claim 1, wherein the type annotation specifies a process of intended input and output actions that the message-passing program module is to perform on a set of communication channels.

7. A system as defined in claim 6, wherein the type system extracts an implementation model of the message-passing program module, wherein the implementation model includes actual input and output actions performed by the message-passing program as the message-passing program is compiled.

8. A system as defined in claim 7, wherein the type system applies the typing rules to the implementation to determine whether the conformance relationship exists between the message-passing program module and the type annotation.

9. A system as defined in claim 6, wherein the type system comprises an abstraction module abstracting a behavioral module reflecting the intended input and output actions specified by the process, the system further comprising:

a model checker applying an assume-guarantee principle to the behavioral module to conclude whether the behavioral module is a valid abstraction of the implementation model.

10. A system as defined in claim 8, wherein the model checker evaluates behavioral properties of the behavioral module and renders a conclusion on the behavioral properties for the message-passing program module if the behavioral module is a valid abstraction of the implementation model.

11. A method for modeling behavior of a message-passing program module having operations responsible for establishing communications between the message-passing program module and other program modules, the method comprising:

specifying a first type process reflecting intended message-passing behavior of an operation of the message-passing program module, wherein the first type process is expressed as a type annotation;

compiling the message-passing program module to render an implementation for the operation;

defining a conformance relation for checking conformance between the implementation and the type annotation;

checking the implementation against the first type process to determine whether the implementation satisfies the conformance relation with respect to the type annotation;

if the implementation does not satisfy the conformance relation, rendering an error message that the message-passing application program is not well-implemented.

12. A method as defined in claim 11, wherein the checking act comprises:

assuming that an implementation of a second operation of the message-passing program module satisfies the conformance relation with respect to an associated type annotation.

13. A method as defined in claim 12, wherein the conformance relation is open simulation.

14. A method as defined in claim 11, wherein the specifying act comprises:

defining a set of communication channels for performance of the first type process.

15. A method as defined in claim 14, further comprising:

if the implementation satisfies the conformance relation, abstracting a behavioral model reflecting message-passing actions required the first type process.

16. A method as defined in claim 15, wherein the abstracting act comprises:

discarding information contained in the first type process that does not relate to an action performed on a channel of the set of communication channels for the first type process.

17. A method as defined in claim 16, wherein the behavioral model is declared as a calculus communicating system expression.

18. The method of claim 15, further comprising:

abstracting subtyping obligations defining a relational assumption between the first type process and a second type process specified for a second operation of the message-passing program module.

19. A method as defined in claim 18, wherein the relational assumption is open simulation.

20. A method as defined in claim 19, further comprising:

checking the relational assumption between the first type process and the second type process to render a conclusion on whether the first type process simulates the second type process.

21. A method as defined in claim 20, wherein the act of checking the relational assumption comprises:

assuming that the second type process simulates a third type process of the message-passing program module.

22. A system for evaluating behavioral properties of a message-passing program module having operations for establishing communications between the message-passing program module and other program modules, the system comprising:

means for abstracting a behavioral module representing an intended process to be performed by an operation of the message-passing program module on a set of communication channels;

means for checking whether the behavioral module is a valid abstraction of an implementation for the operation; and

if the behavioral module is deemed a valid abstraction of the implementation, evaluating behavioral properties of the behavioral module to render a conclusion concerning the behavioral properties for the implementation.

23. A system as defined in claim 22, further comprising:

means for specifying a type annotation at the operation, the type annotations being a communication protocol that represents the intended process to be performed by the operation on the set of communication channels, wherein the type annotations are used to abstract the behavioral module.

24. A system as defined in claim 23, further comprising:

means for checking whether conformance exists between the implementation and the type annotation.

25. A system as defined in claim 24, wherein the intended process specifies intended input and output actions that the implementation is to perform on the set of communication channels.

26. A system as defined in claim 22, wherein the checking means comprises:

means for applying assume-guarantee reasoning to verify open simulation assumptions made for input and output action of the intended process.

27. A computer program product readable by a computing system and encoding a computer program of instructions for executing a computer process for controlling operations of the computing system and for modeling behavior of a message-passing program module having operations responsible for establishing communications between the message-passing program module and other program modules, the computer process comprising:

specifying a first type process reflecting intended message-passing behavior of an operation of the message-passing program module, wherein the first type process is expressed as a type annotation;

compiling the message-passing program module to render an implementation for the operation;

defining a conformance relation for checking conformance between the implementation and the type annotation;

checking the implementation against the first type process to determine whether the implementation satisfies the conformance relation with respect to the type annotation;

if the implementation does not satisfy the conformance relation, rendering an error message that the message-passing application program is not well-implemented.

28. The computer process in the computer program product of claim 27, wherein the checking act comprises:

assuming that an implementation of a second operation of the message-passing program module satisfies the conformance relation with respect to an associated type annotation.

29. The computer process in the computer program product of claim 28, wherein the conformance relation is open simulation.

30. The computer process in the computer program product of claim 27, wherein the specifying act comprises:

defining a set of communication channels for performance of the first type process.

31. The computer process in the computer program product of claim 30, wherein the computer process further comprises:

if the implementation satisfies the conformance relation, abstracting a behavioral model reflecting message-passing actions required the first type process.

32. The computer process in the computer program product of claim 31, wherein the abstracting act comprises:

discarding information contained in the first type process that does not relate to an action performed on a channel of the set of communication channels for the first type process.

33. The computer process in the computer program product of claim 32, wherein the behavioral model is declared as a calculus communicating system expression.

34. The computer process in the computer program product of claim 31, wherein the computer process further comprises:

abstracting subtyping obligations defining a relational assumption between the first type process and a second type process specified for a second operation of the message-passing program module.

35. The computer process in the computer program product of claim 34, wherein the relational assumption is open simulation.

36. The computer process in the computer program product of claim 35, wherein the computer process further comprises:

checking the relational assumption between the first type process and the second type process to render a conclusion on whether the first type process simulates the second type process.

37. The computer process in the computer program product of claim 36, wherein the act of checking the relational assumption comprises:

assuming that the second type process simulates a third type process of the message-passing program module.