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


voorkant	achterkant

ISBN:

978-3-8440-7265-5

Reeks:

Aachener Informatik-Berichte, Software Engineering
Uitgever: Prof. Dr. rer. nat. Bernhard Rumpe
Aachen

Volume:

Trefwoorden:

FOCUS; Formal verification; Theorem prover; Isabelle; Software engineering

Soort publicatie:

Dissertatie

Taal:

Engels

Pagina's:

262 pagina's

Gewicht:

390 g

Formaat:

24 x 17 cm

Bindung:

Softcover

Prijs:

35,80 € / 44,80 SFr

Verschijningsdatum:

Maart 2020

Kopen:

Download:

Beschikbare online documenten voor deze titel:

U heeft Adobe Reader, nodig, om deze bestanden te kunnen bekijken. Hier vindt u ondersteuning en informatie, bij het downloaden van PDF-bestanden.

Let u er a.u.b. op dat de online-bestanden niet drukbaar zijn.


	Document		Document
	Soort bestand		PDF
	Kosten		26,85 EUR
	Acties		Tonen en kopen van het bestand - 2,0 MB (2092039 Byte)
	Acties		Kopen en downloaden van het bestand - 2,0 MB (2092039 Byte)


	Document		Inhoudsopgave
	Soort bestand		PDF
	Kosten		gratis
	Acties		Het bestand tonen - 237 kB (243109 Byte)
	Acties		downloaden van het bestand - 237 kB (243109 Byte)

Gebruikersinstellingen voor geregistreerde online-bezoekers

Hier kunt u uw adresgegevens aanpassen en uw documenten inzien.

Gebruiker:	niet aangemeld
Acties:	aanmelden/registreren Paswoord vergeten?

Aanbevelen:

Wilt u dit boek aanbevelen?

Recensie-exemplaar

Bestelling van een recensie-exemplaar.

Verlinking

Wilt u een link hebben van uw publicatie met onze online catalogus? Klik hier.

Samenvatting

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.