Trier, Univ., Diss., 2002. / Erscheinungsjahr an der Haupttitelstelle: 2001. Computerdatei im Fernzugriff.

Trier, University, Diss., 2002. / Erscheinungsjahr an der Haupttitelstelle: 2001.

University, Diss., 2003--Freiburg (Breisgau).

Today, information and communication systems are ubiquitous and consist very often of several interacting and communicating components. One reason is the widespread use of multi-core processors and the increasing amount of concurrent software for the efficient usage of multi-core processors. Also, the dissemination of distributed emergent technologies like sensor networks or the internet of things is growing. Additionally, a lot of internet protocols are client-server architectures with clients which execute computations in parallel and servers that can handle requests of several clients in parallel. Systems which consist of several interacting and communicating components are often very complex and due to their complexity also prone to errors. Errors in systems can have dramatic consequenses, especially in safety-critical areas where human life can be endangered by incorrect system behavior. Hence, it is inevitable to have methods that ensure the proper functioning of such systems. This thesis aims on improving the verifiability of asynchronous concurrent systems using symbolic model checking based on Binary Decision Diagrams (BDDs). An asynchronous concurrent system is a system that consists of several components, from which only one component can execute a transition at a time. Model checking is a formal verification technique. For a given system description and a set of desired properties, the validity of the properties for the system is decided in model checking automatically by software tools called model checkers. The main problem of model checking is the state-space explosion problem. One approach to reduce this problem is the use of symbolic model checking. There, system states and transitions are not stored explicitely as in explicit model checking. Instead, in symbolic model checking sets of states and sets of transitions are stored and also manipulated together. The data structure which is used in this thesis to store those sets are BDDs. BDD-based symbolic model checking has already been used successful in industry for several times. Nevertheless, BDD-based symbolic model checking still suffers from the state-space explosion problem and further improvements are necessary to improve its applicability. Central operations in BDD-based symbolic model checking are the computation of successor and predecessor states of a given set of states. Those computations are called image computations. They are applied repeatedly in BDD-based symbolic model checking to decide the validity of properties for a given system description. Hence, their efficient execution is crucial for the memory and runtime requirements of a model checker. In an image computation a BDD for a set of transitions and a BDD for a set of states are combined to compute a set of successor or predecessor states. Often, also the size of the BDDs to represent the transition relation is critical for the successful use of model checking. To further improve the applicability of symbolic model checking, we present in this thesis new data structures to store the transition relation of asynchronous concurrent systems. Additionally, we present new image computation algorithms. Both can lead to large runtime and memory reductions for BDD-based symbolic model checking. Asynchronous concurrent systems often contain symmetries. A technique to exploit those symmetries to diminish the state-space explosion problem is symmetry reduction. In this thesis we also present a new efficient algorithm for symmetry reduction in BDD-based symbolic model checking. / In unserem Alltag kommen wir heute ständig mit Systemen der Informations- und Kommunikationstechnik in Kontakt. Diese bestehen häufig aus mehreren interagierenden und kommunizierenden Komponenten, wie zum Beispiel nebenläufige Software zur effizienten Nutzung von Mehrkernprozessoren oder Sensornetzwerke. Systeme, die aus mehreren interagierenden und kommunizierenden Komponenten bestehen sind häufig komplex und dadurch sehr fehleranfällig. Daher ist es wichtig zuverlässige Methoden, die helfen die korrekte Funktionsweise solcher Systeme sicherzustellen, zu besitzen. Im Rahmen dieser Doktorarbeit wurden neue Methoden zur Verbesserung der Verifizierbarkeit von asynchronen nebenläufigen Systemen durch Anwendung der symbolischen Modellprüfung mit binären Entscheidungsdiagrammen (BDDs) entwickelt. Ein asynchrones nebenläufiges System besteht aus mehreren Komponenten, von denen zu einem Zeitpunkt jeweils nur eine Komponente Transitionen ausführen kann. Die Modellprüfung ist eine Technik zur formalen Verifikation, bei der die Gültigkeit einer Menge von zu prüfenden Eigenschaften für eine gegebene Systembeschreibung automatisch durch Softwarewerkzeuge, die Modellprüfer genannt werden, entschieden wird. Das Hauptproblem der symbolischen Modellprüfung ist das Problem der Zustandsraumexplosion und es sind weitere Verbesserungen notwendig, um die symbolische Modellprüfung häufiger erfolgreich durchführen zu können. Bei der BDD-basierten symbolischen Modellprüfung werden Mengen von Systemzuständen und Mengen von Transitionen jeweils durch BDDs repräsentiert. Zentrale Operationen bei ihr sind die Berechnung von Nachfolger- und Vorgängerzuständen von gegebenen Zustandsmengen, welche Bildberechnungen genannt werden. Um die Gültigkeit von Eigenschaften für eine gegebene Systembeschreibung zu überprüfen, werden wiederholt Bildberechnungen durchgeführt. Daher ist ihre effiziente Berechnung entscheidend für eine geringe Laufzeit und einen niedrigen Speicherbedarf der Modellprüfung. In einer Bildberechnung werden ein BDD zur Repräsentation einer Menge von Transitionen und ein BDD für eine Menge von Zuständen kombiniert, um eine Menge von Nachfolger- oder Vorgängerzuständen zu berechnen. Oft ist auch die Größe von BDDs zur Repräsentation der Transitionsrelation von Systemen entscheidend für die erfolgreiche Anwendbarkeit der Modellprüfung. In der vorliegenden Arbeit werden neue Datenstrukturen zur Repräsentation der Transitionsrelation von asynchronen nebenläufigen Systemen bei der BDD-basierten symbolischen Modellprüfung vorgestellt. Zusätzlich werden neue Algorithmen zur Durchführung von Bildberechnungen präsentiert. Beides kann zu großen Reduktionen der Laufzeit und des Speicherbedarfs führen. Asynchrone nebenläufige Systeme besitzen häufig Symmetrien. Eine Technik zur Reduktion des Problems der Zustandsraumexplosion ist die Symmetriereduktion. In dieser Arbeit wird ebenfalls ein neuer effizienter Algorithmus zur Symmetriereduktion bei der symbolischen Modellprüfung mit BDDs aufgeführt.

