Publikationen des Jahres 2004
Bücher und Konferenzbände
Jordi Cortadella and Wolfgang Reisig, editors. Applications and Theory of Petri Nets 2004, 25th International Conference, ICATPN 2004, Bologna, Italy, June 21-25, 2004, Proceedings, volume 3099 of Lecture Notes in Computer Science, 2004. Springer-Verlag.
@Proceedings{ CortadellaR2004_icatpn, title = {{Applications and Theory of Petri Nets 2004, 25th International Conference, ICATPN 2004, Bologna, Italy, June 21-25, 2004, Proceedings}}, year = 2004, editor = {Jordi Cortadella and Wolfgang Reisig}, volume = 3099, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, booktitle = {{ICATPN}}, url = {http://www.informatik.uni-trier.de/%7Eley/db/conf/apn/icatpn2004.html} }Jörg Desel, Wolfgang Reisig, and Grzegorz Rozenberg, editors. Lectures on Concurrency and Petri Nets, Advances in Petri Nets 2003, volume 3098 of Lecture Notes in Computer Science, 2004. Springer-Verlag. Note: This tutorial volume originates from the 4th Advanced Course on Petri Nets, ACPN 2003, held in Eichstätt, Germany in September 2003. In addition to lectures given at ACPN 2003, additional chapters have been commissioned.
@Proceedings{ DeselRR2004_acpn, title = {{Lectures on Concurrency and Petri Nets, Advances in Petri Nets 2003}}, year = 2004, editor = {Jörg Desel and Wolfgang Reisig and Grzegorz Rozenberg}, volume = 3098, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, note = {This tutorial volume originates from the 4th Advanced Course on Petri Nets, ACPN 2003, held in Eichst{\"a}tt, Germany in September 2003. In addition to lectures given at ACPN 2003, additional chapters have been commissioned.}, booktitle = {{Lectures on Concurrency and Petri Nets}}, url = {http://www.informatik.uni-trier.de/%7Eley/db/conf/ac/acpn2003.html} }
Publikationen in Zeitschriften und Büchern
Jose M. Vidal, Paul Buhler, and Christian Stahl. Multiagent Systems with Workflows. IEEE Internet Computing, 8(1):76-82, February 2004.
Abstract: Industry and researchers have two different visions for the future of Web services. Industry wants to capitalize on Web service technology to automate business processes via centralized workflow enactment. Researchers are interested in the dynamic composition of Web services. The authors show how these two visions are points in a continuum and discuss a possible path for bridging the gap between them. @Article{ VidalBS2004_iic81, author = {Jose M. Vidal and Paul Buhler and Christian Stahl}, title = {{Multiagent Systems with Workflows}}, journal = {IEEE Internet Computing}, year = 2004, volume = 8, number = 1, pages = {76-82}, month = feb, url = {http://dx.doi.org/10.1109/MIC.2004.1260707}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/VidalBS2004_iic81.pdf}, keywords = {Geschäftsprozesse, BPEL}, abstract = {Industry and researchers have two different visions for the future of Web services. Industry wants to capitalize on Web service technology to automate business processes via centralized workflow enactment. Researchers are interested in the dynamic composition of Web services. The authors show how these two visions are points in a continuum and discuss a possible path for bridging the gap between them.} }Farn Wang, Karsten Schmidt, Fang Yu, Geng-Dian Huang, and Bow-Yaw Wang. BDD-Based Safety-Analysis of Concurrent Software with Pointer Data Structures Using Graph Automorphism Symmetry Reduction. IEEE Transactions on Software Engineering (TSE), 30(6):403-417, June 2004.
Abstract: Dynamic data-structures with pointer links, which are heavily used in real-world software, cause extremely difficult verification problems. Currently, there is no practical framework for the efficient verification of such software systems. We investigated symmetry reduction techniques for the verification of software systems with C-like indirect reference chains like x->y->z->w. We formally defined the model of software with pointer data structures and developed symbolic algorithms to manipulate conditions and assignments with indirect reference chains using BDD technology. We relied on two techniques, inactive variable elimination and process-symmetry reduction in the data-structure configuration, to reduce time and memory complexity. We used binary permutation for efficiency, but we also identified the possibility of an anomaly of false image reachability. We implemented the techniques in tool Red 5.0 and compared performance with Murø and SMC against several benchmarks. @Article{ WangSYHW2004_tse306, author = {Farn Wang and Karsten Schmidt and Fang Yu and Geng-Dian Huang and Bow-Yaw Wang}, title = {{BDD-Based Safety-Analysis of Concurrent Software with Pointer Data Structures Using Graph Automorphism Symmetry Reduction}}, journal = {IEEE Transactions on Software Engineering (TSE)}, year = 2004, volume = 30, number = 6, pages = {403-417}, month = jun, ps = {http://cc.ee.ntu.edu.tw/~farn/publications/pointer.TSE04.ps}, url = {http://doi.ieeecomputersociety.org/10.1109/TSE.2004.15}, abstract = {Dynamic data-structures with pointer links, which are heavily used in real-world software, cause extremely difficult verification problems. Currently, there is no practical framework for the efficient verification of such software systems. We investigated symmetry reduction techniques for the verification of software systems with C-like indirect reference chains like x->y->z->w. We formally defined the model of software with pointer data structures and developed symbolic algorithms to manipulate conditions and assignments with indirect reference chains using BDD technology. We relied on two techniques, inactive variable elimination and process-symmetry reduction in the data-structure configuration, to reduce time and memory complexity. We used binary permutation for efficiency, but we also identified the possibility of an anomaly of false image reachability. We implemented the techniques in tool Red 5.0 and compared performance with Murø and SMC against several benchmarks.} }
Konferenzbeiträge und Beiträge auf Workshops
Adrianna Alexander. Composition of Temporal Logic Specifications. In Jordi Cortadella and Wolfgang Reisig, editors, Applications and Theory of Petri Nets 2004, 25th International Conference (ICATPN 2004), number 3099 of Lecture Notes in Computer Science, pages 98-116, 2004. Springer-Verlag.
Abstract: The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. TLDA supports a modular design of systems: Subsystems can be specified and verified separately and then be integrated into one system. The properties of the subsystems will be preserved in this process. TLDA can be syntactically viewed as an extension of TLA. We propose a different semantical model based on partial order which increases the expressiveness of the logic. @InProceedings{ Alexander2004_lncs3099, author = {Adrianna Alexander}, title = {{Composition of Temporal Logic Specifications}}, editor = {Jordi Cortadella and Wolfgang Reisig}, booktitle = {{Applications and Theory of Petri Nets 2004, 25th International Conference (ICATPN 2004)}}, year = 2004, series = {Lecture Notes in Computer Science}, pages = {98-116}, publisher = {Springer-Verlag}, number = 3099, url = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3099{\&}spage=98}, keywords = {TLDA, Temporale Logik}, abstract = {The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. TLDA supports a modular design of systems: Subsystems can be specified and verified separately and then be integrated into one system. The properties of the subsystems will be preserved in this process. TLDA can be syntactically viewed as an extension of TLA. We propose a different semantical model based on partial order which increases the expressiveness of the logic.} }Adrianna Alexander and Wolfgang Reisig. Compositional Temporal Logic Based on Partial Order. In 11th International Symposium on Temporal Representation and Reasoning (TIME'04), pages 125-132, 2004. IEEE Computer Society.
Abstract: The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. The logic supports a compositional design of systems: subsystems can be specified separately and then be integrated into one system. TLDA can be syntactically viewed as an extension of TLA. We propose a different semantical model based on partial order which increases the expressiveness of the logic. @InProceedings{ AlexanderR2004_time, author = {Adrianna Alexander and Wolfgang Reisig}, title = {{Compositional Temporal Logic Based on Partial Order}}, booktitle = {{11th International Symposium on Temporal Representation and Reasoning (TIME'04)}}, year = 2004, pages = {125-132}, publisher = {IEEE Computer Society}, url = {http://csdl.computer.org/comp/proceedings/time/2004/2155/00/21550125abs.htm}, keywords = {TLDA, Temporale Logik}, abstract = {The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. The logic supports a compositional design of systems: subsystems can be specified separately and then be integrated into one system. TLDA can be syntactically viewed as an extension of TLA. We propose a different semantical model based on partial order which increases the expressiveness of the logic.} }Axel Martens. Analysis and re-engineering of Web Services. In Proceedings of 6th International Conference on Enterprise Information Systems (ICEIS'04), 2004. Porto, Portugal.
Abstract: To an increasing extend software systems are integrated across the borders of individual enterprises. The Web Service approach provides group of technologies to describe components and their composition, based on well established protocols. Focused on business processes, one Web Service implements a local subprocess. A distributed business processes is implemented by the composition a set of communicating Web Services. At the moment, there are various modeling languages under development to describe the internal structure of one Web Service (e. g. Business Process Execution Language for Web Services BPEL4WS (BEA et al., 2002a)) and the choreography of a set of Web Services (e. g. Web Service Choreography Interface WSCI (BEA et al., 2002b)). Nevertheless, there is a need for methods for stepwise construction and verification of such components. This paper abstracts from concrete syntax of any proposed language definition. Instead, we apply Petri nets to model Web Services. Thus, we are able to reason about essential properties, e. g. usability of a Web Service - our notion of a quality criterion. Based on this framework, we present an algorithm to analyze a given Web Service and to transfer a complex process model into a appropriate model of a Web Service. @InProceedings{ Martens2004_iceis, author = {Axel Martens}, title = {{Analysis and re-engineering of Web Services}}, booktitle = {{Proceedings of 6th International Conference on Enterprise Information Systems (ICEIS'04)}}, year = 2004, publisher = {Porto, Portugal}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Martens2004_iceis.pdf}, keywords = {Geschäftsprozesse}, abstract = {To an increasing extend software systems are integrated across the borders of individual enterprises. The Web Service approach provides group of technologies to describe components and their composition, based on well established protocols. Focused on business processes, one Web Service implements a local subprocess. A distributed business processes is implemented by the composition a set of communicating Web Services. At the moment, there are various modeling languages under development to describe the internal structure of one Web Service (e. g. Business Process Execution Language for Web Services BPEL4WS (BEA et al., 2002a)) and the choreography of a set of Web Services (e. g. Web Service Choreography Interface WSCI (BEA et al., 2002b)). Nevertheless, there is a need for methods for stepwise construction and verification of such components. This paper abstracts from concrete syntax of any proposed language definition. Instead, we apply Petri nets to model Web Services. Thus, we are able to reason about essential properties, e. g. usability of a Web Service - our notion of a quality criterion. Based on this framework, we present an algorithm to analyze a given Web Service and to transfer a complex process model into a appropriate model of a Web Service.} }Karsten Schmidt. Automated Generation of a Progress Measure for the Sweep-Line Method. In Proc. 10th Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2988 of Lecture Notes in Computer Science, pages 192-204, 2004. Springer-Verlag.
Abstract: In the context of Petri nets, we propose an automated construction of a progress measure which is an important pre-requisite for a state space reduction technique called the sweep-line method. Our construction is based on linear-algebraic considerations concerning the transition vectors of the Petri net under consideration. @InProceedings{ Schmidt2004_lncs2988, author = {Karsten Schmidt}, title = {{Automated Generation of a Progress Measure for the Sweep-Line Method}}, booktitle = {{Proc. 10th Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}}, year = 2004, series = {Lecture Notes in Computer Science}, volume = 2988, pages = {192-204}, publisher = {Springer-Verlag}, url = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=2988&spage=192}, abstract = {In the context of Petri nets, we propose an automated construction of a progress measure which is an important pre-requisite for a state space reduction technique called the sweep-line method. Our construction is based on linear-algebraic considerations concerning the transition vectors of the Petri net under consideration.} }Karsten Schmidt. Distributed Usability of Web Services. In Proceedings of the 11th Workshop on Algorithms and Tools for Petri Nets (AWPN 04), pages 19-24, 2004. Bericht tr-ri-04-251, Universität Paderborn.
Abstract: We estabilish a theory of distributed usability. To do so, it is however neccessary to modify the already existing theory of central usability. @InProceedings{ Schmidt2004_awpn, author = {Karsten Schmidt}, title = {{Distributed Usability of Web Services}}, booktitle = {{Proceedings of the 11th Workshop on Algorithms and Tools for Petri Nets (AWPN 04)}}, year = 2004, pages = {19-24}, publisher = {Bericht tr-ri-04-251, Universität Paderborn}, pdf = {http://wwwcs.upb.de/cs/kindler/events/AWPN04/material/proceedings.pdf}, keywords = {Geschäftsprozesse}, abstract = {We estabilish a theory of distributed usability. To do so, it is however neccessary to modify the already existing theory of central usability.} }Karsten Schmidt and Christian Stahl. A Petri net semantic for BPEL4WS - validation and application. In Ekkart Kindler, editor, Proceedings of the 11th Workshop on Algorithms and Tools for Petri Nets (AWPN'04), pages 1-6, October 2004. Universität Paderborn.
Abstract: We translated a small business process into a recently defined Petri net semantic. Then we used the tool LoLA for validating the semantic as well as for proving relevant properties of the particular process. @InProceedings{ SchmidtS2004_awpn, author = {Karsten Schmidt and Christian Stahl}, title = {{A Petri net semantic for BPEL4WS - validation and application}}, editor = {Ekkart Kindler}, booktitle = {{Proceedings of the 11th Workshop on Algorithms and Tools for Petri Nets (AWPN'04)}}, year = 2004, pages = {1-6}, month = oct, publisher = {Universität Paderborn}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/SchmidtS2004_awpn.pdf}, keywords = {BPEL, Geschäftsprozesse, BPEL-Semantik}, abstract = {We translated a small business process into a recently defined Petri net semantic. Then we used the tool LoLA for validating the semantic as well as for proving relevant properties of the particular process.} }
Technische Berichte
Adrianna Alexander and Wolfgang Reisig. Compositional Temporal Logic Based on Partial Order. Informatik-Berichte 185, Humboldt-Universität zu Berlin, December 2004.
@TechReport{ ReisigB2004_hub_tr185, author = {Adrianna Alexander and Wolfgang Reisig}, title = {{Compositional Temporal Logic Based on Partial Order}}, institution = {Humboldt-Universität zu Berlin}, year = 2004, type = {Informatik-Berichte}, number = 185, month = dec }Axel Martens, Christian Stahl, Daniela Weinberg, Dirk Fahland, and Thomas Heidinger. Business Process Execution Language for Web services - Semantik, Analyse und Visualisierung. Informatik-Berichte 169, Humboldt-Universität zu Berlin, July 2004.
Abstract: Moderne Systeme der Informationstechnik bestehen zumeist aus einer Vielzahl von Komponenten, die in einem Netzwerk auf verteilten Knoten ausgeführt werden. Mit dem Web-Service-Ansatz können solche Systeme einfacher und flexibler entwickelt werden. Diese Arbeit befasst sich mit der Modellierung, Visualisierung und Analyse von Web Services. Ein Web Service kapselt eine Anwendung und stellt diese über ein wohldefiniertes Interface der Außenwelt zur Verfügung. Im Gegensatz zu früheren Ansätzen dienen eine Reihe zusammenhängender Technologien zur Beschreibung eines Web Service. Diese Arbeit beschäftigt sich vor allem mit der internen Struktur eines Web Service, beschrieben mit Hilfe der Business Process Execution Language for Web Services (BPEL4WS) [ACD+02]. Der Web-Service-Ansatz bietet ein homogenes Konzept von Komponenten und ihrer Komposition ber einem heterogenen Netzwerk. Damit ist die syntaktische Grundlage für die Entwicklung verteilter Systeme gelegt. Wesentlich für den Erfolg der Web Services ist jedoch die Beantwortung der semantischen Fragestellungen: Passen zwei gegebene Web Services inhaltlich zusammen? Kann in einem verteilten System ein gegebener Web Service durch einen anderen ersetzt werden? Entspricht ein konkreter Web Service einer gegebenen abstrakten Spezifikation? Diese Arbeit befasst sich mit der Beantwortung dieser und weiterer Fragestellungen im Web-Service-Ansatz: In einem ersten Schritt entwickeln wir eine formale Semantik für die Sprache BPEL4WS. Darauf aufbauend werden Methoden zur Analyse verteilter Systeme auf die konkreten Anforderungen bertragen und neue Verfahren entwickelt. Für die Diskussion der Modelle und Eigenschaften entwickeln wir eine intuitive graphische Repräsentation der Sprache BPEL4WS. Das Ziel der Forschungen ist die Umsetzung der Methoden in einem integrierten Entwicklungswerkzeug für BPEL4WS. Die vorliegende Arbeit beschreibt die ersten Ergebnisse in einem laufenden Projekt. @TechReport{ MartensSWFH2004_hub_tr169, author = {Axel Martens and Christian Stahl and Daniela Weinberg and Dirk Fahland and Thomas Heidinger}, title = {{Business Process Execution Language for Web services - Semantik, Analyse und Visualisierung}}, institution = {Humboldt-Universität zu Berlin}, year = 2004, type = {Informatik-Berichte}, number = 169, month = jul, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/MartensSWFH2004_hub_tr169.pdf}, keywords = {BPEL, Geschäftsprozesse, BPEL-Semantik, Bedienbarkeit}, abstract = {Moderne Systeme der Informationstechnik bestehen zumeist aus einer Vielzahl von Komponenten, die in einem Netzwerk auf verteilten Knoten ausgeführt werden. Mit dem Web-Service-Ansatz können solche Systeme einfacher und flexibler entwickelt werden. Diese Arbeit befasst sich mit der Modellierung, Visualisierung und Analyse von Web Services. Ein Web Service kapselt eine Anwendung und stellt diese über ein wohldefiniertes Interface der Außenwelt zur Verfügung. Im Gegensatz zu früheren Ansätzen dienen eine Reihe zusammenhängender Technologien zur Beschreibung eines Web Service. Diese Arbeit beschäftigt sich vor allem mit der internen Struktur eines Web Service, beschrieben mit Hilfe der Business Process Execution Language for Web Services (BPEL4WS) [ACD+02]. Der Web-Service-Ansatz bietet ein homogenes Konzept von Komponenten und ihrer Komposition ber einem heterogenen Netzwerk. Damit ist die syntaktische Grundlage für die Entwicklung verteilter Systeme gelegt. Wesentlich für den Erfolg der Web Services ist jedoch die Beantwortung der semantischen Fragestellungen: Passen zwei gegebene Web Services inhaltlich zusammen? Kann in einem verteilten System ein gegebener Web Service durch einen anderen ersetzt werden? Entspricht ein konkreter Web Service einer gegebenen abstrakten Spezifikation? Diese Arbeit befasst sich mit der Beantwortung dieser und weiterer Fragestellungen im Web-Service-Ansatz: In einem ersten Schritt entwickeln wir eine formale Semantik für die Sprache BPEL4WS. Darauf aufbauend werden Methoden zur Analyse verteilter Systeme auf die konkreten Anforderungen bertragen und neue Verfahren entwickelt. Für die Diskussion der Modelle und Eigenschaften entwickeln wir eine intuitive graphische Repräsentation der Sprache BPEL4WS. Das Ziel der Forschungen ist die Umsetzung der Methoden in einem integrierten Entwicklungswerkzeug für BPEL4WS. Die vorliegende Arbeit beschreibt die ersten Ergebnisse in einem laufenden Projekt.} }Wolfgang Reisig. The computable kernel of Sequential Abstract State Machines. Informatik-Berichte 177, Humboldt-Universität zu Berlin, 2004. Note: To appear:.
@TechReport{ Reisig2004_hub_tr177, author = {Wolfgang Reisig}, title = {{The computable kernel of Sequential Abstract State Machines}}, institution = {Humboldt-Universität zu Berlin}, year = 2004, type = {Informatik-Berichte}, number = 177, note = {to appear:}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Reisig2004_hub_tr177.pdf}, ps = {http://www.informatik.hu-berlin.de/top/download/publications/Reisig2004_hub_tr177.ps} }Wolfgang Reisig and A. Brade. ASM Models for Web Services. Informatik-Berichte 181, Humboldt-Universität zu Berlin, 2004.
@TechReport{ ReisigB2004_hub_tr181, author = {Wolfgang Reisig and A. Brade}, title = {{ASM Models for Web Services}}, institution = {Humboldt-Universität zu Berlin}, year = 2004, type = {Informatik-Berichte}, number = 181 }
Studien- und Diplomarbeiten
Dirk Fahland. Ein Ansatz einer formalen Semantik der Business Process Execution Language for Web Services mit Abstract State Machines. Studienarbeit, Humboldt-Universität zu Berlin, August 2004.
Abstract: In dieser Arbeit stellen wir einen Ansatz zur Definition einer formalen Semantik für die Business Process Execution Language for Web Services (kurz BPEL4WS) von IBM, Microsoft und deren Industriepartnern vor. Zur Formalisierung wählen wir den Abstract-State-Machine-Formalismus (kurz ASM), dessen theoretische Fundierung es uns erlaubt, die Semantik von BPEL4WS auf der selben Abstraktionsebene zur formalisieren, die in der informalen BPEL4WS-Spezifikation vorgegeben ist. Wir werden den inneren Aufbau der Sprache präzise, formal abbilden und damit eine intuitiv und anschaulich nachvollziehbare Entsprechung zwischen den Abläufen eines BPEL4WSProzesses gemäß der gegebenen informalen Semantik und unserer formalen Semantik aufzeigen. Dazu analysieren wir die Struktur von BPEL4WS und zeigen mit welchen Mitteln des ASM-Formalismus diese adäquat, formal erfasst werden und wie in ASM notierte Spezifikationen zu lesen sind. Hierzu werden wir beispielhaft ausgewählte, syntaktische Konstrukte von BPEL4WS nach unserem Ansatz formalisieren. Die vorliegende Arbeit bezieht sich auf die informale BPEL4WS-Spezifikation v1.1, veröffentlicht am 5. Mai 2003. @MastersThesis{ Fahland2004_sa, author = {Dirk Fahland}, title = {{Ein Ansatz einer formalen Semantik der Business Process Execution Language for Web Services mit Abstract State Machines}}, school = {Humboldt-Universität zu Berlin}, year = 2004, type = {Studienarbeit}, month = aug, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Fahland2004_sa.pdf}, keywords = {BPEL, ASM, Geschäftsprozesse, BPEL-Semantik}, abstract = {In dieser Arbeit stellen wir einen Ansatz zur Definition einer formalen Semantik für die Business Process Execution Language for Web Services (kurz BPEL4WS) von IBM, Microsoft und deren Industriepartnern vor. Zur Formalisierung wählen wir den Abstract-State-Machine-Formalismus (kurz ASM), dessen theoretische Fundierung es uns erlaubt, die Semantik von BPEL4WS auf der selben Abstraktionsebene zur formalisieren, die in der informalen BPEL4WS-Spezifikation vorgegeben ist. Wir werden den inneren Aufbau der Sprache präzise, formal abbilden und damit eine intuitiv und anschaulich nachvollziehbare Entsprechung zwischen den Abläufen eines BPEL4WSProzesses gemäß der gegebenen informalen Semantik und unserer formalen Semantik aufzeigen. Dazu analysieren wir die Struktur von BPEL4WS und zeigen mit welchen Mitteln des ASM-Formalismus diese adäquat, formal erfasst werden und wie in ASM notierte Spezifikationen zu lesen sind. Hierzu werden wir beispielhaft ausgewählte, syntaktische Konstrukte von BPEL4WS nach unserem Ansatz formalisieren. Die vorliegende Arbeit bezieht sich auf die informale BPEL4WS-Spezifikation v1.1, veröffentlicht am 5. Mai 2003.} }Carsten Frenkler. BPEL-Boxen. Ein Modell zur Integration von Transaktionskonzepten in Geschäftsprozesse mit Petrinetzen. Studienarbeit, Humboldt-Universität zu Berlin, February 2004.
@MastersThesis{ Frenkler2004_sa, author = {Carsten Frenkler}, title = {{BPEL-Boxen. Ein Modell zur Integration von Transaktionskonzepten in Geschäftsprozesse mit Petrinetzen}}, school = {Humboldt-Universität zu Berlin}, year = 2004, type = {Studienarbeit}, month = feb, ps = {http://www.informatik.hu-berlin.de/top/download/publications/Frenkler2004_sa.ps}, keywords = {BPEL, Geschäftsprozesse} }Yvonne Gabriel. Anbindung externer Werkzeuge an den Petrinetz-Kern am Beispiel des Integrated Net Analyser. Studienarbeit, Humboldt-Universität zu Berlin, April 2004.
@MastersThesis{ Gabriel2004_sa, author = {Yvonne Gabriel}, title = {{Anbindung externer Werkzeuge an den Petrinetz-Kern am Beispiel des Integrated Net Analyser}}, school = {Humboldt-Universität zu Berlin}, year = 2004, type = {Studienarbeit}, month = apr, keywords = {Petri Net Kernel} }Lars Kuhtz. TLDA und Petrinetze. Studienarbeit, Humboldt-Universität zu Berlin, April 2004.
@MastersThesis{ Kuhtz2004_sa, author = {Lars Kuhtz}, title = {{TLDA und Petrinetze}}, school = {Humboldt-Universität zu Berlin}, year = 2004, type = {Studienarbeit}, month = apr, ps = {http://www.informatik.hu-berlin.de/top/download/publications/Kuhtz2004_sa.ps}, keywords = {TLDA, Temporale Logik} }Peter Massuthe. Verfeinerungstechniken der Temporal Logic of Distributed Actions TLDA. Diplomarbeit, Humboldt-Universität zu Berlin, March 2004.
Abstract: TLDA, die Temporal Logic of Distributed Actions, ist eine neue temporale Logik zur Spezifikation verteilter Systeme. Sie basiert auf halbgeordneten Abläufen. Diese Logik hat noch keinen formalen Verfeinerungsbegriff. Die Entwicklung von Methoden zur Unterstützung der Entwicklung komplexer TLDA-Spezifikationen durch schrittweise Verfeinerung ist Inhalt der vorliegenden Arbeit. Wir unterscheiden dabei zwischen Datenverfeinerung und Transitionsverfeinerung. Die Anwendbarkeit dieser Methoden wird anhand mehrerer mittelgroßer Fallstudien gezeigt. Weiterhin beschäftigen wir uns mit der Bewahrung von Eigenschaften durch Daten- und Transitionsverfeinerungsschritte. Diese Arbeit richtet sich vor allem an die Modellierer verteilter Systeme mit formalen Spezifikationsmethoden, insbesondere temporalen Logiken. @MastersThesis{ Massuthe2004_da, author = {Peter Massuthe}, title = {{Verfeinerungstechniken der Temporal Logic of Distributed Actions TLDA}}, school = {Humboldt-Universität zu Berlin}, year = 2004, type = {Diplomarbeit}, month = mar, ps = {http://www.informatik.hu-berlin.de/top/download/publications/Massuthe2004_da.ps}, keywords = {TLDA, Temporale Logik}, abstract = {TLDA, die Temporal Logic of Distributed Actions, ist eine neue temporale Logik zur Spezifikation verteilter Systeme. Sie basiert auf halbgeordneten Abläufen. Diese Logik hat noch keinen formalen Verfeinerungsbegriff. Die Entwicklung von Methoden zur Unterstützung der Entwicklung komplexer TLDA-Spezifikationen durch schrittweise Verfeinerung ist Inhalt der vorliegenden Arbeit. Wir unterscheiden dabei zwischen Datenverfeinerung und Transitionsverfeinerung. Die Anwendbarkeit dieser Methoden wird anhand mehrerer mittelgroßer Fallstudien gezeigt. Weiterhin beschäftigen wir uns mit der Bewahrung von Eigenschaften durch Daten- und Transitionsverfeinerungsschritte. Diese Arbeit richtet sich vor allem an die Modellierer verteilter Systeme mit formalen Spezifikationsmethoden, insbesondere temporalen Logiken.} }Christian Stahl. Transformation von BPEL4WS in Petrinetze. Diplomarbeit, Humboldt-Universität zu Berlin, April 2004.
Abstract: BPEL4WS ist eine Sprache zur Beschreibung verteilter Geschäftsprozesse mit Web Services. Es besteht die Notwendigkeit, die Sprache trotz ihrer Komplexität zu verstehen, um mit ihr im Umfeld von Web Services arbeiten zu können. Mit Hilfe einer formalen Semantik ist es möglich, die Sprache selbst und mit BPEL4WS spezifizierte Geschäftsprozesse zu verifizieren. In der vorliegenden Arbeit wird eine Petrinetz-Semantik für BPEL4WS vorgestellt. Dazu wird gezeigt, dass jedes Konstrukt der Sprache BPEL4WS in ein Petrinetz-Muster übersetzt werden kann. Damit ist es möglich, jeden in der Geschäftsprozesssprache BPEL4WS modellierten Geschäftsprozess in ein Petrinetz zu transformieren. Bei der Entwicklung der Semantik kann auf Forschungsergebnisse aus dem Bereich "Petrinetze als Werkzeug zur Geschäftsprozessmodellierung" zurückgegriffen werden. @MastersThesis{ Stahl2004_da, author = {Christian Stahl}, title = {{Transformation von BPEL4WS in Petrinetze}}, school = {Humboldt-Universität zu Berlin}, year = 2004, type = {Diplomarbeit}, month = apr, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Stahl2004_da.pdf}, keywords = {BPEL, Geschäftsprozesse, BPEL-Semantik}, abstract = {BPEL4WS ist eine Sprache zur Beschreibung verteilter Geschäftsprozesse mit Web Services. Es besteht die Notwendigkeit, die Sprache trotz ihrer Komplexität zu verstehen, um mit ihr im Umfeld von Web Services arbeiten zu können. Mit Hilfe einer formalen Semantik ist es möglich, die Sprache selbst und mit BPEL4WS spezifizierte Geschäftsprozesse zu verifizieren. In der vorliegenden Arbeit wird eine Petrinetz-Semantik für BPEL4WS vorgestellt. Dazu wird gezeigt, dass jedes Konstrukt der Sprache BPEL4WS in ein Petrinetz-Muster übersetzt werden kann. Damit ist es möglich, jeden in der Geschäftsprozesssprache BPEL4WS modellierten Geschäftsprozess in ein Petrinetz zu transformieren. Bei der Entwicklung der Semantik kann auf Forschungsergebnisse aus dem Bereich "Petrinetze als Werkzeug zur Geschäftsprozessmodellierung" zurückgegriffen werden.} }Daniela Weinberg. Analyse der Bedienbarkeit. Diplomarbeit, Humboldt-Universität zu Berlin, October 2004.
Abstract: Das heutige Internet wächst zunehmend von einer Plattform als Informationsquelle hin zu einer Basis für die Abwicklung von Geschäftsprozessen. Zahlreiche Firmen stellen ihre Dienste bereits mit Hilfe von Web-Services zur Verfügung oder integrieren andere bereitgestellte Web-Services in ihren Geschäftsablauf. Nach Studien einiger Forschungsinstitute geht der Trend in der heutigen IT-Branche stark zum Einsatz solcher verteilter Geschäftsprozesse. Es werden Schlagworte wie out-tasking, plug-and-play und Lego-Wirtschaft geprägt. Bevor ein Geschäftsprozess in Form eines Web-Services jedoch veröffentlicht wird, sollte dieser geeignet untersucht werden. Wir werden uns in dieser Arbeit diesem Thema mit Hilfe von Petri-Netz-Modulen nähern. Sie modellieren gerade die interne Struktur von Geschäftsprozessen und ermöglichen es, den Prozess geeignet zu analysieren. Uns interessiert bei der Analyse, ob die Funktionalität, die ein Web-Service bereitstellen soll, auch wirklich genutzt werden kann. Wir sprechen in diesem Zusammenhang von Bedienbarkeit. Für die Analyse definieren wir den Interaktionsgraphen eines Workflow-Moduls, welcher die Zustände des Moduls und dessen Interaktion mit einer Umgebung veranschaulicht. Auf dieser Grundlage können wir dann eine Bedienstrategie definieren, durch die das Modul bedient werden kann. Das hei¼t, wenn eine Umgebung das Modul so bedienen kann, dass dieses ordentlich terminiert, finden wir eine Bedienstrategie in dem Interaktionsgraphen des Moduls. Darüber hinaus bieten die Graphen dem Modellierer die Möglichkeit, einen Blick auf die Abläufe seines Moduls zu werfen und genau erkennen zu können, welche Zustände des Moduls bei welcher Interaktion mit der Umgebung eingenommen werden. Auf Grundlage dieser Analyse kann der Modellierer seinen Prozess überarbeiten, anpassen etc. Um die Bedienbarkeit der Workflow-Module durch den Interaktionsgraphen zu verifizieren, reicht es aus, einen reduzierten Graphen zu konstruieren. Wir werden Reduktionsregeln definieren, die den Nachweis der Bedienbarkeit in den reduzierten Graphen erhalten. Die in dieser Arbeit entwickelten Algorithmen sind implementiert und in Wombat4ws, einem Analysewerkzeug für Web-Services, integriert worden. @MastersThesis{ Weinberg2004_da, author = {Daniela Weinberg}, title = {{Analyse der Bedienbarkeit}}, school = {Humboldt-Universität zu Berlin}, year = 2004, type = {Diplomarbeit}, month = oct, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Weinberg2004_da.pdf}, keywords = {Geschäftsprozesse}, abstract = {Das heutige Internet wächst zunehmend von einer Plattform als Informationsquelle hin zu einer Basis für die Abwicklung von Geschäftsprozessen. Zahlreiche Firmen stellen ihre Dienste bereits mit Hilfe von Web-Services zur Verfügung oder integrieren andere bereitgestellte Web-Services in ihren Geschäftsablauf. Nach Studien einiger Forschungsinstitute geht der Trend in der heutigen IT-Branche stark zum Einsatz solcher verteilter Geschäftsprozesse. Es werden Schlagworte wie out-tasking, plug-and-play und Lego-Wirtschaft geprägt. Bevor ein Geschäftsprozess in Form eines Web-Services jedoch veröffentlicht wird, sollte dieser geeignet untersucht werden. Wir werden uns in dieser Arbeit diesem Thema mit Hilfe von Petri-Netz-Modulen nähern. Sie modellieren gerade die interne Struktur von Geschäftsprozessen und ermöglichen es, den Prozess geeignet zu analysieren. Uns interessiert bei der Analyse, ob die Funktionalität, die ein Web-Service bereitstellen soll, auch wirklich genutzt werden kann. Wir sprechen in diesem Zusammenhang von Bedienbarkeit. Für die Analyse definieren wir den Interaktionsgraphen eines Workflow-Moduls, welcher die Zustände des Moduls und dessen Interaktion mit einer Umgebung veranschaulicht. Auf dieser Grundlage können wir dann eine Bedienstrategie definieren, durch die das Modul bedient werden kann. Das hei¼t, wenn eine Umgebung das Modul so bedienen kann, dass dieses ordentlich terminiert, finden wir eine Bedienstrategie in dem Interaktionsgraphen des Moduls. Darüber hinaus bieten die Graphen dem Modellierer die Möglichkeit, einen Blick auf die Abläufe seines Moduls zu werfen und genau erkennen zu können, welche Zustände des Moduls bei welcher Interaktion mit der Umgebung eingenommen werden. Auf Grundlage dieser Analyse kann der Modellierer seinen Prozess überarbeiten, anpassen etc. Um die Bedienbarkeit der Workflow-Module durch den Interaktionsgraphen zu verifizieren, reicht es aus, einen reduzierten Graphen zu konstruieren. Wir werden Reduktionsregeln definieren, die den Nachweis der Bedienbarkeit in den reduzierten Graphen erhalten. Die in dieser Arbeit entwickelten Algorithmen sind implementiert und in Wombat4ws, einem Analysewerkzeug für Web-Services, integriert worden.} }Stephan Weißleder. Semantische Fundierung der Web-Service-Beschreibungssprache WSCI. Diplomarbeit, Humboldt-Universität zu Berlin, November 2004.
Abstract: Wir beschäftigen uns in dieser Arbeit mit verschiedenen Beschreibungsmöglichkeiten für Web Services. Im Vordergrund stehen dabei die Web-Service-Beschreibungssprache WSCI und ihre Eigenschaften. Wir werden eine Semantik entwickeln, die Stärken und Schwächen der zugrunde liegenden Spezifikation [AAF+02] aufzeigt und mit deren Hilfe wir die Eigenschaften von WSCI überprüfen können. @MastersThesis{ Weissleder2004_da, author = {Stephan Weißleder}, title = {{Semantische Fundierung der Web-Service-Beschreibungssprache WSCI}}, school = {Humboldt-Universität zu Berlin}, year = 2004, type = {Diplomarbeit}, month = nov, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Weissleder2004_da.pdf}, keywords = {Geschäftsprozesse}, abstract = {Wir beschäftigen uns in dieser Arbeit mit verschiedenen Beschreibungsmöglichkeiten für Web Services. Im Vordergrund stehen dabei die Web-Service-Beschreibungssprache WSCI und ihre Eigenschaften. Wir werden eine Semantik entwickeln, die Stärken und Schwächen der zugrunde liegenden Spezifikation [AAF+02] aufzeigt und mit deren Hilfe wir die Eigenschaften von WSCI überprüfen können.} }
Theorie der Programmierung | | XHTML 1.0 | Wed Nov 5 08:30:01 2008

