Stock up on textbooks with 40% off + FREE shipping or choose from thousands of Protocols eBooks at just 9.99 each!

Lecture Notes in Computer Science
cover

Specification and Compositional Verification of Real-Time Systems

Authors: Hooman, Jozef

Buy this book

eBook $74.99
price for USA in USD (gross)
  • The eBook version of this title will be available soon
  • ISBN 978-3-540-46602-4
  • Digitally watermarked, DRM-free
  • Included format:
  • ebooks can be used on all reading devices
  • Immediate eBook download after purchase
Softcover $99.00
price for USA in USD
  • ISBN 978-3-540-54947-5
  • Free shipping for individuals worldwide
  • Usually dispatched within 3 to 5 business days.
About this book

The research described in this monograph concerns the formal specification and compositional verification of real-time systems. A real-time programminglanguage is considered in which concurrent processes communicate by synchronous message passing along unidirectional channels. To specifiy functional and timing properties of programs, two formalisms are investigated: one using a real-time version of temporal logic, called Metric Temporal Logic, and another which is basedon extended Hoare triples. Metric Temporal Logic provides a concise notationto express timing properties and to axiomatize the programming language, whereas Hoare-style formulae are especially convenient for the verification of sequential constructs. For both approaches a compositional proof system has been formulated to verify that a program satisfies a specification. To deduce timing properties of programs, first maximal parallelism is assumed, modeling the situation in which each process has itsown processor. Next, this model is generalized to multiprogramming where several processes may share a processor and scheduling is based on priorities. The proof systems are shown to be sound and relatively complete with respect to a denotational semantics of the programming language. The theory is illustrated by an example of a watchdog timer.

Table of contents (6 chapters)

Table of contents (6 chapters)
  • Introduction

    Pages 1-10

  • Compositionality

    Pages 11-54

  • Compositionality and real-time

    Pages 55-102

  • Adding program variables

    Pages 103-128

  • Shared processors

    Pages 129-160

Buy this book

eBook $74.99
price for USA in USD (gross)
  • The eBook version of this title will be available soon
  • ISBN 978-3-540-46602-4
  • Digitally watermarked, DRM-free
  • Included format:
  • ebooks can be used on all reading devices
  • Immediate eBook download after purchase
Softcover $99.00
price for USA in USD
  • ISBN 978-3-540-54947-5
  • Free shipping for individuals worldwide
  • Usually dispatched within 3 to 5 business days.
Loading...

Services for this Book

Recommended for you

Loading...

Bibliographic Information

Bibliographic Information
Book Title
Specification and Compositional Verification of Real-Time Systems
Authors
Series Title
Lecture Notes in Computer Science
Series Volume
558
Copyright
1991
Publisher
Springer-Verlag Berlin Heidelberg
Copyright Holder
Springer-Verlag Berlin Heidelberg
eBook ISBN
978-3-540-46602-4
DOI
10.1007/3-540-54947-1
Softcover ISBN
978-3-540-54947-5
Series ISSN
0302-9743
Edition Number
1
Number of Pages
X, 242
Topics