This Article 
 Bibliographic References 
 Add to: 
Requirements Specification for Process-Control Systems
September 1994 (vol. 20 no. 9)
pp. 684-707

The paper describes an approach to writing requirements specifications for process-control systems, a specification language that supports this approach, and an example application of the approach and the language on an industrial aircraft collision avoidance system (TCAS II). The example specification demonstrates: the practicality of writing a formal requirements specification for a complex, process-control system; and the feasibility of building a formal model of a system using a specification language that is readable and reviewable by application experts who are not computer scientists or mathematicians. Some lessons learned in the process of this work, which are applicable both to forward and reverse engineering, are also presented.

[1] G. R. Bruns, S. L. Gerhart, I. Forman, and M. Graf, "Design technology assessment: The statecharts approach," Tech. Rep. STP-107-86, MCC, Mar. 1986.
[2] E. M. Clarke, E. A. Emerson, and A. P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic,"ACM Trans. Program. Lang. Syst., vol. 8, no. 2, pp. 244-263, Apr. 1986.
[3] S. Faulk, J. Brackett, P. Ward, and J. Kirby Jr. "The core method for real-time requirements,"IEEE Software, vol. 9, no. 5, Sept. 1992.
[4] M. Fitter and T. R. G. Green, "When do diagrams make good computer languages,"Int. J. Man-Machine Studies, vol. 11, 1979.
[5] D. Harel, "Statecharts: A visual formalism for complex systems,"Sci. Comput. Program., vol. 8, pp. 231-274, 1987.
[6] Mats P. E. Heimdahl, "Static analysis of state based requirements: Analysis for completeness and consistency," Ph.D. thesis, Univ. of California, Irvine, 1994.
[7] K. L. Heninger, "Specifying software for complex systems: New techniques and their application,"IEEE Trans. Software Eng., vol. SE-6, no. 1, Jan. 1980.
[8] D. Harel, H. Lachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, A. Shtull-Trauring, and M. Trakhtenbrot, "Statemate: A working environment for the development of complex reactive systems,"IEEE Trans. Software Eng., vol. 16, no. 4, Apr. 1990.
[9] C. A. R. Hoare, "Communicating sequential processes,"Commun. ACM, vol. 21, pp. 666-677, 1978.
[10] G. J. Holzmann,Design and Validation of Computer Protocols. Englewood, Cliffs, NJ: Prentice-Hall, 1991.
[11] D. Harel and A. Pnueli, "On the development of reactive systems" K.R. Apt, Ed.,Logics and Models of Concurrent Systems. New York: Springer-Verlag, 1985, pp. 477-498.
[12] D.J. Hatley and I. Pirbhai,Strategies for Real-Time System Specification, Dorset House, New York, 1987.
[13] M. S. Jaffe, "Completeness, robustness, and safety in real-time software requirements and specifications," Ph.D. dissertation, Univ. California, Irvine, 1988.
[14] M. S. Jaffe, N. G. Leveson, M. P. E. Heimdahl, and B. Melhart, "Software requirements analysis for real-time process-control systems,"IEEE Trans. Software Eng., vol. 17, no. 3, Mar. 1991.
[15] N. G. Leveson, S. S. Cha, and T. J. Shimeall, "Safety Verification of Ada Programs using Software Fault Trees,"IEEE Software, vol. 14, no. 1, July 1991.
[16] N. G. Leveson and P. R. Harvey, "Analyzing Software Safety,"IEEE Trans. on Software Eng., SE-vol. 9, no. 5, pp. 569-579, Sept. 1983.
[17] N.G. Leveson and J.L. Stolzy, "Safety analysis using Petri nets,"IEEE Trans. Software Eng., vol. SE-13, no. 3, pp. 386-397, Mar. 1987.
[18] B. E. Melhart, "An external interaction model for specifying requirements of embedded software," Tech. Rep. Draft, Texas Christian Univ., Jan. 1991.
[19] D. L. Parnas, "Designing software for ease of extension and contraction,"IEEE Trans. Software Eng., vol. SE-5, no. 2, pp. 128-138, Mar. 1979.
[20] A. Pnueli and M. Shalev, "What is in a step?"J.W. De Baker, Liber Amicorum, J. Klop, J. Meijer, and J. Rutten, Eds. Amsterdam: CWI, pp. 373-400, 1989.
[21] D. L. Parnas and Y. Wang, "The trace assertion method of module interface specification," Tech. Rep. 89-261, Queen's Univ., Kingston, ON, 1989.
[22] A. P. Ravn and H. Rischel, "Requirements capture for embedded real-time systems," inIMACS Symp. MCTS, 1991.
[23] A. C. Shaw, "Communicating real-time state machines,"IEEE Trans. Software Eng., vol. 18, no. 9, pp. 805-816, Sept. 1992.
[24] A. J. van Schouwen, "The A-7 requirements model: Re-examination for real-time systems and an application to monitoring systems," Tech. Rep. 90-276, Queen's Univ., Kingston, ON, May 1990.
[25] E. Weyuker, T. Goradia, and A. Singh, "Automatically generating test data from boolean specification,"IEEE Transactions Software Eng., vol. 20, no. 5, May 1994.
[26] P. T. Ward and S. J. Mellor,Structured Development for Real-Time Systems. New York: Yourdon, 1985.

Index Terms:
process control; process computer control; formal specification; specification languages; position control; aerospace computing; aircraft instrumentation; requirements specification; process-control systems; specification language; example application; industrial aircraft collision avoidance system; TCAS II; example specification; formal requirements specification; formal model; reverse engineering
N.G. Leveson, M.P.E. Heimdahl, H. Hildreth, J.D. Reese, "Requirements Specification for Process-Control Systems," IEEE Transactions on Software Engineering, vol. 20, no. 9, pp. 684-707, Sept. 1994, doi:10.1109/32.317428
Usage of this product signifies your acceptance of the Terms of Use.