Specification and Compositional Verification of Real-Time Systems by JOZEF HOOMANSpecification and Compositional Verification of Real-Time Systems by JOZEF HOOMAN

Specification and Compositional Verification of Real-Time Systems


Paperback | November 27, 1991

Pricing and Purchase Info

$120.04 online 
$128.95 list price save 6%
Earn 600 plum® points

Prices and offers may vary in store


In stock online

Ships free on orders over $25

Not available in stores


The research described in this monograph concerns the formalspecification and compositional verification of real-timesystems. A real-time programminglanguage is considered inwhich concurrent processes communicate by synchronousmessage passing along unidirectional channels. To specifiyfunctional and timing properties of programs, two formalismsare investigated: one using a real-time version of temporallogic, called Metric Temporal Logic, and another which isbasedon extended Hoare triples. Metric Temporal Logicprovides a concise notationto express timing properties andto axiomatize the programming language, whereas Hoare-styleformulae are especially convenient for the verification ofsequential constructs. For both approaches a compositionalproof system has been formulated to verify that a programsatisfies a specification. To deduce timing properties ofprograms, first maximal parallelism is assumed, modeling thesituation in which each process has itsown processor. Next,this model is generalized to multiprogramming where severalprocesses may share a processor and scheduling is based onpriorities. The proof systems are shown to be sound andrelatively complete with respect to a denotational semanticsof the programming language. The theory is illustrated by anexample of a watchdog timer.
Title:Specification and Compositional Verification of Real-Time SystemsFormat:PaperbackDimensions:243 pagesPublished:November 27, 1991Publisher:Springer Berlin HeidelbergLanguage:English

The following ISBNs are associated with this title:

ISBN - 10:3540549471

ISBN - 13:9783540549475

Look for similar items by category:


Table of Contents

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