Skip to main content
SpringerLink
Log in
Book cover

International Hybrid Systems Workshop

International Hybrid Systems Workshop

HS 1992, HS 1991: Hybrid Systems pp 426–451Cite as

On formal support for industrial-scale requirements analysis

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 736))

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.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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.

    Google Scholar 

  2. A. M. Davis. Software Requirements: Analysis & Specification. Prentice-Hall, 1990.

    Google Scholar 

  3. 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.

    Google Scholar 

  4. 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.

    Google Scholar 

  5. 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.

    Google Scholar 

  6. 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.

    Google Scholar 

  7. 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.

    Google Scholar 

  8. D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231–274, 1987.

    Google Scholar 

  9. 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.

    Google Scholar 

  10. 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.

    Google Scholar 

  11. 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.

    Google Scholar 

  12. H. G. Lawley. Hazard and Operability Studies. Chem Eng Process, 8(5):105–116, May 1973.

    Google Scholar 

  13. 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.

    Google Scholar 

  14. L. E. Moser and P. M. Melliar-Smith. Formal Verification of Safety-Critical Systems. Software Practice and Experience, 20(8):799–821, August 1990.

    Google Scholar 

  15. 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.

    Google Scholar 

  16. 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.

    Google Scholar 

  17. 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.

    Google Scholar 

  18. 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.

    Google Scholar 

  19. United Kingdom Ministry of Defence. Interim Defence Standard 00-55: Procurement of Safety Critical Software in Defence Equipment, 1991.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing Science, University of Newcastle upon Tyne, NE1 7RU, UK

    T. Anderson, R. de Lemos, J. S. Fitzgerald & A. Saeed

Authors
  1. T. Anderson
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. R. de Lemos
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. J. S. Fitzgerald
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. A. Saeed
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Robert L. Grossman Anil Nerode Anders P. Ravn Hans Rischel

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation