Willkommen, schön sind Sie da!
Logo Ex Libris

Specification and Compositional Verification of Real-Time Systems

  • Kartonierter Einband
  • 252 Seiten
(0) Erste Bewertung abgeben
Bewertungen & Rezensionen
(0)
(0)
(0)
(0)
(0)
Alle Bewertungen ansehen
The research described in this monograph concerns the formal specification and compositional verification of real-time systems. A ... Weiterlesen
20%
100.00 CHF 80.00
Sie sparen CHF 20.00
Print on Demand - Auslieferung erfolgt in der Regel innert 4 bis 6 Wochen.
Bestellung & Lieferung in eine Filiale möglich

Beschreibung

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.

This monograph presents two formal methods for the specification and compositional verification of real-time systems. One uses a real-time extension of temporal logic and the other is based on extended Hoare triples. Programs consist of concurrent processes with synchronous message passing. The maximal parallelism model is extended to multiprogramming.

Klappentext

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.



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

Produktinformationen

Titel: Specification and Compositional Verification of Real-Time Systems
Autor:
EAN: 9783540549475
ISBN: 3540549471
Format: Kartonierter Einband
Herausgeber: Springer Berlin Heidelberg
Anzahl Seiten: 252
Gewicht: 388g
Größe: H235mm x B155mm x T13mm
Jahr: 1991
Untertitel: Englisch
Auflage: 1991

Weitere Produkte aus der Reihe "Lecture Notes in Computer Science"