The growing influence of telecommunication-systems in all areas has brought with it the need for elaborate and reliable software running on concurrent and, in particular, dynamically changing systems. With the development of such systems becoming ever more complex, the outline and development of mechanized and mechanizable verification-techniques is indispensable. This overall goal can be divided into three tasks: (1) outline of a framework in which (2) complex systems can be analysed, and the (3) design and implementation of efficient proof-techniques. It is certainly beyond the scope of a thesis to provide an integrated framework dealing with these questions within one environment. This work therefore concentrates on dominant aspects of each of the three tasks in separate discussions. A major result of the thesis is that the approaches outlined for each of the three questions obviously fit together, so that they can be used as a basis for the development of an integrated framework. Often automatic verification of larger hardware- and software-applications is impossible, because the systems are too large or even infinite. This thesis focusses on infinite-state and parameterized systems, and builds tool-support on interactive theorem-proving. Further, it concentrates on the validation of correct implementations by exploiting behavioural reasoning. It demonstrates how to apply various techniques to tackle proofs about infinite-state and parameterized systems with large descriptions, discusses the support that theorem-provers can offer, and presents a foundational platform for reasoning about mobile systems in a general-purpose theorem-prover. Several design-decisions have to be taken. This thesis uses process-algebra as a framework, in particular CCS for the description and analysis of infinite-state reactive systems, and the pi-calculus for the discussion of mobile and higher-order systems. For a validation, it applies observation-equivalence, exploiting a range of proof-techniques that have been developed for the two calculi. For all mechanizations, the general-purpose theorem-prover Isabelle/HOL is used.     «

The growing influence of telecommunication-systems in all areas has brought with it the need for elaborate and reliable software running on concurrent and, in particular, dynamically changing systems. With the development of such systems becoming ever more complex, the outline and development of mechanized and mechanizable verification-techniques is indispensable. This overall goal can be divided into three tasks: (1) outline of a framework in which (2) complex systems can be analysed, and the (...     »

Mit dem zunehmenden Einfluß von Telekommunikationssystemen in allen Bereichen steigt auch der Bedarf an zuverlässiger Software für verteilte und insbesondere dynamisch veränderliche Systeme. Da die Entwicklung derartiger Systeme immer komplexer wird, ist die Konzipierung und Bereitstellung mechanisierter und mechanisierbarer Verifikationstechniken unabdingbar. Dieses globale Ziel läßt sich in drei Aufgaben zerlegen: (1) die Konzipierung einer Umgebung, in der (2) komplexe Systeme analysiert werden können, sowie (3) Design und Implementierung effizienter Beweistechniken. Eine einzelne Dissertation kann natürlich keine integrierte Umgebung bezüglich dieser drei Fragestellungen bereitstellen. Die vorliegende Arbeit konzentriert sich daher in separaten Diskussionen auf herausragende Aspekte jeder einzelner der obengenannten Aufgaben. Ein wichtiges Resultat der Dissertation ist, daß die dabei entwickelten Techniken offensichtlich harmonieren und somit als Grundlage für eine integrierte Umgebung dienen können. Eine automatische Verifizierung größerer Hardware- und Softwareanwendungen ist oft wegen zu großer oder sogar unendlicher Zustandsräume unmöglich. Die vorliegende Arbeit konzentriert sich daher in separaten Diskussionen auf herausragende Aspekte jeder einzelner der obengenannten Aufgaben. Ein wichtiges Resultat der Dissertation ist, daß die dabei entwickelten Techniken offensichtlich harmonieren und somit als Grundlage für eine integrierte Umgebung dienen können. Eine automatische Verifizierung größerer Hardware- und Softwareanwendungen ist oft wegen zu großer oder sogar unendlicher Zustandsräume unmöglich. Die vorliegende Arbeit konzentriert sich auf unendliche und parametrisierte Systeme und verwendet interaktives Theorembeweisen. Dabei geht es vordringlich um die Validierung korrekter Systeme auf der Basis einer operationellen Argumentationsweise. Es wird gezeigt, wie sich verschiedene Beweistechniken auf unendliche und parametrisierte Systeme anwenden lassen, und welche Unterstützung dabei Theorembeweiser bieten können. Darüber hinaus wird eine grundlegende Beweiserplattform für mobile Systeme geschaffen. Verschiedene Designentscheidungen mußten getroffen werden. Die Arbeit basiert auf der Verwendung von Prozeßalgebren, insbesondere CCS für die Beschreibung und Analyse unendlicher reaktiver Systeme, sowie dem Pi-Kalkül für die Diskussion mobiler Systeme und solcher höherer Ordnung. Zur Validierung wird Beobachtungsäquivalenz verwendet, wobei eine Reihe von Beweistechniken Verwendung findet. Alle Mechanisierungen verwenden den Theorembeweiser Isabelle/HOL.     «

Mit dem zunehmenden Einfluß von Telekommunikationssystemen in allen Bereichen steigt auch der Bedarf an zuverlässiger Software für verteilte und insbesondere dynamisch veränderliche Systeme. Da die Entwicklung derartiger Systeme immer komplexer wird, ist die Konzipierung und Bereitstellung mechanisierter und mechanisierbarer Verifikationstechniken unabdingbar. Dieses globale Ziel läßt sich in drei Aufgaben zerlegen: (1) die Konzipierung einer Umgebung, in der (2) komplexe Systeme analysiert werd...     »