Shop : Details
Shop
Details
Jens Christoph Bürger, Hendrik Kausch, Deni Raco, Jan Oliver Ringert, Prof. Dr. rer. nat. Bernhard Rumpe, Sebastian Stüber, Marc Wiartalla
Towards an Isabelle Theory for distributed, interactive systems
The untimed case
This report describes a specification and verification framework for distributed interactive systems. The framework encodes the untimed part of the formal methodology FOCUS in the proof assistant Isabelle using domain-theoretical concepts. The key concept of FOCUS, the stream data type, together with the corresponding prefix-order, is formalized as a pointed complete partial order.
Furthermore, a high-level API is provided to hide the explicit usage of domain theoretical concepts by the user in typical proofs. Realizability constraints for modeling component networks with potential feedback loops are implemented. Moreover, a set of commonly used functions on streams are defined as least fixed points of the corresponding functionals and are proven to be prefix-continuous.
As a second key concept the stream processing function (SPF) is introduced describing a statefull, deterministic behavior of a message-passing component. The denotational semantics of components in this work is a defined set of stream processing functions, each of which maps input streams to output streams.
Furthermore, an extension of the framework is presented by using an isomorphic transformation of tuples of streams to model component interfaces and allowing composition. The structures for modeling component networks are implemented by giving names to channels and defining composition operators. This is motivated by the advantage that a modular modeling of component networks offers, based on the correctness of components of the decomposed system and using proper composition operators, the correctness of the whole system is automatically derived by construction.
Finally, a running example extracted from a controller in a car is realized to demonstrate and validate the framework.
Furthermore, a high-level API is provided to hide the explicit usage of domain theoretical concepts by the user in typical proofs. Realizability constraints for modeling component networks with potential feedback loops are implemented. Moreover, a set of commonly used functions on streams are defined as least fixed points of the corresponding functionals and are proven to be prefix-continuous.
As a second key concept the stream processing function (SPF) is introduced describing a statefull, deterministic behavior of a message-passing component. The denotational semantics of components in this work is a defined set of stream processing functions, each of which maps input streams to output streams.
Furthermore, an extension of the framework is presented by using an isomorphic transformation of tuples of streams to model component interfaces and allowing composition. The structures for modeling component networks are implemented by giving names to channels and defining composition operators. This is motivated by the advantage that a modular modeling of component networks offers, based on the correctness of components of the decomposed system and using proper composition operators, the correctness of the whole system is automatically derived by construction.
Finally, a running example extracted from a controller in a car is realized to demonstrate and validate the framework.
Schlagwörter: FOCUS; Formal verification; Theorem prover; Isabelle; Software engineering
Aachener Informatik-Berichte, Software Engineering
Herausgegeben von Prof. Dr. rer. nat. Bernhard Rumpe, Aachen
Band 45
Verfügbare Online-Dokumente zu diesem Titel
Sie benötigen den Adobe Reader, um diese Dateien ansehen zu können. Hier erhalten Sie eine kleine Hilfe und Informationen, zum Download der PDF-Dateien.
Bitte beachten Sie, dass die Online-Dokumente nicht ausdruckbar und nicht editierbar sind.
Bitte beachten Sie auch weitere Informationen unter: Hilfe und Informationen.
Bitte beachten Sie auch weitere Informationen unter: Hilfe und Informationen.
| Dokument |  | Gesamtdokument | ||
| Dateiart |  | |||
| Kosten |  | 26,85 € | ||
| Aktion |  | Zahlungspflichtig kaufen und anzeigen der Datei - 2,0 MB | ||
| Aktion |  | Zahlungspflichtig kaufen und download der Datei - 2,0 MB | ||
| Dokument |  | Inhaltsverzeichnis | ||
| Dateiart | | |||
| Kosten |  | frei | ||
| Aktion |  | Anzeigen der Datei - 237 kB | ||
| Aktion |  | Download der Datei - 237 kB | ||
Benutzereinstellungen für registrierte Online-Kunden (Online-Dokumente)
Sie können hier Ihre Adressdaten ändern sowie bereits georderte Dokumente erneut aufrufen.
Benutzer
Nicht angemeldet
Export bibliographischer Daten
Shaker Verlag GmbHAm Langen Graben 15a52353 Düren
Mo. - Do. 8:00 Uhr bis 16:00 UhrFr. 8:00 Uhr bis 15:00 Uhr
Kontaktieren Sie uns. Wir helfen Ihnen gerne weiter.
