This Article 
 Bibliographic References 
 Add to: 
Formal Requirements Analysis of an Avionics Control System
May 1997 (vol. 23 no. 5)
pp. 267-278

Abstract—We report on a formal requirements analysis experiment involving an avionics control system. We describe a method for specifying and verifying real-time systems with PVS. The experiment involves the formalization of the functional and safety requirements of the avionics system as well as its multilevel verification. First level verification demonstrates the consistency of the specifications whilst the second level shows that certain system safety properties are satisfied by the specification. We critically analyze methodological issues of large scale verification and propose some practical ways of structuring verification activities for optimizing the benefits.

[1] "The Procurement of Safety Critical Software in Defence Equipment," Interim Defence Standard 00-55, Issue 1, 1991.
[2] "Draft IEC Standard 1508—Functional Safety: Safety-Related Systems,", Int'l Electrotechnical Commission, Technical Committee no. 65, Working Group 9/10 (WG 9/10), IEC 65A, Apr. 1995.
[3] P. Bradley, L. Shackleton, and V. Stavridou, "The SafeFM Project," Proc. Safety Critical Systems Symp. 93, F. Redmill, ed., pp. 168-176. Springer-Verlag, Feb. 1993.
[4] V. Stavridou, A. Boothroyd, T. Boyce, P. Bradley, J. Draper, B. Dutertre, and R. Smith, "Developing and Assessing Safety Critical Systems with Formal Methods: the SafeFM Way," J. High Integrity Systems, vol. 1, no. 6, pp. 541-545, 1996.
[5] S. Owre, J. Rushby, N. Shankar, and F. von Henke, "Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS," IEEE Trans. Software Eng., vol. 21, pp. 107-125, Feb. 1995.
[6] J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas, "A Tutorial Introduction to PVS," WIFT '95 Workshop on Industrial-Strength Formal Specification Techniques, Apr. 1995.
[7] T. Boyce, "SafeFM Case Study Report," Technical Report SafeFM-018-GEC-1, SafeFM project, Jan. 1994.
[8] S. Owre, N. Shankar, and J.M. Rushby, "User Guide for the PVS Specification and Verification System," Computer Science Lab., SRI Int'l, Mar. 1993.
[9] S.P. Miller and M. Srivas, "Formal Verification of the AAMP5 Microprocessor: A Case Study in the Industrial Use of Formal Methods," WIFT '95 Workshop on Industrial-Strength Formal Specification Techniques, Apr. 1995.
[10] M.K. Srivas and S.P. Miller, "Formal Verification of an Avionics Microprocessor," Technical Report SRI-CSL-95-04, SRI Int'l, June 1995.
[11] K.-H. Buth, "Automated Code Generator Verification Based on Algebraic Laws," Technical Report, ProCoS II, Kiel KHB 5/1, Univ. of Kiel, Sept. 1995.
[12] J. Hooman, "Correctness of Real Time Systems by Construction," Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science 863, pp. 19-40. Springer-Verlag, Sept. 1994.
[13] N. Shankar, "Verification of Real-Time Systems Using PVS," Computer Aided Verification, CAV '93, Lecture Notes in Computer Science 697. Springer-Verlag, June-July 1993.
[14] M.-J.-C. Gordon and T.-F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. ISBN 0-521-44189-7. Cambridge Univ. Press, 1993.
[15] A.P. Ravn, H. Rischel, and K.M. Hansen, “Specifying and Verifying Requirements of Real-Time Systems,” IEEE Trans. Software Eng., vol. 19, no. 1, pp. 41–55, Jan. 1993.
[16] Z. Chaochen, C.A.R. Hoare, and A.P. Ravn, "A Calculus of Durations," Information Processing Letters, vol. 40, no. 5, pp. 269-276, Dec. 1991.
[17] J.U. Skakkebæk and N. Shankar, "Towards a Duration Calculus Proof Assistant in PVS," Formal Techniques in Real-time and Fault-Tolerant Systems, Lecture Notes in Computer Science 863. Springer-Verlag, Sept. 1994.
[18] Z. Chaochen, A.P. Ravn, and M.R. Hansen, "An Extended Duration Calculus for Hybrid Real-Time Systems," Hybrid Systems, Lecture Notes in Computer Science 736, pp. 36-59, 1993.
[19] A.P. Ravn, "Design of Embedded Real-Time Computing Systems," PhD thesis, Technical Univ. of Denmark, Lyngby, Denmark, Oct. 1995.
[20] N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, "The Synchronous Data-Flow Programming Language LUSTRE," Proc. IEEE, vol. 79, no. 9, pp. 1,305-1,320, Sept. 1991.
[21] P. Le Guernic, T. Gautier, M. Le Borgne, and C. Le Maire, "Programming Real-Time Applications with SIGNAL," Proc. IEEE, vol. 79, no. 9, pp. 1,321-1,336, Sept. 1991.
[22] J. Crow and B. Di Vito, "Formalizing Space Shuttle Software Requirements," ACM SIGSOFT Workshop on Formal Methods in Software Practice, Jan. 1996.
[23] C.B. Jones, Systematic Software Development Using VDM.Englewood Cliffs, N.J.: Prentice Hall, 1986.
[24] J.R. Abrial, M. Lee, D. Neilson, N. Scharbach, and I. Sorensen, "The B method for Large Software. Specification, Design and Coding," VDM '91: vol. 2: Tutorials, pp. 398-405, Lecture Notes in Computer Science 552. Springer-Verlag, 1991.
[25] B. Dutertre, "Case Study Coherent Specifications," Technical Report SafeFM-050-RH-1, SafeFM project, July 1994.
[26] T. Boyce, "Formal Techniques in Analysis and Design," Technical Report SafeFM-027-GEC-2, SafeFM project, July 1994.
[27] B.L. Di Vito, "Formalizing New Navigation Requirements for NASA's Space Shuttle," Proc. Formal Methods Europe (FME '96),Oxford, England, Mar. 1996.
[28] T. Boyce, "ML Animation and Test Case Generation," Technical Report SafeFM-036-GEC-1, SafeFM project, Jan. 1995.

Index Terms:
Formal specification, formal verification, safety critical systems, requirements analysis, avionics systems.
Bruno Dutertre, Victoria Stavridou, "Formal Requirements Analysis of an Avionics Control System," IEEE Transactions on Software Engineering, vol. 23, no. 5, pp. 267-278, May 1997, doi:10.1109/32.588520
Usage of this product signifies your acceptance of the Terms of Use.