Specification and verification for concurrent systems with graphical and textual editors

• US 6,385,765 B1
• Filed: 07/02/1997
• Issued: 05/07/2002
• Est. Priority Date: 07/02/1996
• Status: Expired due to Term

• Current Assignee: North Carolina State University Technology Transfer and Industry Research, The Research Foundation for The State University of New York (State University of New York)
• Original Assignee: Rutgers University
• Inventors: Cleaveland, Rance, Ramakrishna, Y. S., Smolka, Scott A., Lewis, Philip M.
• Primary Examiner(s): Powell, Mark R.
• Assistant Examiner(s): INGBERG, TODD D
• Application Number:
  US08/887,147
• Time in Patent Office: 1,770 Days
• Field of Search: 395/701, 395/500, 395/183.09, 371/27.4, 706/920, 717/1, 717/9, 717/8, 717/5, 717/7
• US Class Current: 717/100
• CPC Class Codes: G06F 8/10 Requirements analysis; Specification techniques

Abstract

Software for, and a method of using a computer for, specifying and verifying synchronous and asynchronous concurrent systems. The method comprises specifying software in a design language possessing a formal semantics; simulating the design in accordance with its formal semantics; verifying that the design satisfies predetermined requirements; generating test cases and; generating software code. The method includes the steps of inputting by a graphical editor and a textual editor a formal design of the software, inputting desired properties as formulas in temporal logic, and verifying automatically if the formal design satisfies the desired properties.

Claims

1. A method of designing software for a concurrent system comprising:

specifying software in a design language possessing a formal semantics;

simulating the design in accordance with its formal semantics;

verifying that the design satisfies predetermined requirements;

generating test cases and;

generating software code.

2. A method as in claim 1 wherein:

the verification includes using partial-order reduction algorithms to reduce the state space.

3. A method as in claim 1 wherein:

the specification is composed using a graphical editor and a textual editor.

4. A method as in claim 3 wherein:

the graphical and textual editors perform static type checking to insure that correct values are communicated in all contexts.

5. A method as in claim 3 wherein:

the graphical and textual editors are structure-based editors that insure that all specifications produced using these editors are syntactically correct.

6. A method as in claim 1 wherein:

the design language is a graphical coordination language permitting subsystems specified in different design notations to be combined together.

7. A method as in claim 1 wherein:

the design language provides constructs that allow communication ports of different, independent subsystems to be connected, thereby introducing a capability for exchange of data values among the subsystems.

8. A method as in claim 1 wherein:

the design language provides constructs that allow the communication ports of a subsystem to selectively be removed from or added to the subsystem'"'"'s communication interface.

9. A method as in claim 1 wherein:

the design language supports hierarchical specifications in which a system is composed of subsystems and subsystems are composed of sub-subsystems.

10. A method as in claim 1 wherein:

the design specification supports open notation allowing for the simulation and verification of subsystems independently of other subsystems.

11. A method as in claim 1 wherein:

the simulation can simulate different levels of the hierarchy simultaneously.

12. A method as in claim 1 wherein:

the simulation allows for commands to stop upon satisfaction of a predetermined condition.

13. A method as in claim 1 further comprising:

providing a history list that documents the simulation.

14. A method as in claim 13 wherein:

the simulation may be stopped and restarted at any point on the history list.

15. A method as in claim 1 wherein:

the verification is accomplished by model checking.

16. A method as in claim 15 wherein:

the model checker can verify possibility properties.

17. A method as in claim 15 wherein:

the model checker can check hierarchical networks.

18. A method as in claim 15 wherein:

the model checker uses partial-order reduction methods.

19. A method as in claim 18 wherein:

the partial-order reduction methods use dynamic information regarding the behavior of the specification to determine which states and transitions can be eliminated from consideration.

20. A method as in claim 15 wherein:

the model checker allows for the independent verification of subsystems and the ability to verify hierarchical systems.

21. A method as in claim 1 wherein:

the verification checks for the predetermined condition of equivalence.

22. A method as in claim 1 wherein:

the verification uses minimization to eliminate redundant states from the state space underlying a system specification.

23. A method as in claim 1 wherein:

the verification checks for the predetermined condition of preordering.

40. A method of using a computer as in claim 18 wherein:

the simulation allows for commands to stop upon satisfaction of a predetermined condition.

