SC(R)3: towards usability of formal methods

ABSTRACT

This paper gives an overview of SC(R)³ - a toolset designed to increase the usability of formal methods for software development. Formal requirements are specified in SC(R)³ in an easy to use and review format, and then used in checking requirements for correctness and in verifying consistency between annotated code and requirements.In this paper we discuss motivations behind this work, describe several tools which are part of SC(R)³ and illustrate their operation on an example of a Cruise Control system.

REFERENCES

• 1: {1} Ruth Abraham. "Evaluating Generalized Tabular Expressions in Software Documentation". CRL Technical Report 267, McMaster University, February 1997.
• 2: Joanne M. Atlee , Michael A. Buckley, A logic-model semantics for SCR software requirements, Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis, p.280-292, January 08-10, 1996, San Diego, California, United States
• 3: Maria Marsha A. Chechik , John Gannon, Automatic analysis of consistency between requirements and designs, 1996
• 4: {4} M. Chechik and M. Cwirko-Godyski. "Cruise Control System: A Case-Study in Using SCR in Development and Verification of Event-Driven Systems". Technical report, University of Toronto, June 1998. (in preparation).
• 5: {5} M. Chechik and V.S. Sudha. "Checking Consistency between Source Code and Annotations". CSRG Technical Report 373, Department of Computer Science, University of Toronto, 1998.
• 6: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 7: Edmund M. Clarke , Jeannette M. Wing, Formal methods: state of the art and future directions, ACM Computing Surveys (CSUR), v.28 n.4, p.626-643, Dec. 1996 [doi>10.1145/242223.242257]
• 8: Patrick Causot , Radhia Cousot, Static determination of dynamic properties of generalized type unions, ACM SIGPLAN Notices, v.12 n.3, p.77-94, March 1977
• 9: Anthony Hall, Seven Myths of Formal Methods, IEEE Software, v.7 n.5, p.11-19, September 1990 [doi>10.1109/52.57887]
• 10: Constance L. Heitmeyer , Ralph D. Jeffords , Bruce G. Labaw, Automated consistency checking of requirements specifications, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.3, p.231-261, July 1996 [doi>10.1145/234426.234431]
• 11: {11} K. Heninger. "Software Requirements for the A-7E Aircraft". Technical Report NRL Report 3876, Naval Research Laboratory, Washington, DC, 1978.
• 12: {12} K. Heninger. "Specifying Software Requirements for Complex Systems: New Techniques and Their Applications". IEEE Transactions on Software Engineering, SE-6(1):2-12, January 1980.
• 13: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 14: {14} D. N. Hoover and Zewei Chen. "Table-Wise: A Decision Table Tool". In John Rushby, editor, Proceedings of COMPASS'95 , June 1995.
• 15: {15} James Kirby. "Example NRL/SCR Software Requirements for an Automobile Cruise Control and Monitoring System". Technical report, Wang Institute of Graduate Studies, October 1988. Revision 2.0 by Skip Osborne and Aaron Temin.
• 16: {16} R. P. Kurshan. "COSPAN". In Proceedings of CAV'96, 1996.
• 17: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 18: {18} S. Owre, N. Shankar, and J. Rushby. "User Guide for the PVS Specification and Verification System (Draft)". Technical report, Computer Science Lab, SRI International, Menlo Park, CA, 1993.
• 19: Sam Owre , John M. Rushby , Natarajan Shankar, Integration in PVS: Tables, Types, and Model Checking, Proceedings of the Third International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.366-383, April 02-04, 1997
• 20: David Lorge Parnas , Jan Madey, Functional documents for computer systems, Science of Computer Programming, v.25 n.1, p.41-61, Oct. 1995 [doi>10.1016/0167-6423(95)96871-J]
• 21: David Lorge Parnas, Some Theorems We Should Prove, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, p.155-162, August 11-13, 1993
• 22: David Lorge Parnas , Jan Madey , Michal Iglewski, Precise Documentation of Well-Structured Programs, IEEE Transactions on Software Engineering, v.20 n.12, p.948-976, December 1994 [doi>10.1109/32.368133]
• 23: Dennis K. Peters , David Lorge Parnas, Using Test Oracles Generated from Program Documentation, IEEE Transactions on Software Engineering, v.24 n.3, p.161-173, March 1998 [doi>10.1109/32.667877]
• 24: {24} Tirumale Sreemani and Joanne M. Atlee. "Feasibility of Model Checking Software Requirements: A Case Study". In Proceedings of COMPASS'96, Gaithersburg, Maryland, June 1996.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages
      D.2.4 Software/Program Verification
          Subjects: Validation

General Terms:
Algorithms, Design, Experimentation, Measurement, Theory