University, Diss., 2005--Bonn.

京都大学 / 0048 / 新制・課程博士 / 博士(工学) / 甲第19742号 / 工博第4197号 / 新制||工||1647(附属図書館) / 32778 / 京都大学大学院工学研究科高分子化学専攻 / (主査)教授 吉崎 武尚, 教授 古賀 毅, 准教授 竹中 幹人 / 学位規則第4条第1項該当 / Doctor of Philosophy (Engineering) / Kyoto University / DFAM

Il y a un besoin grandissant pour d'autonomie dans des systèmes temps réel complexes tels que les robots ou les satellites. Ceci met en avant un problème non trivial : d'un côté il y a des systèmes complexes - donc difficiles à valider - avec une intervention de l'humain dans la boucle qui se veut minimale, de l'autre nous avons des domaines où il faut que le système ait un comportement sûr fonctionnellement afin d'éviter les coûts financiers et/ou humains d'une perte ou d'une détérioration du système. Ces deux notions mises en vis-à-vis semblent contradictoires. En effet comment être sûr qu'un système autonome avec un pouvoir décisionnel fort, n'aura pas un comportement non nominal qui pourra menacer le bon déroulement de la mission ? Comment être sûr qu'un satellite n'allumera pas ses réacteurs sans avoir protégé ses capteurs fragiles (objectif de la caméra, ...) ? Une réponse partielle à ce type de problèmes pourrait être d'utiliser un planificateur de haut niveau qui ne donnerait que des plans garantis comme sûrs et valides. Toutefois ces planificateurs n'ont pas un modèle complet des actions qu'ils effectuent et de leurs conséquences. En effet, les directives données par ce planificateur sont généralement affinées en sous tâches par un superviseur. Le planificateur n'a donc pas un contrôle complet sur le moyen d'effectuer cette action. Nous présentons ici les travaux effectués afin d'intégrer un système de contrôle d'exécution en ligne dans une architecture hiérarchisée. Nous décrivons ici la nécessité et le rôle d'un tel composant dans ce type d'architecture. Nous introduisons le R2C, notre contrôleur basé sur les hypothèses synchrones, ainsi que l'outil permettant sa génération en exploitant des techniques issues du model-checking symbolique. Enfin nous discutons de la nécessité de prendre en compte les com-posants décisionnels dans le contrôle afin d'interférer le moins possible avec les décisions prises par ceux-ci. Les résultats obtenus durant des expérimentations sur une plate-forme robotique confirment les idées développées au cours de ce travail et permettent d'en tirer les conclusions et perspectives sur la mise en place d'un contrôle pour l'amélioration de la fiabilité globale de tels systèmes.