Skip to main content
SpringerLink
Log in

Specification and verification of controlled systems

  • Conference paper
  • First Online:
Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 1994, ProCoS 1994)

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

Abstract

We propose a conceptual framework to support specification, design and verification of programs controlling physical systems. We introduce a computational model that represents the controller capabilities and distinguishes between synchronous and phase transitions. A graphical system description language is proposed that we believe is readily accessible to control engineers. We formalize the notion of control strategy in controller design.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi and L. Lamport. Composing specifications. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, Lecture Notes in Computer Science 430, pages 1–41. Springer-Verlag, 1990.

    Google Scholar 

  2. D. Harel. Statecharts: A visual Formalism for Complex Systems. Science of Computer Programming, 8, pages 231–274, 1987.

    Google Scholar 

  3. T.A. Henzinger, and Z. Manna, and A. Pnueli. Towards Refining Temporal Specifications into Hybrid Systems. In R.L. Grossman, A. Nerode, A.P. Ravn, H. Rischel, editors, Hybrid Systems, Lecture Notes in Computer Science 736, pages 60–76. Springer Verlag, 1993.

    Google Scholar 

  4. M.S. Jaffe, N.G. Leveson, M.P.E. Heimdahl, B.E. Melhart. Software Requirements Analysis for Real-Time Process-Control Systems. IEEE Transactions on Software Engineering 17:3, pages 241–258, 1991.

    Google Scholar 

  5. A. Kapur, T.A. Henzinger, Z. Manna, A. Pnueli. Proving Safety Properties of Hybrid Systems This volume, 1994.

    Google Scholar 

  6. Y. Kesten, A. Pnueli. Timed and Hybrid Statecharts and their Textual Representation. In J.Vytopil, editor, Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science 571, pages 591–619, Springer Verlag, 1992.

    Google Scholar 

  7. Z. Manna, A. Pnueli. Models for reactivity. Acta Informatica, 30, pages 609–678, 1993.

    Google Scholar 

  8. Z. Manna, A. Pnueli. Temporal Verification of Reactive Systems. To be published by Springer Verlag, to appear 1994.

    Google Scholar 

  9. A. Nerode, W. Kohn. Models for Hybrid Systems: Automata, Topologies, Controllability, Observability. In R.L. Grossman, A. Nerode, A.P. Ravn, H. Rischel, editors, Hybrid Systems, Lecture Notes in Computer Science 736, pages 317–365. Springer Verlag, 1993.

    Google Scholar 

  10. J.S. Ostroff. Temporal Logic of Real-Time Systems. Advanced Software Development Series, Research Studies Press (John Wiley & Sons), 1990.

    Google Scholar 

  11. A.P. Ravn, H. Rischel, K.M. Hansen. Specifying and Verifying Requirements of Real-Time Systems. IEEE Transactions on Software Engineering, 19, pages 41–55, 1993.

    Google Scholar 

  12. H.B. Sipma, Z. Manna. Interactive Design and Verification of Controlled Systems. In Hybrid Systems and Autonomous Control Workshop, to appear 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Stanford University, 94305, Stanford, California

    Henny B. Sipma & Zohar Manna

Authors
  1. Henny B. Sipma
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zohar Manna
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Hans Langmaack Willem-Paul de Roever Jan Vytopil

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Sipma, H.B., Manna, Z. (1994). Specification and verification of controlled systems. In: Langmaack, H., de Roever, WP., Vytopil, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT ProCoS 1994 1994. Lecture Notes in Computer Science, vol 863. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58468-4_188

Download citation

  • DOI: https://doi.org/10.1007/3-540-58468-4_188

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58468-1

  • Online ISBN: 978-3-540-48984-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation