| 书目名称 | Specification and Compositional Verification of Real-Time Systems | | 编辑 | Jozef Hooman | | 视频video | | | 丛书名称 | Lecture Notes in Computer Science | | 图书封面 |  | | 描述 | The research described in this monograph concerns the formalspecificationand 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, twoformalismsare 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 whereseveralprocesses may share a processor and scheduling is based onpriorities. The proof systems are shown to be sound andrelatively complete with respect to a denotational | | 出版日期 | Book 1991 | | 关键词 | formal specification; logic; modeling; programming; programming language; real-time; semantics; system; veri | | 版次 | 1 | | doi | https://doi.org/10.1007/3-540-54947-1 | | isbn_softcover | 978-3-540-54947-5 | | isbn_ebook | 978-3-540-46602-4Series ISSN 0302-9743 Series E-ISSN 1611-3349 | | issn_series | 0302-9743 | | copyright | Springer-Verlag Berlin Heidelberg 1991 |
The information of publication is updating
|
|
发表于 2025-3-21 19:26:59
