Real-time systems : formal specification and automatic verification

著者

書誌事項

Real-time systems : formal specification and automatic verification

Ernst-Rüdiger Olderog and Henning Dierks

Cambridge University Press, 2008

大学図書館所蔵 件 / 7

この図書・雑誌をさがす

注記

Bibliography: p. 304-311

Includes index

内容説明・目次

内容説明

Real-time systems need to react to certain input stimuli within given time bounds. For example, an airbag in a car has to unfold within 300 milliseconds in a crash. There are many embedded safety-critical applications and each requires real-time specification techniques. This text introduces three of these techniques, based on logic and automata: duration calculus, timed automata, and PLC-automata. The techniques are brought together to form a seamless design flow, from real-time requirements specified in the duration calculus; via designs specified by PLC-automata; and into source code for hardware platforms of embedded systems. The syntax, semantics, and proof methods of the specification techniques are introduced; their most important properties are established; and real-life examples illustrate their use. Detailed case studies and exercises conclude each chapter. Ideal for students of real-time systems or embedded systems, this text will also be of great interest to researchers and professionals in transportation and automation.

目次

  • Preface
  • 1. Introduction
  • 2. Duration calculus
  • 3. Properties and subsets of DC
  • 4. Timed automata
  • 5. PLC-automata
  • 6 Automatic verification
  • Appendix
  • Notations
  • Bibliography
  • Index.

「Nielsen BookData」 より

詳細情報

  • NII書誌ID(NCID)
    BA87776131
  • ISBN
    • 9780521883337
  • 出版国コード
    uk
  • タイトル言語コード
    eng
  • 本文言語コード
    eng
  • 出版地
    Cambridge, UK ; New York
  • ページ数/冊数
    xvi, 320 p.
  • 大きさ
    26 cm
  • 分類
  • 件名
ページトップへ

AltStyle によって変換されたページ (->オリジナル) /