• DocumentCode
    1835636
  • Title

    A Timed Extension of Property Sequence Chart

  • Author

    Zhang, Pengcheng ; Li, Bixin ; Sun, Mingjie

  • Author_Institution
    Sch. of Comput. Sci. & Eng., Southeast Univ., Nanjing
  • fYear
    2008
  • fDate
    3-5 Dec. 2008
  • Firstpage
    197
  • Lastpage
    206
  • Abstract
    Property sequence chart (PSC) is a novel scenarios based notation, which is proposed to represent the temporal properties for concurrent system. It represents a first step toward languages that try to balance expressive power and simplicity of use. Thus, PSC is more intuitive and easily understandable than the traditional temporal logic, such as linear-time temporal logic or computation tree logic. However, the current version of PSC just represents the order of eventpsilas occurrence and lacks the ability to express timed properties. In real-time systems, it is well known that some timed requirements are also very important and need to be specified clearly. Thus, in this paper, in order to make PSC have timed expressiveness, we extend PSC into Timed PSC (TPSC) and give the semantics of TPSC in terms of timed Buchi automaton. Then, we measure the expressive power of TPSC by the use of recently proposed real-time specification pattern. Finally, we illustrate the use of TPSC in the context of a Web service application which requires special timed requirements.
  • Keywords
    automata theory; concurrency control; formal specification; formal verification; real-time systems; temporal logic; computation tree logic; concurrent system; linear-time temporal logic; real-time specification pattern; real-time system; timed Buchi automaton; timed property sequence chart semantics; Automata; Computer science; Context-aware services; Logic; Power engineering and energy; Power measurement; Real time systems; Sun; Systems engineering and theory; Unified modeling language;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    High Assurance Systems Engineering Symposium, 2008. HASE 2008. 11th IEEE
  • Conference_Location
    Nanjing
  • ISSN
    1530-2059
  • Print_ISBN
    978-0-7695-3482-4
  • Type

    conf

  • DOI
    10.1109/HASE.2008.20
  • Filename
    4708878