41. A method of using a computer as in claim 18 further comprising:

producing a history list that documents the simulation.

42. A method of using a computer as in claim 41 wherein:

the simulation may be stopped and restarted at any point on the history list.

24. A method of using a computer for specifying and verifying a concurrent system comprising:

inputting by a graphical editor and a textual editor a formal design of the software;

inputting desired properties as formulas in temporal logic;

verifying automatically if the formal design satisfies the desired properties.

25. A method of using a computer as in claim 24 wherein:

the graphical and textual editors allow for specifying hierarchically structured systems which are composed of subsystems.

26. A method of using a computer as in claim 25 wherein:

the specification created by the graphical and textual editors has formal operational semantics.

27. A method of using a computer as in claim 24 wherein:

the graphical and textual editors perform static type checking to insure that correct values are communicated in all contexts.

28. A method of using a computer as in claim 24 wherein:

the graphical and textual editors are structure-based editors that insure that all specifications produced using these editors are syntactically correct.

29. A method of using a computer as in claim 24 wherein:

the formal design supports the specification of open systems.

30. A method of using a computer as in claim 24 wherein:

one desired property that is verified is a condition of equivalence.

31. A method of using a computer as in claim 24 wherein:

one desired property that is verified is a condition of preordering.

32. A method of using a computer as in claim 24 wherein:

one desired property that is verified is a condition of freedom from deadlock.

33. A method of using a computer as in claim 24 wherein:

one desired property that is verified is a condition of a possibility property.

34. A method of using a computer as in claim 24 further comprising:

using partial-order reduction methods to eliminate redundant portions of the state space from consideration.

35. A method of using a computer as in claim 34 wherein:

the partial-order reduction methods include using dynamic information regarding the behavior of the specification to determine which states and transactions can be eliminated from the verification.

36. A method of using a computer as in claim 24 wherein:

the verification is done in a local, demand-driven manner.

37. A method of using a computer as in claim 24 wherein:

verification allows for independent verification of subsystems and an ability to verify hierarchical systems.

38. A method of using a computer as in claim 24 further comprising:

simulating the design in accordance with its formal semantics.

39. A method of using a computer as in claim 38 wherein:

the simulation can simulate different levels of the hierarchy simultaneously.

43. A method of using a computer as in claim 24 further comprising:

generating implementation code from the formal design.

44. Computer software for specifying and verifying concurrent systems comprising:

a graphical editor for specifying a system;

a textual editor for specifying a system;

means for verifying the specification for preselected properties.

45. Software as in claim 44 wherein:

the graphical and textual editors allow for specifying hierarchically structured systems.

46. Software as in claim 44 wherein:

the specifications produced using the graphical and textual editors have formal operational semantics.

47. Software as in claim 44 wherein:

the graphical and textual editors perform static type checking to insure that correct values are communicated in all contexts.

48. Software as in claim 44 wherein:

the graphical and textual editors are structure-based editors that insure that all specifications produced using these editors are syntactically correct.

49. Software as in claim 44 wherein:

open systems can be specified.

50. Software as in claim 44 wherein:

one preselected property is a condition of equivalence.

51. Software as in claim 44 wherein:

one preselected property is a condition of preordering.

52. Software as in claim 44 wherein:

one preselected property is a condition of freedom from deadlock.

53. Software as in claim 44 wherein:

one preselected property is a condition of possibility properties.

54. Software as in claim 44 further comprising:

means for partial-order reduction.

55. Software as in claim 54 wherein:

the means for partial-order reduction includes using dynamic information regarding the behavior of the specification to determine which states and transitions can be eliminated from the verification.

56. Software as in claim 44 wherein:

the verification is done in a local, demand-driven manner.

57. Software as in claim 44 wherein:

the verification allows for independent verification of subsystems and an ability to verify hierarchical systems.

58. Software as in claim 44 further comprising:

an implementation code generator for generating executable code from the specification.

59. Software as in claim 44 further comprising:

a simulator for simulating the system in accordance with its specification.

60. Software as in claim 59 wherein:

the simulator can simultaneously simulate different levels of a hierarchical system.

61. Software as in claim 60 wherein:

the simulation may be stopped and restarted at any point on the history list.

62. Software as in claim 59 wherein:

the simulator stops upon satisfaction of a predetermined condition.

63. Software as in claim 59 further comprising:

a history list that documents the simulation.