Forschungsbericht der Otto-Friedrich-Universität Bamberg 2004
Interoperabilität und Middleware-Abstraktion
Yüklə 2,2 Mb. Pdf görüntüsü
|
- Bu səhifədəki naviqasiya:
- Middleware-Plattformen für Multi-Agentensysteme Projektleitung
- Peer-to-Peer Middleware Projektleitung
- Scheduling in Zustands-basierten Systemen Projektleitung
- Professur für Grundlagen der Informatik Anschrift
- Wissenschaftliche Tagungen
- Forschungsprojekte Compositionality for Synchronous Visual Programming Languages Projektleitung
- Lax Logic in Formal System Design Projektleitung
- Förderer
- Proofs-as-Delays: Verzögerungsanalyse in Intuitionistischer Logik Projektleitung
|
Interoperabilität und Middleware-Abstraktion Stichwörter: SOA, Client/Server-Archi- tekturen, Webservices, RPC
Beginn: 1.1.2003 Das Konzept der Web Services stellt den Versuch dar, eine Basis für die Kooperation zwischen unterschiedlichen Umgebungen zu eta- blieren. Als Grundlage dient diesem Konzept eine Client/Server-Ar- chitektur welche eine lose Kopplung zwischen den beteiligten Interaktionspartnern annimmt. Die Bemühungen in diesem Zusam- menhang konzentrieren sich momentan auf die Spezifikation von Standards für einzelne Teilaspekte. Darüber hinaus bieten unter- schiedliche Hersteller Plattformen für die Implementierung von Web Services an. Ein Erfolg des Konzeptes ist nur als erreichbar anzuse- hen, wenn seine Umsetzungen in der gewünschten Weise interagie- ren können. Erste Arbeiten in dieser Richtung befassen sich mit der Analyse un- terschiedlicher Plattformen in Bezug auf ihre Interaktionsfähigkeit zum Gegenstand und zeigen bestehende Probleme sowie mögliche Lösungen auf. Die Forschung zum Themenkomplex Web Services soll als Grundlage für die weitere Arbeiten in den Bereichen Intero- perabilität und Middleware-Abstraktion dienen. Ziel ist die Spezifi- kation und prototypische Implementierung einer Abstraktions- schicht, die eine einheitliche Schnittstelle für unterschiedliche Um- gebungen zur Verfügung stellt und gleichzeitig von der zugrunde lie- genden Infrastruktur abstrahiert. Somit wäre eine Integration und Koexistenz unterschiedlicher Plattformen möglich. Web Services können in diesem Zusammenhang eine Art Brückenfunktion über- nehmen. Somit würde die tatsächlich eingesetzte Middlware wei- testgehend austauschbar, ohne dass sich Auswirkungen über die Abstraktionsschicht hinaus ergäben. Als Konsequenz ergäbe sich eine Trennung unterschiedlicher Gesichtspunkte bei der Entwick- lung von Software. Zusätzlich wird eine möglichst weitgehende Aus- schöpfung des Automatisierungspotentials bei wiederkehrenden Aufgaben im Kontext der jeweiligen Middleware angestrebt.
Forschungsbericht der Otto-Friedrich-Universität Bamberg Seite 911 Middleware-Plattformen für Multi-Agentensysteme Projektleitung: Prof. Dr. rer. nat. Guido Wirtz
Sven Kaffille, MScIS Stichwörter: Agenten, FIPA, Plattform, ACL
Kaffille, Sven Telefon 0951 863 2812, Fax 0951 863 5528, E- Mail: sven.kaffille@wi- ai.uni-bamberg.de Software Agenten werden als neues Paradigma zur Entwicklung und Realisierung von komplexen Softwaresystemen angesehen. Ein Software Agent ist ein autonomes Programm, das im Sinne seines Besitzers handelt und zu reaktiven und proaktiven Handlungen fähig ist. Interagieren mehrere Software Agenten miteinander zur Lösung ihrer Aufgaben oder auch zur Lösung einer gemeinsamen Aufgabe, spricht man von einem Multi-Agentensystem. Gerade durch das In- ternet entsteht die Möglichkeit, dass Agenten verschiedener Besit- zer miteinander interagieren. Dabei können die Software Agenten mit Hilfe unterschiedlicher Hard- u. Software-Technologien realisiert sein. Eben diese Heterogenität erfordert offene, standardisierte Schnittstellen über die Agenten miteinander interagieren können. Über diese Schnittstellen hinaus, werden Koordinationsmechanis- men und Protokolle zur Verhandlung zwischen Agenten benötigt, so dass trotz der Autonomie einzelner Agenten ein funktionierendes Gesamtsystem entsteht. In diesem Bereich gibt es verschiedene An- sätze, die diese sozialen Aspekte von Software Agenten untersu- chen, und versuchen mit Hilfe bereits bestehender Theorien wie z.B. der Organisations- o. Spieltheorie zu erklären. Das Ziel ist es diese Ansätze zu untersuchen und aus ihnen diejeni- gen, die generell für Software Agenten einsetzbar sind, auszuwäh- len und gegebenenfalls zu kombinieren. Des Weiteren werden diese in einer standardkonformen Middleware-Plattform realisiert, die als Framework zur Realisierung autonomer und sozialer Agenten dienen soll. Mit dieser Plattform wird die Einsetzbarkeit der ausgewählten Ansätze in verschiedenen Anwendungsgebieten evaluiert und mit ihrer Hilfe werden gegebenenfalls Empfehlungen zur weiteren Aus- arbeitung der Standards zur besseren Interaktion von autonomen und sozialen Software Agenten und deren Plattformen abgeleitet. Die bisherige Arbeit in diesem Gebiet umfasst die Evaluierung zwei bestehender Standards für Multi-Agentensysteme und Plattformen für Multi-Agentensysteme. Für diese beiden Standards wurde eine Integration vorgeschlagen, die in einer Plattform für Multi-Agenten- systeme realisiert wurde. Zusätzlich wurde im Rahmen einer Di- plomarbeit ein generischer Parser für standardisierte Agentenkom- munikation entwicjelt und realisiert. Publikationen 1. Kaffille, Sven ; Wirtz, Guido: Integrating MASIF and FIPA Standards for Agent and Agent System Interoperability . In: PDCS 2003 (Veranst.) : Proc. 7th Interntional Conference on Software Engineering and Applications (SEA 2003), Marina del Rey, CA (USA) 03.- 05.11.2003). 2003, S. 798-806. Forschungsbericht der Otto-Friedrich-Universität Bamberg Seite 912 Peer-to-Peer Middleware Projektleitung: Prof. Dr. rer. nat. Guido Wirtz
Karsten Loesing, MScIS Stichwörter: Peer-to-Peer; middleware; view-consistency
Loesing, Karsten Telefon 0951 863 2810, Fax ++49-951/8635528, E-Mail: karsten.loe- sing@wiai.uni-bam- berg.de Peer-to-Peer-Systeme sind verteilte Systeme, in denen im Gegen- satz zu Client/Server-Systemen keine Unterscheidung zwischen Dienstanbietern und -nutzern gemacht wird. Die Kommunikation findet ohne zentrale Kontrollinstanz zwischen den Teilnehmern (Peers) statt. Dabei müssen Peer-to-Peer-Netzwerke dynamische Netzwerkänderungen wie Knoten- und Verbindungsausfälle kom- pensieren können. Peer-to-Peer-Systeme versprechen skalierbarer und fehlertoleranter als gewöhnliche Client/Server-Architekturen zu sein. Demgegenüber bieten sie neue Herausforderungen an die Ent- wicklung, da bisher zentral gelöste Probleme mit verteilten Algorith- men in unsicheren Netzwerken bewerkstelligt werden müssen. Hierzu ist es notwendig, dem Entwickler von P2P-Anwendungen eine einheitliche Middleware zu bieten, die von den Spezifika von P2P- Systemen abstrahiert und ein einheitliches Programmiermodell zur Verfügung stellt. Die bisherige Arbeit in diesem Gebiet beschäftigt sich mit der Schaf- fung einer Middleware für zuverlässige Gruppenkommunikation ba- sierend auf dem Konzept der View Consistency in P2P-Netzwerken. Dazu wurde ein neues Gruppenkommunikationsprotokoll vorge- schlagen und basierend auf der P2P-Middleware JXTA implemen- tiert. Als langfristige Perspektive wird die Entwicklung oder der Beitrag zu einer P2P-Middleware angestrebt. Weitere Arbeiten be- schäftigen sich mit der Untersuchung vorhandener P2P-Middleware- Plattformen und P2P-Anwendungen. Zum einen steht dabei das von einer möglichen Middleware angebotene Programmiermodell im Mittelpunkt. Zum anderen sollen Einzelaspekte wie direkte Konnek- tivität zwischen Knoten oder Algorithmen zur Replikation von Daten als Bausteine für eine solche Middleware betrachtet werden.
Prof. Dr. rer. nat. Guido Wirtz
Jens Bruhn, MScIS, Sven Kaffille, MScIS
Scheduling, State-based services, Petri-Netze
Bruhn, Jens Telefon 0951 863 2811, Fax 0951 863 5528, E- Mail: jens.bruhn@wi- ai.uni-bamberg.de In einem beliebig weit verteilten System ist die Annahme, dass alle Dienste zu jederzeit in der gleichen Art und Weise verfügbar sind, in vielen Fällen zu optimistisch. Häufig treten Situationen auf, in denen nur eine eingeschränkte Funktionalität zur Verfügung steht. In die- sem Fall ist ein naiver z.B. RPC-basierter Ansatz, der entfernte Dien- ste wie lokale Dienste bedingungslos blockierend aufruft, eine zusätzliche Fehlerquelle für die Gesamtfunktionalität eines Systems. Ursachen für solche Situationen werden einerseits im Kontext von Quality-of-Service Überlegungen allgemein untersucht, z.B. basie- rend auf Annahmen zu Servern, Netzwerken usw. Mindestens genauso wichtig sind aber Fälle, in denen die spezifische Semantik eines Dienstes selbst dazu führt, dass nur bestimmte Auf- rufsequenzen die erwartete Funktionsweise garantieren. Hier han- delt es sich um Dienste, deren extern sichtbarer Zustand eine notwendige Information über ihre korrekte Nutzung liefert. Die Be- nutzungsprotokolle für solche Dienste können z.B. mit Endlichen Automaten oder Petrinetzen beschrieben werden, was ihre statische Analyse erleichtert. Aus Sicht einer implementierenden Dienstumgebung muss der Zu- standsaspekt natürlich ebenfalls berücksichtigt werden. Dies gilt Forschungsbericht der Otto-Friedrich-Universität Bamberg Seite 913 insbesondere für das Scheduling von Diensten auf Serverseite. Zur Handhabung dieser Probleme wurde ein Scheduling Framework um- gesetzt. Dieses Framework beinhaltet neue Aspekte in Bezug auf die Möglichkeit Scheduler hierarchisch zu organisieren. Darüber hinaus wurde eine Abstraktion von der zugrunde liegenden Middleware so- wie ein hoher Grad an Ausfallsicherheit und Selbstorganisation er- reicht. Längerfristige Ziele des Projekts sind • die Integration aktueller Ergebnisse aus der Typentheorie, insbeson- dere Verhaltens-basierte Typisierung von Diensten, sowie • die Weiterentwicklung zu einem umfassenden, auf Typhierarchien aufbauenden, Schedulingsystem, das Plattformunabhängig z.B. für Webservices und andere Middleware nutzbar ist.
Forschungsbericht der Otto-Friedrich-Universität Bamberg Seite 914 Professur für Grundlagen der Informatik Anschrift: Feldkirchenstraße 21, 96045 Bamberg Leitung: Prof. Michael Mendler, Ph.D.
BEng Joaquin Aguado, MSc
Heidrun Fichtel Nicht zuletzt durch das enorme Wachstumspotenzial des Internets angetrieben stützt sich moderne Informationstechnik in Wirtschaft, Banken und der Verwaltung in zunehmendem Maße auf verteilte ko- operative Systeme (z.B. Telekommunikation, Web-Dienste, Soft- wareagenten, Mobile Systeme). Diese stellen nach Art und Umfang bisher nicht gekannte Anforderungen an die technische Robustheit und Sicherheit. Zur technischen Robustheit zählen Eigenschaften wie Fehlertoleranz, Verzögerungsunabhängigkeit sowie Skalierbar- keit, zur Sicherheit Bedürfnisse wie Datenintegrität, Anonymität, Authentizität und Verifizierbarkeit. Um hier die Lücke zwischen Wunsch und technischer Realisierbarkeit zu schliessen, müssen un- ter anderem neuartige, flexible Interaktionsprotokolle und Synchro- nisationsverfahren entwickelt werden, die dem Aspekt der Nebenläufigkeit Rechnung tragen und die für die heterogene Kopp- lung bzw. Integration sowohl von Software- als auch von Hardware- komponenten geeignet sind. An der Professur für Grundlagen der Informatik werden innovative Synchronisations- und Interaktionsmodelle sowie methodische Werkzeuge zur formalen Analyse (Verifikation und Test) von verteil- ten sowie reaktiven Systemen erforscht und entwickelt. Besonderes Interesse gilt dabei den Sicherheitsprotokollen und der Beschrei- bung von standardisierten Kommunikationsschnittstellen, welche die komponentenorientierte Entwicklung und Implementierung von kooperierenden Informationssystemen ermöglicht. Forschungsschwerpunkte • Prozesskalküle, Synchronie und Asynchronie • Intuitionistische und Modale Logik und Typentheorie, logische Spiel- theorie
• Semantik synchroner und visueller Programmiersprachen (UML, Statecharts) • Abstraktion und Verfeinerung, Constraints und das Kompositionali- tätsproblem • Automatische und interaktive Validierungsverfahren: Modellprüfung, Verzögerungsanalyse, Typprüfung, Theorembeweisen Kooperationsbeziehungen • Europäisches Forschungsnetzwerk TYPES (35 akademische und in- dustrielle Forschergruppen aus 11 europäischen Ländern) im 6. Rah- menprogramm • Universität Sheffield, Großbritannien • Universität York, Großbritannien Wissenschaftliche Tagungen • Intuitionistic Modal Logic and Applications (IMLA’99), Trento, Italien, Juli 1999 • Intuitionistic Modal Logic and Applications (IMLA’02), Kopenhagen, Dänemark, Juli 2002
Forschungsbericht der Otto-Friedrich-Universität Bamberg Seite 915 • Semantic Foundations of Engineering Design Languages (SFEDL’02), Grenoble, Frankreich, April 2002 • Semantic Foundations of Engineering Design Languages (SFEDL’04), Barcelona, Spanien, April 2004 • Synchronous Programming (SYNCHRON 2004), Dagstuhl Tagung, Dezember 2004 Forschungsprojekte Compositionality for Synchronous Visual Programming Languages Projektleitung: Prof. Michael Mendler, Ph.D.
BEng Joaquin Aguado, MSc Lüttgen, Gerald Beginn: 1.12.2002 Synchronous languages such as Esterel or Statecharts with their un- derlying cycle-based computation principle (synchrony hypothesis, maximal progress, run-to-completion) are very popular among en- gineers and widely used in the programming of reactive and embed- ded systems. Traditionally, the development platforms for such languages were built mainly with simulation and code-generation in mind. Only recently increasing efforts are being made on the inte- gration of semantic validation techniques (model-checking, theo- rem-proving, test sequence generation, etc). These efforts depend crucially on modular semantics of the standard two-level micro- macro step model which are notoriously hard to come by. In this project aims to show how the Synchronoy Hypothesis and some of the recent successful proposals for solving the compositio- nality problem for Statecharts and Esterel can be understood in a game-theoretic way. Technically, synchronous programs are map- ped into finite two-player games in such a way that the analysis of signal statuses is reflected in the computation of winning strategies. This game-theoretic approach offers a new semantical foundation for synchronous languages. Publikationen 0XX
1. Aguado, Joaquin ; Luettgen, G. ; Mendler, Michael: A-maze-ing Esterel . In: Maraninchi, F. ; Girault, A. ; Rutten, E. (Hrsg.) : Synchronous Languages, Applications and Programming (SLAP‘03 Porto, Portugal July 2003). 2003, S. 15 Seiten. (Electronic Notes in Theoretical Computer Science Bd. to appear) Lax Logic in Formal System Design Projektleitung: Dr. Matt Fairtlough Beteiligte: Prof. Michael Mendler, Ph.D. Dr. Xiaochun Cheng, The University of Reading, UK Stichwörter: System Design and Formal Verification, Abstraction and Refinement, Intuitio- nistic Modal Logic
5.2.2002
Förderer: British EPSRC Project Objectives: • to develop a general theory of abstraction and refinement at multiple abstraction levels and to specialise it to provide a logical and cohe- rent account of how to handle behavioural constraints during formal hardware and software synthesis. • to improve the technology of formal system design by building a sy- stem centred on a generic mechanism for constraint-handling, toge- ther with concrete constraint packages for timing, data and structure. • to demonstrate the adequacy of the theory and the usefulness of the implementation by means of a substantial case study of formal syn- thesis.
Forschungsbericht der Otto-Friedrich-Universität Bamberg Seite 916 Publikationen 0XX
1. Fairtlough, M. ; Mendler, Michael ; Cheng, X.: Abstraction and refinement in higher-order logic . In: Boulton, R. J. ; Jackson, P. B. (Hrsg.) : International Conference on Theorem Proving in Higher-order Logic (TPHOLs‘2001 Edinburgh September 2001). 2001, S. 201- 216. (LNCS Bd. 2152) 2. Fairtlough, M. ; Mendler, Michael ; Moggi, E. (Hrsg.): Modalities in Type Theory . Cambridge : Cambridge University Press, 2001 (Special Issue of Mathematical Structures in Computer Science Bd. 11, Nr. 4) . - 90 Seiten. 3. Cheng, X. ; Fairtlough, M. ; Mendler, Michael: Proofs as constraints for abstraction and re- finement. . In: Egly, U. ; Fiedler, A. ; Horacek, H. ; Schmitt, S. (Hrsg.) : Workshop on Proof Transformations, Proof Presentations and Complexities of Proof (PTP ’01 Siena, Universitá degli Studi di Siena, Dipartimento di Ingegneria dell’Informatione June 2001). 2001, S. 1- 11. 4. Gore, R. ; Mendler, Michael ; De Paiva, V. (Hrsg.): Intuitionistic Modal Logic and Applicati- ons . (IMLA’02 Copenhagen, DK July 2002) 2002. - 100 Seiten. 5. Fairtlough, M. ; Mendler, Michael: On the logical content of computational type theory: A solution to Curry‘s problem . In: Callaghan, P. ; Luo, Z. ; McKinna, J. ; Pollack, R. (Hrsg.) : Types for Proofs and Programs. Berlin u.a. : Springer, 2002, (LNCS Bd. 2277), S. 63-78. 6. Fairtlough, M. ; Mendler, Michael: Intensional completeness in an extension of Goedel- Dummett logic . In: Studia Logica 73 (2003), S. 51-80 7. De Paiva, V. ; Gore, R. ; Mendler, Michael (Hrsg.): Modalities in Constructive Modal Logics and Type Theories . Oxford : Oxford University Press, 2004 (Special Issue of Journal of Lo- gic and Computation Bd. to appear) 8. Mendler, Michael: Constrained proofs: a logic for dealing with behavioural constraints in formal hardware verification . In: Jones, G. ; Sheeran, M. (Hrsg.) : Workshop on Designing Correct Circuits. Berlin u.a. : Springer, 1991, S. 1-28. 9. Mendler, Michael: A modal logic for handling behavioural constraints in formal hardware ve- rification . Edinburgh : Dept. of Computer Science, University of Edinburgh. 1993 (ECS- LFCS-93-255, March). - Forschungsbericht. 236 Seiten 10. Mendler, Michael: Dealing with Hardware Constraints - A modal logical approach . In: Kloos, C., D. (Hrsg.) : 1st Euroform Workshop (1st Euroform Workshop Las Navas del Marques, Spain January 1994). 1994, S. 7 Seiten. 11. Fairtlough, M. ; Mendler, Michael: An intuitionistic modal logic with applications to the for- mal verification of hardware . In: Pacholski, L. ; Tiuryn, J. (Hrsg.) : Proceedings of the 1994 Annual Conference of the European Association for Computer Science Logic. Berlin u. a. : Springer, 1995, S. 354-368. (LNCS Bd. 933) 12. Fairtlough, M. ; Mendler, Michael ; Walton, M.: First-order Lax Logic as a Framework for Constraint Logic Programming . Passau : Universität Passau. 1997 (MIP-9714). - For- schungsbericht. 51 Seiten Proofs-as-Delays: Verzögerungsanalyse in Intuitionistischer Logik Projektleitung: Prof. Michael Mendler, Ph.D.
Deutsche Forschungsge- meinschaft DFG (1996- 1998)
Die meisten heute verwendeten Verfahren zur formalen Spezifikati- on und Verifikation von komplexen verteilten Systemen basieren auf klassischen zweiwertigen Logiken (z.B. Aussagenlogik, Modallogik, Prädikatenlogik). Für klassische Logiken wird die zur Darstellung von dynamischem Verhalten nötige Ausdruckskraft in erster Linie durch Erweiterung der sprachlichen Ausdrucksmittel erreicht. Ein grundsätzlich anderer Ansatz besteht darin, nicht die Syntax der lo-
Forschungsbericht der Otto-Friedrich-Universität Bamberg Seite 917 gischen Sprache, sondern die Reichhaltigkeit ihrer Wahrheitswerte zu erhöhen. Eine der bedeutendsten mehrwertigen Logiken, die in- tuitionistische Logik, wurde wegen ihrer höheren beweis- und mo- delltheoretischen Komplexität in diesem Zusammenhang bisher kaum beachtet. In diesem Projekt wird eine intuitionistischen Modallogik, die soge- nannte Laxe Logik für die Verzögerungsanalyse kombinatorischer Systeme eingesetzt. Dies führt auf einen neuartigen Ansatz zur Ana- lyse datenabhängiger Verzögerungszeiten, der sich gegenüber den herkömmlichen algorithmenorientierten Verfahren in seiner seman- tischen Fundierung, seiner Exaktheit und seiner inhärenten Kompo- sitionalität auszeichnet. Eine Reihe bekannter Algorithmen zur Verzögerungsanalyse sind auf diese Weise erstmalig semantisch präzise charakterisierbar. Die methodische Trennung von tempora- len und funktionalen Aspekten in Laxer Logik erlaubt dabei eine nahtlose Integration von Verzögerungsanalysealgorithmen und pro- grammiersprachlichen Typprüfungsverfahren.
Yüklə 2,2 Mb. Dostları ilə paylaş:
|