• DocumentCode
    3538487
  • Title

    Emerald: An Automated Modeling and Verification Tool for Component-Based Real-Time Systems

  • Author

    Zhang, Yizhou ; Lin, Hao ; Li, Guoqiang

  • Author_Institution
    Sch. of Software, Shanghai Jiao Tong Univ., Shanghai, China
  • fYear
    2012
  • fDate
    27-29 Aug. 2012
  • Firstpage
    120
  • Lastpage
    123
  • Abstract
    Controller automata, extending timed automata, are a formal theory to model and analyze real-time systems with mutex components. Given a strict partial order over states, an ordered controller automaton can be faithfully translated into a timed automaton. We present a tool named Emerald to translate ordered controller automata into timed automata and perform the transformation between their specifications in order to use the existing model checking engine, UPPAAL.
  • Keywords
    automata theory; formal verification; real-time systems; Emerald; automated modeling; component-based real-time systems; controller automata; mutex components; timed automata; verification tool; Automata; Clocks; Computational modeling; Engines; Real-time systems; Software; Real-time systems; controller automata; modeling; verification;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Quality Software (QSIC), 2012 12th International Conference on
  • Conference_Location
    Xi´an, Shaanxi
  • ISSN
    1550-6002
  • Print_ISBN
    978-1-4673-2857-9
  • Type

    conf

  • DOI
    10.1109/QSIC.2012.27
  • Filename
    6319234
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3538487