Buch, Englisch, Band 558, 242 Seiten, Format (B × H): 155 mm x 235 mm, Gewicht: 388 g
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.
Zielgruppe
Research
Autoren/Hrsg.
Fachgebiete
- Mathematik | Informatik Mathematik Mathematik Interdisziplinär Systemtheorie
- Interdisziplinäres Wissenschaften Wissenschaften: Forschung und Information Kybernetik, Systemtheorie, Komplexe Systeme
- Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Prozedurale Programmierung
- Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Software Engineering Objektorientierte Softwareentwicklung
- Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Programmierung: Methoden und Allgemeines
- Mathematik | Informatik EDV | Informatik Informatik Logik, formale Sprachen, Automaten
Weitere Infos & Material
Compositionality.- Compositionality and real-time.- Adding program variables.- Shared processors.- Concluding remarks.
