• DocumentCode
    1681391
  • Title

    Formal verification of the PATHO real-time operating system

  • Author

    Balarin, Felice ; Petty, Karl ; Sengiovanni-Vincentello, A.L. ; Varaiya, Pravin

  • Author_Institution
    Dept. of Electr. Eng. & Comput. Sci., California Univ., Berkeley, CA, USA
  • Volume
    3
  • fYear
    1994
  • Firstpage
    2459
  • Abstract
    We present several models of PATHO, a real-time operating system for an automatically controlled vehicle. The models are simple and scalable, thus they can be used to evaluate real-time verification tools. We describe the verification of PATHO using real-time extensions of HSIS verification system. Experiments show that user-supplied guidelines are crucial for successful verification
  • Keywords
    operating systems (computers); program verification; real-time systems; software performance evaluation; vehicles; HSIS; PATHO; automatically controlled vehicle; formal verification; real-time operating system; real-time verification tools; user-supplied guidelines; verification system; Automata; Automatic control; Control systems; Embedded system; Formal verification; Guidelines; Operating systems; Real time systems; Safety; Vehicles;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Decision and Control, 1994., Proceedings of the 33rd IEEE Conference on
  • Conference_Location
    Lake Buena Vista, FL
  • Print_ISBN
    0-7803-1968-0
  • Type

    conf

  • DOI
    10.1109/CDC.1994.411507
  • Filename
    411507
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=1681391