Marc K. Zimmerman
ABSTRACT
The readability of formal requirements specification languages is hypothesized as a limiting factor in the acceptance of formal methods by the industrial community. An empirical study was conducted to determine how various factors of state-based requirements specification language design affect readability using aerospace applications. Six factors were tested in all, including the representation of the overall state machine structure, the expression of triggering conditions, the use of macros, the use of internal broadcast events, the use of hierarchies, and transition perspective (going-to or coming-from). Subjects included computer scientists as well as aerospace engineers in an effort to determine whether background affects notational preferences. Because so little previous experimentation on this topic exists on which to build hypotheses, the study was designed as a preliminary exploration of what factors are most important with respect to readability. It can serve as a starting point for more thorough and carefully controlled experimentation in specification language readability.
- Brooks, R. Studying Programmer Behavior Experimentally: The Problems of Proper Methodology. Communications of the ACM. vol 23, no. 4, April 1980. pp. 207-14. Google Scholar
Digital Library
- Finney, K., Fenton, N., and Fedorec, A. Effects of Structure on the Comprehensibility of Formal Specifications. IEE Proceedings - Software. vol 146, no. 4, August 1999. pp. 193-202.Google ScholarCross Ref
- Fitter, M. and Green, T.R. When Do Diagrams Make Good Computer Languages? International Journal of Man-Machine Studies. vol. 11, 1979. pp. 235-261.Google ScholarCross Ref
- Harel, D, et.al. Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming 8. Elsevier Science Publishers B. V., North Holland. 1987. pp. 231-274. Google ScholarDigital Library
- Heimdahl, M., Leveson, N., and Reese, J. Experiences From Specifying the TCASII Requirements Using RSML. Proceedings of the 17th Digital Avionics Systems Conference, November 1998.Google Scholar
- Heitmeyer, C., Jeffords, R., and Labaw, B. Automated Consistency Checking of Requirements Specifications. ACM Transactions on Software Engineering and Methodology, vol 5, no 3, July, 1996. pp. 231-261. Google ScholarDigital Library
- Leveson, N. Completeness in Formal Specification Language Design for Process Control Systems. Proceedings of Formal Methods in Software Practice Conference, August 2000. Google ScholarDigital Library
- Sherry, L., Youssefi, D., and Hynes, C. A Formalism for the Specification of Operationally Embedded Reactive Avionic Systems. HSR FD G&C Task 4 - VMS Structure Development. Honeywell, October 1995.Google Scholar
- Zimmerman, Marc. Investigation the Readability of Formal Specification Languages. M.Sc. thesis, Massachusetts Institute of Technology, May, 2001.Google Scholar
- Zimmerman, M., Rodriguez, M., Ingram, B., Katahira, M., de Villepin, M., and Leveson, N. Making Formal Methods Practical. Proceedings of the 19th Digitial Avionics Systems Conference. October 2000.Google ScholarCross Ref
Index Terms
- Investigating the readability of state-based formal requirements specification languages
Recommendations
Informal and Formal Requirements Specification Languages: Bridging the Gap
The differences between informal and formal requirements specification languages are noted, and the issue of bridging the gap between them is discussed. Using structured analysis (SA) and the Vienna development method (VDM) as surrogates for informal ...
Operational specification languages
ACM '83: Proceedings of the 1983 annual conference on Computers : Extending the human resourceThe “operational approach” to software development is based on separation of problem-oriented and implementation-oriented concerns, and features executable specifications and transformational implementation. “Operational specification languages” are ...
Comments