Analysis of communication topologies by partner abstraction [Elektronische Ressource] / von Jörg Bauer

Analysis of CommunicationTopologies by PartnerAbstractionDissertationzur Erlangung des Grades desDoktors der Ingenieurwissenschaften (Dr.-Ing.) derNaturwissenschaftlich-Technischen Fakult¨aten derUniversit¨at des SaarlandesvonDiplom-InformatikerJ¨org BauerSaarbruc¨ kenSeptember 2006iiTag des Kolloquiums: 13.12.2006Dekan: Prof. Dr.-Ing. Thorsten HerfetPrufungsa¨ usschuss:Vorsitzender: Prof. Dr. Holger HermannsUniversit¨at des Saarlandes, Saarbruc¨ kenGutachter: Prof. Dr. Reinhard WilhelmUniversit¨at des Saarlandes, Saarbruc¨ kenProf. Dr. Werner DammCarl von Ossietzky Universit¨at, OldenburgProf. Dr. Arend RensinkUniversity of Twente, EnschedeAkademischerMitarbeiter: Dr. Jan SchwinghammerAbstractDynamic communication systems are hard to verify due to inherent un-boundedness. Unbounded creation and destruction of objects and a dynam-ically evolving communication topology are characteristic features. Promi-nent examples include traffic control systems based on wireless communi-cation and ad hoc networks. As dynamic communication systems have tomeet safety-critical requirements, this thesis develops appropriate specifica-tion and verification techniques for them. It is shown that earlier attemptsat doing so have failed.Partner graph grammars are presented as an adequate specification for-malism for dynamic communication systems.