Hooman | Specification and Compositional Verification of Real-Time Systems | Buch | 978-3-540-54947-5 | sack.de

Buch, Englisch, Band 558, 242 Seiten, Format (B × H): 155 mm x 235 mm, Gewicht: 388 g

Reihe: Lecture Notes in Computer Science

Hooman

Specification and Compositional Verification of Real-Time Systems


1991
ISBN: 978-3-540-54947-5
Verlag: Springer Berlin Heidelberg

Buch, Englisch, Band 558, 242 Seiten, Format (B × H): 155 mm x 235 mm, Gewicht: 388 g

Reihe: Lecture Notes in Computer Science

ISBN: 978-3-540-54947-5
Verlag: Springer Berlin Heidelberg


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.

Hooman Specification and Compositional Verification of Real-Time Systems jetzt bestellen!

Zielgruppe


Research


Autoren/Hrsg.


Weitere Infos & Material


Compositionality.- Compositionality and real-time.- Adding program variables.- Shared processors.- Concluding remarks.



Ihre Fragen, Wünsche oder Anmerkungen
Vorname*
Nachname*
Ihre E-Mail-Adresse*
Kundennr.
Ihre Nachricht*
Lediglich mit * gekennzeichnete Felder sind Pflichtfelder.
Wenn Sie die im Kontaktformular eingegebenen Daten durch Klick auf den nachfolgenden Button übersenden, erklären Sie sich damit einverstanden, dass wir Ihr Angaben für die Beantwortung Ihrer Anfrage verwenden. Selbstverständlich werden Ihre Daten vertraulich behandelt und nicht an Dritte weitergegeben. Sie können der Verwendung Ihrer Daten jederzeit widersprechen. Das Datenhandling bei Sack Fachmedien erklären wir Ihnen in unserer Datenschutzerklärung.