Specification and Compositional Verification of Real-Time Systems. 1st ed. 1991

種類:

電子ブック

責任表示:

by Jozef Hooman

出版情報:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1991

著者名:

• Hooman, Jozef.
• SpringerLink (Online service)

シリーズ名:

Lecture Notes in Computer Science ; 558

ISBN:

9783540466024 [3540466029]    

注記:

Compositionality -- Compositionality and real-time -- Adding program variables -- Shared processors -- Concluding remarks.
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

ローカル注記:

学内専用E-BOOKS (local access only)