Advertisement

Embedded Systems: Challenges in Specification and Verification

An (Extended Abstract)
  • Amir Pnueli
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2491)

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.

Keywords

Hybrid System Formal Method Temporal Logic Embed System Hybrid Automaton 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. ACD90.
    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. ACH+95.
    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.zbMATHCrossRefGoogle Scholar
  3. ACHH93.
    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. AD94.
    R. Alur and D.L. Dill. A theory of timed automata. Theor. Comp. Sci., 126:183–235, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  5. AH90.
    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. AM99.
    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. AMP95.
    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. AMPS98.
    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. BDL+02.
    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. Ben98.
    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. BGJ91.
    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.zbMATHCrossRefMathSciNetGoogle Scholar
  12. CE81.
    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. Con95.
    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. CRH93.
    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. DH99.
    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. DJS94.
    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. FJ97.
    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. Har88.
    D. Harel. On visual formalisms. Comm. ACM, 31:514–530, 1988.CrossRefMathSciNetGoogle Scholar
  19. Har01.
    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. HHWT97.
    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. HK00.
    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. HLN+90.
    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.CrossRefGoogle Scholar
  23. HM01.
    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. HMKT00.
    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. Hoa78.
    C.A.R Hoare. Communicating sequential processes. Comm. ACM, 21:666–677, 1978.zbMATHCrossRefGoogle Scholar
  26. KMP98.
    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. KP92.
    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. Lam83.
    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. LPP98a.
    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. LPP98b.
    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. LPP01.
    A. Leung, K. Palem, and A. Pnueli. Scheduling time-constrained instructions on pipelined processors. ACM Trans. Prog. Lang. Sys., 23(1):73–103, 2001.CrossRefGoogle Scholar
  32. Mil80.
    R. Milner. A Calculus of Communicating Systems. Lec. Notes in Comp. Sci. 94, Springer-Verlag, 1980.Google Scholar
  33. MMP92a.
    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. MMP92b.
    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. MP91.
    Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991.zbMATHGoogle Scholar
  36. NSY92.
    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. OL82.
    S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. A CM Trans. Prog. Lang. Sys., 4:455–495, 1982.zbMATHCrossRefGoogle Scholar
  38. Pnu77.
    A. Pnueli. The temporal logic of programs. In Proc. 18th IEEE Symp. Found. of Comp. Sci., pages 46–57, 1977.Google Scholar
  39. PSS98.
    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.zbMATHCrossRefGoogle Scholar
  40. QS83.
    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.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Amir Pnueli
    • 1
  1. 1.Weizmann Institute of ScienceIsrael

Personalised recommendations