Abstract
Drawing on practical experience in the development of dependable applications, this paper presents a number of “goals” for industrially applicable formal techniques in the specification and analysis of requirements for hybrid systems. These goals stem from domain-specific concerns such as the division between environment, plant and controller; and from the development context with its wide variety of analysis and design activities.
Motivated by some of these goals, we present a methodology, based on formal methods, for the requirements analysis of hybrid systems that are safetycritical. This methodology comprises a framework whose stages are based on levels of abstraction that follow a general structure for process control systems, a set of techniques appropriate for the issues to be analysed at each stage of the framework, and a hierarchical structure for the product of the analysis. Some aspects of the methodology are exemplified through two case studies. The extent to which this approach meets the goals espoused earlier is discussed.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Tom Anderson, Rogério de Lemos, John Fitzgerald, and Amer Saeed. On Formal Support for Industrial-scale Requirements Analysis. Technical Report TR412, University of Newcastle, NE1 7RU, UK, 1992.
A. M. Davis. Software Requirements: Analysis & Specification. Prentice-Hall, 1990.
R. de Lemos, A. Saeed, and T. Anderson. A Train set as a Case Study for the Requirements Analysis of Safety-Critical Systems. The Computer Journal, 35(1):30–40, February 1992.
R. de Lemos, A. Saeed, and T. Anderson. Analysis of Timeliness Requirements in Safety-Critical Systems. In J. Vytopil, editor, Proceedings of the Symposium in Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 571 of Lecture Notes in Computer Science, pages 171–192. Springer-Verlag, 1992.
J. S. Fitzgerald and C. B. Jones. Modularizing the Formal Description of a Database System. In D. Bjorner, C.A.R. Hoare, and H. Langmaack, editors, VDM'90: VDM and Z — Formal Methods in Software Development., volume 428 of Lecture Notes in Computer Science, pages 189–210. Springer-Verlag, 1990.
H. Genrich. Predicate/Transition Nets. In W. Brauer, W. Reisig, and G. Rozemberg, editors, Petri Nets: Central Models and their Properties, volume 254 of Lecture Notes in Computer Science, pages 206–247. Springer-Verlag, 1987.
K. M. Hansen, A. P. Ravn, and H. Rischel. Specifying and Verifying Requirements of Real-Time Systems. In Proceedings of the ACM SIGSOFT'91 Conference on Software for Critical Systems, New Orleans, Louisiana, pages 44–54, December 1991.
D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231–274, 1987.
D. Harel, H. Lachover, A. Naamad, and A. Pnueli. Statemate: A Working Environment for the Development of Complex reactive Systems. IEEE Transactions on Software Engineering, 16(4):403–414, 1990.
M. S. Jaffe, N. G. Leveson, M. P. E. Heimdahl, and B. E. Melhart. Software Requirements Analysis for Real-Time Process-Control Systems. IEEE Transactions on Software Engineering, SE-17(3):241–258, March 1991.
F. Jahanian and A. K. Mok. Safety Analysis of Timing Properties in Real-Time Systems. IEEE Transactions on Software Engineering, SE-12(9):2–13, September 1986.
H. G. Lawley. Hazard and Operability Studies. Chem Eng Process, 8(5):105–116, May 1973.
O. Maler, Z. Manna, and A. Pnueli. A formal approach to hybrid systems. In Proceedings of the REX Workshop “Real-Time: Theory in Practice”, volume 600 of Lecture Notes in Computer Science. Springer-Verlag, 1992.
L. E. Moser and P. M. Melliar-Smith. Formal Verification of Safety-Critical Systems. Software Practice and Experience, 20(8):799–821, August 1990.
D. L. Parnas and J. Madey. Functional Documentation for Computer Systems Engineering (Version 2). Technical Report CRL Report No. 237, TRIO, McMaster University, Hamilton, Ontario, 1991.
A. Saeed, T. Anderson, and M. Koutny. A Formal Model for Safety-Critical Computing Systems. In SAFECOMP'90, London, UK, pages 1–6, October 1990.
A. Saeed, R. de Lemos, and T. Anderson. The Role of Formal Methods in the Requirements Analysis of Safety-Critical Systems: a Train Set Example. In Proceedings of the 21st Symposium on Fault-Tolerant Computing, Montreal, Canada, pages 478–485, June 1991.
A. Saeed, R. de Lemos, and T. Anderson. An Approach to the Assessment of Requirements Specifications for Safety-Critical Systems. Technical Report No. 381, Computing Laboratory, University of Newcastle upon Tyne, 1992.
United Kingdom Ministry of Defence. Interim Defence Standard 00-55: Procurement of Safety Critical Software in Defence Equipment, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Anderson, T., de Lemos, R., Fitzgerald, J.S., Saeed, A. (1993). On formal support for industrial-scale requirements analysis. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds) Hybrid Systems. HS HS 1992 1991. Lecture Notes in Computer Science, vol 736. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57318-6_39
Download citation
DOI: https://doi.org/10.1007/3-540-57318-6_39
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57318-0
Online ISBN: 978-3-540-48060-0
eBook Packages: Springer Book Archive