Loading…
Formal Modeling, Simulation, and Validation of Communication Platforms
Modica, Tony
Kommunikationsbasierte Systeme, welche sich nach Menschen und deren Bedürfnissen orientieren, erlangten in den letzten Jahren immer größere Bedeutung und Interesse. Bislang gibt es allerdings keine angemessene umfassende Modellierungstechnik für diese Art von Kommunikationsplattformen, welche es erlauben würden, das Benutzerverhalten in derartigen Systemen formal zu modellieren, zu simulieren und zu validieren. In dieser Dissertation stellen wir eine geeignete Integration von algebraischen high-level Petrinetzen und high-level Ersetzungssystemen vor, um diese Lücke zu schließen. Von der theoretischen Seite her erfordert dies, eine Theorie algebraischer high-level Netze zu entwickeln, so dass einerseits die entsprechenden high-level Ersetzungssysteme den Eigenschaften M-adhesiver Transformationssysteme genügen und andererseits der Entwickler von Kommunikationsplattformen deren Schaltverhalten und regelbasierte Modifikation innerhalb eines Frameworks modellieren und analysieren kann. Von der konzeptuellen Seite her können wir nachweisen, dass typische Eigenschaften von Kommunikationsplattformen innerhalb dieses Frameworks unter Vewendung geeigneter Modellierungstechniken modelliert und validiert werden können, wie etwa Anrufe, Chats zwischen verschiedenen Benutzern, Konferenzen, Datenmulticasting, sowie Plattform-Constraints und andere. Dies demonstrieren wir anhand von Skype, welches uns durch die ganze Arbeit als Leitfaden, Beispiel und umfassende Fallstudie dient. Abschließend beschreiben wir die Entwicklung eines visuellen Werkzeugs für Kommunikations\-platt\-formen in Eclipse, welches den Entwickler beim Modellieren, Simulieren und Validieren unterstützt.
Human-centric communication-based systems, including social networks as Skype, Facebook, and Second Life, have been of increasing interest throughout the last years. Up to now, however, there are no adequate modeling techniques for this kind of communication platforms that would allow formal modeling, simulation, and validation of the user behavior. In this thesis, we propose a suitable integration of algebraic high-level Petri nets and high-level replacement systems, based on well-known graph transformation techniques, in order to close this gap. On the theoretical side, this requires to develop a theory of algebraic high-level nets with individual tokens, such that the corresponding high-level replacement systems satisfy the requirements of M-adhesive transformation systems and allow the platform designer to model and to analyze token-firing and rule-based modification within a single framework. On the conceptual side, we are able to show that typical features of communication platforms such as direct calls, multi-user chats, conferences, data multicasting, platform constraints and other requirements can be modeled and validated in this framework combining suitable modeling techniques. This is demonstrated for Skype, which is used as a running example and case study. Last but not least, it is shown how to develop a visual Eclipse-based tool for communication platforms, which supports modeling, simulation, and validation of typical scenarios.
