Skip to main content
SpringerLink
Log in

Embedded Systems: Challenges in Specification and Verification

An (Extended Abstract)

  • Conference paper
  • First Online:
Book cover Embedded Software (EMSOFT 2002)

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

Included in the following conference series:

Abstract

In this position paper, we mention some of the challenges in specification and verification which are raised by the emerging discipline of embedded systems. The main proposition of the paper is that a feasible solution to the problem of effective, reliable, and dependable construction of embedded systems can be provided by a seamless development process based on a formal specification of the required system, which proceeds by the activities of verification and analysis of the specification at very early stages of the design, and then followed by automatic code generation, preceded if necessary by code distribution and allocation.

As a prototype example of such a development process, we quote some experiences from the Sacres project and its follow-up Safeair. Necessary extensions to these preliminary experiments are discussed and evaluated.

This research was supported in part by the John von Newman Minerva Center for the Verification of Reactive Systems.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur, C. Courcoubetis, and D.L. Dill. Model checking for real-time systems. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science, pages 414–425. IEEE Computer Society Press, 1990.

    Google Scholar 

  2. R. Alur, C. Coucoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theor. Comp. Sci., 138(1):3–34, 1995. Special issue on Hybrid Systems.

    Article  MATH  Google Scholar 

  3. R. Alur, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In R.L. Grossman, A. Nerode, A. Ravn, and H. Rischel, editors, Hybrid Systems, volume 736 of Lect. Notes in Comp. Sci., pages 209–229. Springer-Verlag, 1993.

    Google Scholar 

  4. R. Alur and D.L. Dill. A theory of timed automata. Theor. Comp. Sci., 126:183–235, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  5. R. Alur and T.A. Henzinger. Real-time logics: Complexity and expressiveness. In Proc. 5th IEEE Symp. Logic in Comp. Sci., pages 390–401, 1990. See [AlurHenzinger-LICS90] for Journal Version.

    Google Scholar 

  6. E. Asarin and O. Maler. As soon as possible: Time optimal control for timed automata. In F. Vaandrager and J. van Schuppen, editors, Hybrid Systems: Computation and Control, volume 1569 of Lect. Notes in Comp. Sci., pages 19–30. Springer-Verlag, 1999.

    Google Scholar 

  7. E. Asarin, O. Maler, and A. Pnueli. Symbolic controller synthesis for discrete and timed systems. In P. Antsaklis, W. Kohn, A. Nerode, and S. Sastry, editors, Hybrid System II, volume 999 of Lect. Notes in Comp. Sci. Springer-Verlag, 1995.

    Google Scholar 

  8. E. Asarin, O. Maler, A. Pnueli, and J. Sifakis. Controller synthesis for timed automata. In IF AC Symposium on System Structure and Control, pages 469–474. Elsevier, 1998.

    Google Scholar 

  9. P. Bauferton, F. Dupont, R. Leviathan, M. Segleken, and K. Winkelman. Constructing correct systems in the safeair project. In 6th World Multi-conference on Systems, Cybernetics and Informatics (SCI’2002), Orlando, Florida, July 2002. To appear.

    Google Scholar 

  10. A. Benveniste. Safety critical embedded systems: the sacres approach. In A.P. Ravn and H. Rischel, editors, FTRTFT 98: 5th International School and Symposium on Formal Techniques in Real-time and Fault-tolerant Systems, volume 1486 of Lect. Notes in Comp. Sci. Springer-Verlag, 1998.

    Google Scholar 

  11. A. Benveniste, P. Le Guernic, and C. Jacquemot. Synchronous programming with events and relations: the SIGNAL languages and its semantics. Science of Computer Programming, 16:103–149, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  12. E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. IBM Workshop on Logics of Programs, volume 131 of Lect. Notes in Comp. Sci., pages 52–71. Springer-Verlag, 1981.

    Google Scholar 

  13. The Sacres Consortium. Safety critical embedded systems: from requirements to system architecture, 1995. Esprit Project Description EP 20.897, http://www.tni.fr/sacres.

  14. Z. Chaochen, A.P. Ravn, and M.R. Hansen. An extended duration calculus for hybrid real-time systems. In R.L. Grossman, A. Nerode, A. Ravn, and H. Rischel, editors, Hybrid Systems, volume 736 of Lect. Notes in Comp. Sci., pages 36–59. Springer-Verlag, 1993.

    Google Scholar 

  15. W. Damm and D. Harel. LSC’s: Breathing life into message sequence charts. In P. Ciancarini, A. Fantechi, and R. Gorrieri, editors, Proc. 3rd IFIP Int. Conf. on Formal Methods for Open Object-Based Distributed Systems (FMOODS’99. Kluwer Academic Publishers, 1999.

    Google Scholar 

  16. W. Damm, B. Josko, and R. Schlör. Specification and verification of vhdl-based system-level hardware design. In E. Börger, editor, Specification and Validation Methods, pages 331–410. Oxford University Press, 1994.

    Google Scholar 

  17. Konrad Feyerabend and Bernhard Josko. A visual formalism for real time requirement specifications. In Miquel Bertran and Teodor Rus, editors, Transformation-Based Reactive Systems Development, Proceedings, 4th International AM AST Workshop on Real-Time Systems and Concurrent and Distributed Software, ARTS’97, Lecture Notes in Computer Science 1231, pages 156–168. Springer-Verlag, 1997.

    Google Scholar 

  18. D. Harel. On visual formalisms. Comm. ACM, 31:514–530, 1988.

    Article  MathSciNet  Google Scholar 

  19. D. Harel. From play-in scenarios to code: An achievable dream. IEEE Computer, 34(1):53–60, 2001. Also, Proc. Fundamental Approaches to Software Engineering (FASE), Lecture Notes in Computer Science, Vol. 1783 (Tom Maibaum, ed.), Springer-Verlag.

    Google Scholar 

  20. T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: A model checker for hybrid systems. In O. Grumberg, editor, Proc. 9 th Intl. Conference on Computer Aided Verification, (CAV’97), volume 1254 of Lect. Notes in Comp. Sci., Springer-Verlag, pages 460–463, 1997.

    Google Scholar 

  21. D. Harel and H. Kugler. Synthesizing state-based object systems from LSC specifications. In Proc. 5th Inf. Conf. on Implementation and Application of Automata (CIAA’00), Lect. Notes in Comp. Sci. Springer-Verlag, July 2000. To appear.

    Google Scholar 

  22. 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 Engin., 16:403–414, 1990.

    Article  Google Scholar 

  23. D. Harel and R. Marelly. Specifying and Executing Behavioral Requirements: The Play-In/Play-Out Approach. Tech. Report MCS01-15, The Weizmann Institute of Science, 2001. Submitted.

    Google Scholar 

  24. J.G. Henriksen, M. Mukund, K.N. Kumar, and P.S. Thiagarajan. On message sequence graphs and finitely generated regular MSC languages. In J.D.P. Rolim U. Montanari and E. Welzl, editors, Proc. 27th Int. Colloq. Aut. Lang. Prog., volume 1853 of Lect. Notes in Comp. Sci., pages 675–686. Springer-Verlag, 2000.

    Google Scholar 

  25. C.A.R Hoare. Communicating sequential processes. Comm. ACM, 21:666–677, 1978.

    Article  MATH  Google Scholar 

  26. Y. Kesten, Z. Manna, and A. Pnueli. Verification of clocked and hybrid systems. In G. Rozenberg and F.W. Vaandrager, editors, School on Embedded Systems, volume 1494, pages 4–73. Springer-Verlag, 1998.

    Google Scholar 

  27. Y. Kesten and A. Pnueli. Timed and hybrid statecharts and their textual representation. In J. Vytopil, editor, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 571 of Lect. Notes in Comp. Sci., pages 591–619. Springer-Verlag, 1992.

    Google Scholar 

  28. L. Lamport. What good is temporal logic. In R.E.A. Mason, editor, Proc. IFIP 9th World Congress, pages 657–668. North-Holland, 1983.

    Google Scholar 

  29. A. Leung, K.V. Palem, and A. Pnueli. A fast algorithm for scheduling time-constrained instructions on processors with ILP. In The 1998 International Conference on Parallel Architectures and Compilation Techniques (PACT’98), Paris, October 1998.

    Google Scholar 

  30. A. Leung, K.V. Palem, and A. Pnueli. TimeC: A time constraint language for ILP processor compilation. In The 5th Annual Australasian Conference on Parallel And Real-Time Systems (PART’98), Adelaide, Australia, September 1998. Also available as Courant Institute Technical Report No. 764, May 1998.

    Google Scholar 

  31. A. Leung, K. Palem, and A. Pnueli. Scheduling time-constrained instructions on pipelined processors. ACM Trans. Prog. Lang. Sys., 23(1):73–103, 2001.

    Article  Google Scholar 

  32. R. Milner. A Calculus of Communicating Systems. Lec. Notes in Comp. Sci. 94, Springer-Verlag, 1980.

    Google Scholar 

  33. O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Workshop “Real-Time: Theory in Practice’, volume 600 of Lect. Notes in Comp. Sci., pages 447–484. Springer-Verlag, 1992.

    Google Scholar 

  34. O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Workshop “Real-Time: Theory in Practice”, volume 600 of Lect. Notes in Comp. Sci., pages 447–484. Springer-Verlag, 1992.

    Google Scholar 

  35. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991.

    MATH  Google Scholar 

  36. X. Nicollin, J. Sifakis, and S. Yovine. From ATP to timed graphs and hybrid systems. In J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Workshop “Real-Time: Theory in Practice”, volume 600 of Lect. Notes in Comp. Sci., pages 549–572. Springer-Verlag, 1992. See [atp:acta] for Journal Version.

    Google Scholar 

  37. S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. A CM Trans. Prog. Lang. Sys., 4:455–495, 1982.

    Article  MATH  Google Scholar 

  38. A. Pnueli. The temporal logic of programs. In Proc. 18th IEEE Symp. Found. of Comp. Sci., pages 46–57, 1977.

    Google Scholar 

  39. A. Pnueli, M. Siegel, and O. Shtrichman. The code validation tool (CVT)-automatic verification of a compilation process. Software Tools for Technology Transfer, 2(2):192–201, 1998.

    Article  MATH  Google Scholar 

  40. J.P. Queille and J. Sifakis. Fairness and related properties in transition systems— A temporal logic to deal with fairness. Acta Informatica, 19:195–220, 1983.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Weizmann Institute of Science, Israel

    Amir Pnueli

Authors
  1. Amir Pnueli
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of EECS, University of California at Berkeley, Berkeley, CA, 94720, USA

    Alberto Sangiovanni-Vincentelli

  2. Verimag, Centre Equation, 2 rue de Vignate, 38610, Gieres, France

    Joseph Sifakis

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pnueli, A. (2002). Embedded Systems: Challenges in Specification and Verification. In: Sangiovanni-Vincentelli, A., Sifakis, J. (eds) Embedded Software. EMSOFT 2002. Lecture Notes in Computer Science, vol 2491. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45828-X_1

Download citation

  • DOI: https://doi.org/10.1007/3-540-45828-X_1

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44307-0

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation