Heutzutage besteht ein komplexes Software-System häufig aus lose gekoppelten, interagierenden Komponenten. Eine Komponente ist ein offenes System, das unabhängig von anderen offenen Systemen entwickelt und später mit diesen komponiert wird. Die Komposition L+R zweier offener Systeme L und R kann sich jedoch inkorrekt verhalten, beispielsweise verklemmen (die Komponenten warten gegenseitig aufeinander), in eine Endlosschleife geraten oder unbeschränkten Speicherplatz erfordern. Ist L+R dagegen ein korrektes System, bezeichnet man L und R als Partner voneinander. Formale Methoden der Modellierung, Analyse und Synthese ermöglichen die systematische Konstruktion eines korrekten Systems durch Komposition von Partnern. Die Kosten, die ein offenes System L verursacht, variieren in Abhängigkeit von der konkreten Wahl eines Partners. Es ist daher wünschenswert, L nur mit solchen Partnern zu komponieren, welche die Kosten von L beschränken oder sogar minimieren. Ein Partner, der die Kosten von L minimiert, ist ein optimaler Partner von L. Ziel dieser Arbeit ist die Erarbeitung von Techniken, die garantieren, dass L nur mit optimalen Partnern komponiert wird. Dazu entwickeln wir formale Methoden zur Modellierung, Analyse und Synthese kostenbehafteter offener Systeme und ihrer optimalen Partner. Wir präsentieren einen Formalismus zur Modellierung funktionaler (d.h. Zustandsübergänge) und nicht-funktionaler Verhaltenseigenschaften (d.h. Kosten). In diesem Formalismus definieren wir Kostenbeschränktheit und Optimalität von Partnern. Darauf aufbauend entwickeln wir formale Methoden zur Entscheidung der kostenbeschränkten Bedienbarkeit (d.h. der Existenz kostenbeschränkter Partner), der Synthese optimaler Partner und der endlichen Repräsentation aller optimalen Partner. / Nowadays, a complex software system usually consists of loosely-coupled, interacting components. Such a component is an independently developed open system that one composes with other open systems. The composition L+R of two open systems L and R can be faulty: For instance, the components deadlock (i.e. mutually wait for each other) or require an unbounded amount of memory. If L+R is correct, L and R are called partners of each other. Formal methods for modeling, analysis and synthesis yield a systematic approach to constructing a correct system by means of composing partners. The costs of executing a given open system L vary based on a chosen partner. Therefore, it is desirable to choose a partner that bounds or even minimizes the costs of executing L. If a partner R minimizes the costs of executing L, then R is an optimal partner of L. Our goal is to develop techniques that guarantee the composition of L with optimal partners. To this end, we develop formal methods of modeling, analysis and synthesis of open systems incorporating costs. We present a formalism to model functional aspects (i.e. states and transitions) and non-functional aspects (costs) of behavior. We define the properties of cost boundedness and cost optimality for partners in this formalism. Based thereon, we develop formal methods to decide cost bounded controllability (i.e. the existence of cost bounded partners), to synthesize optimal partners, and to finitely represent the set of all optimal partners.
| Identifer | oai:union.ndltd.org:HUMBOLT/oai:edoc.hu-berlin.de:18452/17860 |
| Date | 05 May 2015 |
| Creators | Sürmeli, Jan |
| Contributors | Reisig, Wolfgang, Droste, Manfred, Popova-Zeugmann, Louchka |
| Publisher | Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät |
| Source Sets | Humboldt University of Berlin |
| Language | German |
| Detected Language | English |
| Type | doctoralThesis, doc-type:doctoralThesis |
| Format | application/pdf |
| Rights | Namensnennung - Keine kommerzielle Nutzung - Keine Bearbeitung, http://creativecommons.org/licenses/by-nc-nd/3.0/de/ |
Page generated in 0.0031 seconds