union jack
Publikationen
HU-Logo
Institut für Informatik

Publikationen des Jahres 2005

Dissertationen und Habilitationen

  • Adrianna Alexander. Komposition Temporallogischer Spezifikationen - Spezifikation und Verifikation von Systemen mit Temporal Logic of Distributed Actions. Dissertation, Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II, September 2005. icon 

    @PhDThesis{ Alexander2005_diss,
author = {Adrianna Alexander},
title = {{Komposition Temporallogischer Spezifikationen - Spezifikation und Verifikation von Systemen mit Temporal Logic of Distributed Actions}},
school = {Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II},
year = 2005,
type = {Dissertation},
month = sep,
ps = {http://www.informatik.hu-berlin.de/top/download/publications/Alexander2005_diss.ps},
keywords = {TLDA, Temporale Logik},
abstract = {This thesis introduces a new temporal logic, called Temporal Logic ofDistributed Actions, TLDA for short. TLDA is designed for compositional specification and verification of distributed systems. TLDA originates syntactically from an already established temporal logic, TLA. But TLDA, contrary to TLA and other known compositional temporal logics, is based semantically on a partial order structure, called distributed run. Compared to TLA, the use of this semantical model increases the expressiveness of TLDA. Both the system and its properties are described in one formalism: They are represented by a set of distributed runs and specified in TLDA by a temporal logic formula. Hence, the verification of a system is reduced to proving that the system specification implies the property specification. We provide a set of proof rules for this. We show that the composition of systems is specified by conjunction of the specifications of its components and, usually, the specification of the interaction between the components. Hence, the specification of a composed system can be derived from specifications of its components. Component properties are preserved in the process of composition. Thus, components can be verified separately and then be integrated into the composed system. This economises the effort for verification. Attuned for distributed runs we develop a semantical criterion for TLDA-formulas, called environmental invariance. We show that environmental invariant formulas are suited for the specification of system components. We prove that such environmental invariant formulas, due to their properties, supply a modular design of systems. } 
}

Publikationen in Zeitschriften und Büchern

  • Peter Massuthe, Wolfgang Reisig, and Karsten Schmidt. An Operating Guideline Approach to the SOA. Annals of Mathematics, Computing & Teleinformatics, 1(3): 35-43, 2005. icon 

    @Article{ MassutheRS2005_amct,
author = {Peter Massuthe and Wolfgang Reisig and Karsten Schmidt},
title = {{An Operating Guideline Approach to the SOA}},
journal = {Annals of Mathematics, Computing \& Teleinformatics},
year = 2005,
volume = 1,
number = 3,
pages = {35-43},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/MassutheRS2005_amct.pdf},
keywords = {Services, Operating guidelines, oWFNs},
abstract = {Interorganizational cooperation is more andmore organized by the paradigm of services. The serviceoriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the three operations publish, find, and bind. We provide a formal method based on Petri nets to model services and their cooperation. We characterize well-behaving pairs of requester's and provider's services and suggest operating guidelines as a convenient and intuitive artifact to realize publish. In our approach, the find operation reduces to a matching problem between the requester's service and the operating guideline. Binding of a requester's and a provider's service is therefore guaranteed to result in a well-behaving cooperating service. At this time, the approach is limited to acyclic Petri nets.} 
}

  • Wolfgang Reisig, Karsten Schmidt, and Christian Stahl. Kommunizierende Workflow-Services modellieren und analysieren. Informatik - Forschung und Entwicklung, pp 90-101, October 2005. icon icon 

    @Article{ ReisigSS2005_ife,
author = {Wolfgang Reisig and Karsten Schmidt and Christian Stahl},
title = {{Kommunizierende Workflow-Services modellieren und analysieren}},
journal = {Informatik - Forschung und Entwicklung},
year = 2005,
pages = {90-101},
month = oct,
publisher = {Springer-Verlag},
issn = {0178-3564},
url = {http://dx.doi.org/10.1007/s00450-005-0209-5},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/ReisigSS2005_ife.pdf},
keywords = {Petrinetze, oWFNs, BPEL, Bedienbarkeit},
abstract = {Zur adäquaten Nutzung von Workflow-Implementierungen kommunizierender Geschäftsprozesse werden Konzepte vorgeschlagen,die von konkreten Implementierungen abstrahieren. Auf der Basis von Petrinetzen werden unterschiedliche Varianten der Bedienbarkeit von Workflows charakterisiert und dafür Entscheidungsalgorithmen vorgestellt. Die Angemessenheit des Ansatzes wird am Beispiel der Semantik von Komponenten der Geschäftsprozess-Modellierungssprache BPEL demonstriert.} 
}

  • Bernd-Holger Schlingloff, Axel Martens, and Karsten Schmidt. Modeling and Model Checking Web Services. Electronic Notes in Theoretical Computer Science: Issue on Logic and Communication in Multi-Agent Systems, 126: 3-26, March 2005. icon 

    @Article{ SchlingloffMS2005_entcs126,
author = {Bernd-Holger Schlingloff and Axel Martens and Karsten Schmidt},
title = {{Modeling and Model Checking Web Services}},
journal = {Electronic Notes in Theoretical Computer Science: Issue on Logic and Communication in Multi-Agent Systems},
year = 2005,
volume = 126,
pages = {3-26},
month = mar,
publisher = {Elsevier},
pdf = {http://www.sciencedirect.com/science?_ob=MImg&_imagekey=B75H1-4FKXPY9-F-1&_cdi=13109&_user=10&_orig=browse&_coverDate=03/08/2005&_sk=998739999&view=c&wchp=dGLzVzz-zSkWW&md5=da83be1d134c9d04ded5ee2029ac50bf&ie=/sdarticle.pdf},
keywords = {Geschäftsprozesse},
abstract = {We give an overview on web services and the web service technology stack. We then show how to build Petri net models of web services formulated in the specification language BPEL4WS. We define an abstract correctness criterion for these models and study the automated verification according to this criterion. Finally, we relate correctness of web service models to the model checking problem for alternating temporal logics.} 
}

Konferenzbeiträge und Beiträge auf Workshops

  • Dirk Fahland and Wolfgang Reisig. ASM-based semantics for BPEL: The negative Control Flow. In Danièle Beauquier, Egon Börger, and Anatol Slissenko, editors, Proceedings of the 12th International Workshop on Abstract State Machines (ASM'05), pages 131-151, March 2005. Paris XII. icon 

    @InProceedings{ FahlandR2005_asm,
author = {Dirk Fahland and Wolfgang Reisig},
title = {{ASM-based semantics for BPEL: The negative Control Flow}},
editor = {Danièle Beauquier and Egon Börger and Anatol Slissenko},
booktitle = {{Proceedings of the 12th International Workshop on Abstract State Machines (ASM'05)}},
year = 2005,
pages = {131-151},
month = mar,
publisher = {Paris XII},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/FahlandR2005_asm.pdf},
keywords = {ASM, BPEL, Geschäftsprozesse, BPEL-Semantik},
abstract = {BPEL is presently the most prominent language to specify and execute business processes, using Web Services as its technological basis. Particular problems arise when activities are faulty: faults have to be propagated, other activities have to be irregularly terminated, etc. We describe the formal semantics of fault handlers and event handlers, demonstrating that ASMs are most adequate for this purpose.} 
}

  • Carsten Frenkler and Karsten Schmidt. Modellierung und Analyse transaktionaler Geschäftsprozesse. In Karsten Schmidt and Christian Stahl, editors, 12. Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN 2005), Proceedings, pages 72-77, September 2005. Humboldt-Universität zu Berlin. 

    @InProceedings{ Frenklers2005_awpn,
author = {Carsten Frenkler and Karsten Schmidt},
title = {{Modellierung und Analyse transaktionaler Geschäftsprozesse}},
editor = {Karsten Schmidt and Christian Stahl},
booktitle = {{12. Workshop "Algorithmen und Werkzeuge für Petrinetze" (AWPN 2005), Proceedings}},
year = 2005,
pages = {72-77},
month = sep,
publisher = {Humboldt-Universität zu Berlin},
keywords = {Geschäftsprozesse, Bedienbarkeit},
abstract = {Wie erweitern in dieser Arbeit Workflow-Module um ein Konzept, mit dem derEinfluß eines Datenbanksystems auf die Bedienbarkeit eines Geschäftsprozesses untersucht werden kann. Wir integrieren transaktionale Eigenschaften als internes Verhalten in Workflow-Module und können damit Bedienbarkeit und Einhaltung transaktionaler Eigenschaften durch Analyse entscheiden.} 
}

  • Andreas Glausch. Eine Charakterisierung einfacher Petrinetz-Schemata. In Karsten Schmidt and Christian Stahl, editors, 12. Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN 2005), Proceedings, pages 1-6, September 2005. Humboldt-Universität zu Berlin. 

    @InProceedings{ Glausch2005_awpn,
author = {Andreas Glausch},
title = {{Eine Charakterisierung einfacher Petrinetz-Schemata}},
editor = {Karsten Schmidt and Christian Stahl},
booktitle = {{12. Workshop "Algorithmen und Werkzeuge für Petrinetze" (AWPN 2005), Proceedings}},
year = 2005,
pages = {1-6},
month = sep,
publisher = {Humboldt-Universität zu Berlin},
keywords = {Petrinetze},
abstract = {Wir untersuchen die Ausdrucksmächtigkeit von Petrinetz-Schemata. Dazuführen wir die Teilklasse der einfachen Petrinetz-Schemata ein und zeigen, welche Systeme sich durch ein einfaches Petrinetz-Schema darstellen lassen und welche nicht. Die hinreichenden und notwendigen Eigenschaften dazu formulieren wir in einem Theorem.} 
}

  • Eckhard Grass, Frank Winkler, Milos Krstic, Alexandra Julius, Christian Stahl, and Maxim Piz. Enhanced GALS Techniques for Datapath Applications. In Vassilis Paliouras, Johan Vounckx, and Diederik Verkest, editors, Integrated Circuit and System Design: 15th International Workshop, PATMOS 2005, Leuven, Belgium, September 20-23, 2005, volume 3728 of Lecture Notes in Computer Science, pages 581-590, August 2005. Springer-Verlag. icon icon 

    @InProceedings{ GrassWKJSP2005_lncs3728,
author = {Eckhard Grass and Frank Winkler and Milos Krstic and Alexandra Julius and Christian Stahl and Maxim Piz},
title = {{Enhanced GALS Techniques for Datapath Applications}},
editor = {Vassilis Paliouras and Johan Vounckx and Diederik Verkest},
booktitle = {{Integrated Circuit and System Design: 15th International Workshop, PATMOS 2005, Leuven, Belgium, September 20-23, 2005}},
year = 2005,
series = {Lecture Notes in Computer Science},
volume = 3728,
pages = {581-590},
month = aug,
publisher = {Springer-Verlag},
isbn = {3-540-29013-3},
url = {http://dx.doi.org/10.1007/11556930_59},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/GrassWKJSP2005_lncs3728.pdf},
keywords = {GALS},
abstract = {Based on a previously reported request driven technique for Globally-Asynchronous Locally-Synchronous (GALS) circuits this paper presents two significant enhancements. Firstly, the previously required local ring oscillators are avoided. Instead, an external clock with arbitrary phase for each GALS block is used. Details of the required wrapper circuitry, the proposed design flow and performance are provided. Secondly, to reduce supply noise, a novel approach applying individual clock jitter for GALS blocks is proposed. A simulation using the jitter technique shows that for a typical GALS system, the power spectrum of the supply current can be reduced by about 15 dB.} 
}

  • Sebastian Hinz, Karsten Schmidt, and Christian Stahl. Transforming BPEL to Petri Nets. In Wil M. P. van der Aalst, B. Benatallah, F. Casati, and F. Curbera, editors, Proceedings of the Third International Conference on Business Process Management (BPM 2005), volume 3649 of Lecture Notes in Computer Science, Nancy, France, pages 220-235, September 2005. Springer-Verlag. icon icon 

    @InProceedings{ HinzSS2005_lncs3649,
author = {Sebastian Hinz and Karsten Schmidt and Christian Stahl},
title = {{Transforming BPEL to Petri Nets}},
editor = {{Wil} {M.} {P.} {van} {der} Aalst and B. Benatallah and F. Casati and F. Curbera},
booktitle = {{Proceedings of the Third International Conference on Business Process Management (BPM 2005)}},
year = 2005,
series = {Lecture Notes in Computer Science},
volume = 3649,
pages = {220-235},
address = {Nancy, France},
month = sep,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/HinzSS2005_lncs3649.pdf},
publisher = {Springer-Verlag},
url = {http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/11538394_15},
keywords = {BPEL, Geschäftsprozesse, BPEL-Semantik},
abstract = {We present a Petri net semantics for the Business Process Execution Language for Web Services (BPEL). Our semantics covers the standard behaviour of BPEL as well as the exceptional behaviour (e.g. faults, events, compensation). The semantics is implemented as a parser that translates BPEL specifications into the input language of the Petri net model checking tool LoLA. We demonstrate that the semantics is well suited for computer aided verification purposes.} 
}

  • Milos Krstic, Eckhard Grass, and Christian Stahl. Request-Driven GALS Technique for Wireless Communication System. In Proceedings of the 11th International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC 2005), New York, NY, USA, pages 76-85, March 2005. IEEE Computer Society. icon icon 

    @InProceedings{ KrsticGS2005_async,
author = {Milos Krstic and Eckhard Grass and Christian Stahl},
title = {{Request-Driven GALS Technique for Wireless Communication System}},
booktitle = {{Proceedings of the 11th International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC 2005)}},
year = 2005,
pages = {76-85},
address = {New York, NY, USA},
month = mar,
publisher = {IEEE Computer Society},
isbn = {0-7695-2305-6},
url = {http://doi.ieeecomputersociety.org/10.1109/ASYNC.2005.28},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/KrsticGS2005_async.pdf},
keywords = {GALS},
abstract = {A Globally Asynchronous - Locally Synchronous (GALS) technique for application in wireless communication systems is proposed and evaluated. The GALS wrappers are based on a request-driven operation with an embedded time-out function. A formally verified GALS wrapper is deployed for the ?GALSification? of a baseband processor for WLAN. Details of the GALS partitioning, implementation and the design-flow are discussed. Furthermore, a test strategy based on built-in self-test (BIST) is suggested. The described baseband processor was fabricated and successfully tested. The GALS design is compared with a clock-gated, synchronous version. Advantages for system integration are achieved along with a 1% reduction in dynamic power consumption, a 30% reduction in peak power supply current, and 5 dB reduction in spectral noise.} 
}

  • Axel Martens. Analyzing Web Service based Business Processes. In Maura Cerioli, editor, Proceedings of Intl. Conference on Fundamental Approaches to Software Engineering (FASE'05), Part of the 2005 European Joint Conferences on Theory and Practice of Software (ETAPS'05), volume 3442 of Lecture Notes in Computer Science, Edinburgh, Scotland, April 2005. Springer-Verlag. icon 

    @InProceedings{ Martens2005_lncs3442,
author = {Axel Martens},
title = {{Analyzing Web Service based Business Processes}},
editor = {Maura Cerioli},
booktitle = {{Proceedings of Intl. Conference on Fundamental Approaches to Software Engineering (FASE'05), Part of the 2005 European Joint Conferences on Theory and Practice of Software (ETAPS'05)}},
year = 2005,
series = {Lecture Notes in Computer Science},
volume = 3442,
address = {Edinburgh, Scotland},
month = apr,
publisher = {Springer-Verlag},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Martens2005_lncs3442.pdf},
keywords = {Geschäftsprozesse},
abstract = {This paper is concerned with the application of Web services to distributed, cross-organizational business processes. In this scenario, it is crucial to answer the following questions: Do two Web services fit together in a way such that the composed system is deadlock-free? - the question of compatibility. Can one Web service be replaced by another while the remaining components stay untouched? - the question of equivalence. Can we reason about the soundness of one given Web service without considering the actual environment it will by used in? This paper defines the notion of usability - an intuitive and locally provable soundness criterion for a given Web services. Based on this notion, this paper demonstrates how the other questions could be answered. The presented method is based on Petri nets, because this formalism is widely used for modeling and analyzing business processes. Due to the existing Petri net semantics for BPEL4WS - a language that is in the very act of becoming the industrial standard for Web service based business processes - the results are directly applicable to real world examples.} 
}

  • Axel Martens. Consistency between Executable and Abstract Processes. In Proceedings of Intl. IEEE Conference on e-Technology, e-Commerce, and e-Services (EEE'05), Hong Kong, March 2005. IEEE Computer Society Press. icon 

    @InProceedings{ Martens2005_eee,
author = {Axel Martens},
title = {{Consistency between Executable and Abstract Processes}},
booktitle = {{Proceedings of Intl. IEEE Conference on e-Technology, e-Commerce, and e-Services (EEE'05)}},
year = 2005,
address = {Hong Kong},
month = mar,
publisher = {IEEE Computer Society Press},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Martens2005_eee.pdf},
keywords = {Geschäftsprozesse},
abstract = {Process models play an all-important role in the development of cross-organizational business processes. On the one hand, the interaction between the participating companies often is specified globally, for example by means of multiple abstract process models - one for each partner. On the other hand, each partner defines its local process autonomously in terms of an executable process model. The important question is whether such an executable model is consistent to the predefined abstract model. This paper describes an approach to prove this property automatically.} 
}

  • Axel Martens. Process Oriented Discovery of Business Partners. In Proceedings of 7th Intl. Conference on Enterprise Information Systems (ICEIS'05), Vol 3, Miami, Florida, May 2005. INSTICC. icon 

    @InProceedings{ Martens2005_iceis,
author = {Axel Martens},
title = {{Process Oriented Discovery of Business Partners}},
booktitle = {{Proceedings of 7th Intl. Conference on Enterprise Information Systems (ICEIS'05)}},
year = 2005,
series = {Vol 3},
address = {Miami, Florida},
month = may,
publisher = {INSTICC},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Martens2005_iceis.pdf},
keywords = {Geschäftsprozesse},
abstract = {Emerging technologies and industrial standards in the field of Web services enable a much faster and easier cooperation of distributed partners. With the increasing number of enterprises that offer specific functionality in terms of Web services, discovery of matching partners becomes a serious issue. At the moment, discovery of Web services generally is based on meta-information (e. g. name, business category) and some technical aspects (e. g. interface, protocols). But, this selection might be to coarse grained for dynamic application integration, and there is much more information available. This paper describes a method to discover business partners based on the comparison of their behavior ? specified in terms of their published Web service process models.} 
}

  • Axel Martens. Simulation and Equivalence between BPEL Process Models. In Proceedings of the Design, Analysis, and Simulation of Distributed Systems Symposium (DASD'05), Part of the 2005 Spring Simulation Multiconference (SpringSim'05), San Diego, California, April 2005. icon 

    @InProceedings{ Martens2005_dasd,
author = {Axel Martens},
title = {{Simulation and Equivalence between BPEL Process Models}},
booktitle = {{Proceedings of the Design, Analysis, and Simulation of Distributed Systems Symposium (DASD'05), Part of the 2005 Spring Simulation Multiconference (SpringSim'05)}},
year = 2005,
address = {San Diego, California},
month = apr,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Martens2005_dasd.pdf},
keywords = {BPEL, Geschäftsprozesse},
abstract = {The integration of business process across the boundaries of individual enterprises or business units is becoming increasingly important. In this scenario, process models play an all-important role. On the one hand, the interaction between the participating companies often is specified globally, for example by means of multiple abstract process models - one for each partner. On the other hand, each partner defines its local process autonomously in terms of an executable process model. The important question is whether such an executable model is consistent to the predefined abstract model. This paper defines a simulation relation between BPEL process models, and presents a method to verify consistency automatically, on top of it.} 
}

  • Peter Massuthe, Wolfgang Reisig, and Karsten Schmidt. An Operating Guideline Approach to the SOA. In 2nd South-East European Workshop on Formal Methods 2005 (SEEFM05), Ohrid, Republic of Macedonia, 2005. icon 

    @InProceedings{ MassutheRS2005_seefm,
author = {Peter Massuthe and Wolfgang Reisig and Karsten Schmidt},
title = {{An Operating Guideline Approach to the SOA}},
booktitle = {{2nd South-East European Workshop on Formal Methods 2005 (SEEFM05)}},
year = 2005,
address = {Ohrid, Republic of Macedonia},
ps = {http://www.informatik.hu-berlin.de/top/download/publications/MassutheRS2005_seefm.ps} 


}

  • Peter Massuthe and Karsten Schmidt. Operating Guidelines - an Automata-Theoretic Foundation for the Service-Oriented Architecture. In Kai-Yuan Cai, Atsushi Ohnishi, and M.F. Lau, editors, Proceedings of the Fifth International Conference on Quality Software (QSIC 2005), Melbourne, Australia, pages 452-457, September 2005. IEEE Computer Society. icon 

    @InProceedings{ MassutheS2005_qsic,
author = {Peter Massuthe and Karsten Schmidt},
title = {{Operating Guidelines - an Automata-Theoretic Foundation for the Service-Oriented Architecture}},
editor = {Kai-Yuan Cai and Atsushi Ohnishi and M.F. Lau},
booktitle = {{Proceedings of the Fifth International Conference on Quality Software (QSIC 2005)}},
year = 2005,
pages = {452-457},
address = {Melbourne, Australia},
month = sep,
publisher = {IEEE Computer Society},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/MassutheS2005_qsic.pdf},
keywords = {Services, Operating Guidelines},
abstract = {In the service-oriented architecture (SOA), we distinguish three roles of service owners: service providers, service requesters, and service brokers. Each service provider publishes information to the broker about how requesters can interact with its service. Thus, the broker can assign a fitting service provider to a querying requester. We propose the information published to the broker to be operating guidelines. Operating guidelines are essentially communication instructions for the service requester. We present an automata-theoretic approach that is centered around operating guidelines and is capable of implementing all tasks arising in the SOA.} 
}

  • Peter Massuthe and Karsten Schmidt. Operating Guidelines for Services. In Karsten Schmidt and Christian Stahl, editors, 12. Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN 2005), Proceedings, pages 78-83, September 2005. Humboldt-Universität zu Berlin. icon 

    @InProceedings{ MassutheS2005_awpn,
author = {Peter Massuthe and Karsten Schmidt},
title = {{Operating Guidelines for Services}},
editor = {Karsten Schmidt and Christian Stahl},
booktitle = {{12. Workshop "Algorithmen und Werkzeuge für Petrinetze" (AWPN 2005), Proceedings}},
year = 2005,
pages = {78-83},
month = sep,
publisher = {Humboldt-Universität zu Berlin},
keywords = {Services, Operating Guidelines},
abstract = {In the service-oriented architecture (SOA), we distinguish three roles of service owners:service providers, service requesters, and service brokers, and the three standard operations publish, find, and bind. We provide a formal method based on Petri nets to model services. We suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester?s service and the operating guideline.},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/MassutheS2005_awpn.pdf} 


}

  • Wolfgang Reisig. Modeling- and Analysis Techniques for Web Services and Business Processes. In Martin Steffen and Gianluigi Zavattaro, editors, Formal Methods for Open Object-Based Distributed Systems: 7th IFIP WG 6.1 International Conference, FMOODS 2005, Athens, Greece, June 15-17, 2005. Proceedings, volume 3535 of Lecture Notes in Computer Science, pages 243-258, May 2005. Springer Verlag. icon icon 

    @InProceedings{ Reisig2005_fmoods,
author = {Wolfgang Reisig},
title = {{Modeling- and Analysis Techniques for Web Services and Business Processes}},
editor = {Martin Steffen and Gianluigi Zavattaro},
booktitle = {{Formal Methods for Open Object-Based Distributed Systems: 7th IFIP WG 6.1 International Conference, FMOODS 2005, Athens, Greece, June 15-17, 2005. Proceedings}},
year = 2005,
series = {Lecture Notes in Computer Science},
volume = 3535,
pages = {243-258},
month = may,
publisher = {Springer Verlag},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Reisig2005_fmoods.pdf},
url = {http://dx.doi.org/10.1007/11494881_16},
keywords = {Geschäftsprozesse},
abstract = {Open distributed systems include in particular Web services and business processes. There is a need of techniques to model such systems formally, and to derive decisive properties from such models. Three such techniques are presented in this paper, exemplified by help of realistic examples, and mutually related w.r.t. their respective expressive power and the availability of analysis techniques.} 
}

  • Wolfgang Reisig. On the Expressive Power of Petri Net Schemata. In Gianfranco Ciardo and Philippe Darondeau, editors, Applications and Theory of Petri Nets 2005: 26th International Conference, ICATPN 2005, Miami, USA, June 20-25, 2005. Proceedings, volume 3536 of Lecture Notes in Computer Science, pages 349-364, May 2005. Springer Verlag. icon 

    @InProceedings{ Reisig2005_icatpn,
author = {Wolfgang Reisig},
title = {{On the Expressive Power of Petri Net Schemata}},
editor = {Gianfranco Ciardo and Philippe Darondeau},
booktitle = {{Applications and Theory of Petri Nets 2005: 26th International Conference, ICATPN 2005, Miami, USA, June 20-25, 2005. Proceedings}},
year = 2005,
series = {Lecture Notes in Computer Science},
volume = 3536,
pages = {349-364},
month = may,
publisher = {Springer Verlag},
url = {http://dx.doi.org/10.1007/11494744_20},
abstract = {High-level Petri nets are frequently represented as Petri net schemas, with places, transitions and arcs inscribed by terms. A concrete system is then gained by interpreting the symbols in those terms. The behavior of a concrete system is a transition system. The composition of all those transition systems represents the behavior of the Petri net schema. This paper characterizes the expressive power of (a basic class of) Petri net schemas. It turns out that quite simple as well as quite general requirements at a transition system suffice to generate it by such a Petri net schema.} 
}

  • Karsten Schmidt. Controllability of Open Workflow Nets. In Jörg Desel and Ulrich Frank, editors, Enterprise Modelling and Information Systems Architectures, volume P-75 of Lecture Notes in Informatics (LNI), Bonn, pages 236-249, 2005. Entwicklungsmethoden für Informationssysteme und deren Anwendung (EMISA, RWTH Aachen), Köllen Druck+Verlag GmbH. icon 

    @InProceedings{ Schmidt2005_lnip75,
author = {Karsten Schmidt},
title = {{Controllability of Open Workflow Nets}},
editor = {J{\"{o}}rg Desel and Ulrich Frank},
booktitle = {{Enterprise Modelling and Information Systems Architectures}},
year = 2005,
series = {Lecture Notes in Informatics (LNI)},
volume = {P-75},
pages = {236-249},
address = {Bonn},
organization = {Entwicklungsmethoden für Informationssysteme und deren Anwendung (EMISA, RWTH Aachen)},
publisher = {K{\"{o}}llen Druck+Verlag GmbH},
keywords = {oWFNs, Bedienbarkeit},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Schmidt2005_lnip75.pdf} 


}

  • Christian Stahl, Wolfgang Reisig, and Milos Krstic. Hazard Detection in a GALS Wrapper: A Case Study. In Jörg Desel and Y. Watanabe, editors, Proceedings of the Fifth International Conference on Application of Concurrency to System Design (ACSD'05), St. Malo, France, pages 234-243, June 2005. IEEE Computer Society. icon icon 

    @InProceedings{ StahlRK2005_acsd,
author = {Christian Stahl and Wolfgang Reisig and Milos Krstic},
title = {{Hazard Detection in a GALS Wrapper: A Case Study}},
editor = {Jörg Desel and Y. Watanabe},
booktitle = {{Proceedings of the Fifth International Conference on Application of Concurrency to System Design (ACSD'05)}},
year = 2005,
pages = {234-243},
address = {St. Malo, France},
month = jun,
publisher = {IEEE Computer Society},
url = {http://doi.ieeecomputersociety.org/10.1109/ACSD.2005.20},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/StahlRK2005_acsd.pdf},
keywords = {GALS, LoLA},
abstract = {An asynchronous wrapper of a fabricated GALS system is analyzed for hazards. For this purpose a Petri net based modelling approach of this GALS wrapper is presented. In our model the question whether a hazard can occur in a gate is reduced to a model checking problem: the reachability of a particular marking in the Petri net. In order to alleviate state space explosion two techniques to reduce the model's state space are presented. By use of these techniques we detected several potential hazards and a deadlock in the wrapper.} 
}

  • Ingo Stürmer, Daniela Weinberg, and Mirko Conrad. Overview of Existing Safeguarding Techniques for Automatically Generated Code. In SEAS '05: Proceedings of the Second International Workshop on Software Engineering for Automotive Systems, New York, NY, USA, pages 1-6, 2005. ACM Press. icon 

    @InProceedings{ StuermerWC2005_icse,
author = {Ingo Stürmer and Daniela Weinberg and Mirko Conrad},
title = {{Overview of Existing Safeguarding Techniques for Automatically Generated Code}},
booktitle = {{SEAS '05: Proceedings of the Second International Workshop on Software Engineering for Automotive Systems}},
year = {2005},
pages = {1-6},
address = {New York, NY, USA},
publisher = {ACM Press},
isbn = {1-59593-128-7},
location = {St. Louis, Missouri},
url = {http://doi.acm.org/10.1145/1083190.1083192},
abstract = {Code generators are increasingly used in an industrial context to translate graphical models into executable code. Since the code is often deployed in safety-related environments, the quality of the code generators is of paramount importance. In this paper, we will present and discuss state-of-the-art techniques for safeguarding automatic code generation applied in model-based development.} 
}

  • Daniela Weinberg and Karsten Schmidt. Reduction Rules for Interaction Graphs. In Karsten Schmidt and Christian Stahl, editors, 12. Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN 2005), Proceedings, pages 60-65, September 2005. Humboldt-Universität zu Berlin. 

    @InProceedings{ WeinbergS2005_awpn,
author = {Daniela Weinberg and Karsten Schmidt},
title = {{Reduction Rules for Interaction Graphs}},
editor = {Karsten Schmidt and Christian Stahl},
booktitle = {{12. Workshop "Algorithmen und Werkzeuge für Petrinetze" (AWPN 2005), Proceedings}},
year = 2005,
pages = {60-65},
month = sep,
publisher = {Humboldt-Universität zu Berlin},
keywords = {Geschäftsprozesse, Bedienbarkeit, oWFNs},
abstract = {The internet today has grown to be more than just being a basisfor exchanging information. It steadily becomes a platform for processing business processes. Many companies distribute their service with the help of web services or integrate other web services into their own workflow. However, before a web service gets published it should be examined well. We will introduce a way of examining the controllability of a web service. We propose the interaction graph of a web service, that is modelled by an open workflow net. To verify whether such a net is controllable or not it is sufficient to construct a reduced interaction graph. We will define reduction rules that minimize the size of the graph greatly. The analysis using the interaction graph as well as the reduction rules are implemented and have been integrated into an analysis tool kit for web services.} 
}

Technische Berichte

  • Dirk Fahland. Complete Abstract Operational Semantics for the Web Service Business Process Execution Language. Informatik-Berichte 190, Humboldt-Universität zu Berlin, September 2005. icon 

    @TechReport{ Fahland2005_hub_tr190,
author = {Dirk Fahland},
title = {{Complete Abstract Operational Semantics for the Web Service Business Process Execution Language}},
institution = {Humboldt-Universität zu Berlin},
year = 2005,
type = {Informatik-Berichte},
number = 190,
month = sep,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Fahland2005_hub_tr190.pdf},
keywords = {BPEL, ASM, BPEL-Semantik},
abstract = {In this technical report we present an abstract operational semantics for the Business ProcessExecution Language for Web Services, or BPEL for short. In effect, the semantics defined herein are a variation and an extension of the semantics published first in [FGV04a] and [Far04] defined by the group of Uwe Glässer the Simon Fraser University, Vancouver, Canada. We namely add semantics for correlation handling, dead path elimination and event handling; we define the data handling on a finer level; we slightly alter the basic framework of how activities are formalized in [FGV04a] in order to achieve greater robustness against changes of the informal specification. Furthermore this technical report serves as a base for a joint work with the group of Simon Fraser University.} 
}

  • Peter Massuthe, Wolfgang Reisig, and Karsten Schmidt. An Operating Guideline Approach to the SOA. Informatik-Berichte 191, Humboldt-Universität zu Berlin, 2005. icon 

    @TechReport{ MassutheRS2005_hub_tr191,
author = {Peter Massuthe and Wolfgang Reisig and Karsten Schmidt},
title = {{An Operating Guideline Approach to the SOA}},
institution = {Humboldt-Universität zu Berlin},
year = 2005,
type = {Informatik-Berichte},
number = 191,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/MassutheRS2005_hub_tr191.pdf},
keywords = {Services, Operating guidelines, oWFNs},
abstract = {Interorganizational cooperation is more and more organized by the paradigm of services. The service-oriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the three operations publish, find, and bind. We provide a formal method based on Petri nets to model services and their cooperation. We characterize well-behaving pairs of requester?s and provider?s services and suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester?s service and the operating guideline. Binding of a requester?s and a provider?s service is therefore guaranteed to result in a well-behaving cooperating service.} 
}

  • Peter Massuthe and Karsten Schmidt. Matching Nondeterministic Services with Operating Guidelines. Informatik-Berichte 193, Humboldt-Universität zu Berlin, June 2005. icon 

    @TechReport{ MassutheS2005_hub_tr193,
author = {Peter Massuthe and Karsten Schmidt},
title = {{Matching Nondeterministic Services with Operating Guidelines}},
institution = {Humboldt-Universität zu Berlin},
year = 2005,
type = {Informatik-Berichte},
number = 193,
month = jun,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/MassutheS2005_hub_tr193.pdf},
keywords = {Services, Operating Guidelines, Matching},
abstract = {Abstract Interorganizational cooperation is more and more organizedby the paradigm of services. The service-oriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the operations publish, find, and bind. We provide a formal method based on nondeterministic automata to model services and their interaction. We suggest operating guidelines as a convenient and intuitive artifact to realize publish. In our approach, the find operation reduces to a matching problem between the requester?s service and operating guidelines. In this paper, matching of deterministic as well as nondeterministic automata with operating guidelines is presented.} 
}

  • Peter Massuthe and Karsten Schmidt. Operating Guidelines - an Alternative to Public View. Informatik-Berichte 189, Humboldt-Universität zu Berlin, 2005. icon 

    @TechReport{ MassutheS2005_hub_tr189,
author = {Peter Massuthe and Karsten Schmidt},
title = {{Operating Guidelines - an Alternative to Public View}},
institution = {Humboldt-Universität zu Berlin},
year = 2005,
type = {Informatik-Berichte},
number = 189,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/MassutheS2005_hub_tr189.pdf},
keywords = {Services, Operating guidelines},
abstract = {We propose operating guidelines as artifacts for publishing information about how to communicate with a business process that is intended to be provided as a service. We present an approach to compute operating guidelines fully automatically. We compare operating guidelines with the concept of public view.} 
}

  • Wolfgang Reisig. Modeling- and Analysis Techniques for Web Services and Business Processes. Informatik-Berichte 183, Humboldt-Universität zu Berlin, 2005. 

    @TechReport{ Reisig2005_hub_tr183,
author = {Wolfgang Reisig},
title = {{Modeling- and Analysis Techniques for Web Services and Business Processes}},
institution = {Humboldt-Universität zu Berlin},
year = 2005,
type = {Informatik-Berichte},
number = 183,
keywords = {Geschäftsprozesse} 
}

  • Wolfgang Reisig, Karsten Schmidt, and Christian Stahl. Verteilte Geschäftsprozesse modellieren und analysieren. Informatik-Berichte 182, Humboldt-Universität zu Berlin, February 2005. icon 

    @TechReport{ ReisigSS2005_hub_tr182,
author = {Wolfgang Reisig and Karsten Schmidt and Christian Stahl},
title = {{Verteilte Geschäftsprozesse modellieren und analysieren}},
institution = {Humboldt-Universität zu Berlin},
year = 2005,
type = {Informatik-Berichte},
number = 182,
month = feb,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/ReisigSS2005_hub_tr182.pdf},
keywords = {Petrinetze, oWFNs, BPEL, Bedienbarkeit},
abstract = {Verteilte Geschäftsprozesse nutzen das Internet, um auf heterogenen Rechnerstrukturen Dienste auszubieten. Modellierungstechniken und Implementierungssprachen für solche Dienste werfen im Vergleich mit herkömmlichen Rechnern grundlegend neue Fragestellungen auf. Wir diskutieren einige davon und zeigen, wie Petrinetze ihre Beantwortung ermöglichen.} 
}

  • Karsten Schmidt. Controlability of Distributed Business Processes. Informatik-Berichte 180, Humboldt-Universität zu Berlin, 2005. 

    @TechReport{ Schmidt2005_hub_tr180,
author = {Karsten Schmidt},
title = {{Controlability of Distributed Business Processes}},
institution = {Humboldt-Universität zu Berlin},
year = 2005,
type = {Informatik-Berichte},
number = 180,
keywords = {Bedienbarkeit} 
}

  • Karsten Schmidt and Christian Stahl. 12. Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN 2005), Proceedings. Informatik-Berichte 192, Humboldt-Universität zu Berlin, September 2005. icon 

    @TechReport{ SchmidtS2005_hub_tr192,
author = {Karsten Schmidt and Christian Stahl},
title = {{12. Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN 2005), Proceedings}},
institution = {Humboldt-Universität zu Berlin},
year = 2005,
type = {Informatik-Berichte},
number = 192,
month = sep,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/SchmidtS2005_hub_tr192.pdf},
keywords = {Petrinetze} 
}

  • Christian Stahl. A Petri Net Semantics for BPEL. Informatik-Berichte 188, Humboldt-Universität zu Berlin, July 2005. icon 

    @TechReport{ Stahl2005_hub_tr188,
author = {Christian Stahl},
title = {{A Petri Net Semantics for BPEL}},
institution = {Humboldt-Universität zu Berlin},
year = 2005,
type = {Informatik-Berichte},
number = 188,
month = jul,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Stahl2005_hub_tr188.pdf},
keywords = {Geschäftsprozesse, BPEL, BPEL-Semantik},
abstract = {We present a pattern-based Petri net semantics for the Business Process Execution Language for Web Services (BPEL). Our semantics is complete - it covers the standard behaviour of BPEL as well as the exceptional behav-iour (e.g. faults, events, compensation). Therefore every business process specified in BPEL can be transformed into a Petri net.} 
}

  • Christian Stahl, Wolfgang Reisig, and Milos Krstic. Hazard Detection in a GALS Wrapper: a Case study. Informatik-Berichte 184, Humboldt-Universität zu Berlin, February 2005. icon 

    @TechReport{ StahlRK2005_hub_tr184,
author = {Christian Stahl and Wolfgang Reisig and Milos Krstic},
title = {{Hazard Detection in a GALS Wrapper: a Case study}},
institution = {Humboldt-Universität zu Berlin},
year = 2005,
type = {Informatik-Berichte},
number = 184,
month = feb,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/StahlRK2005_hub_tr184.pdf},
keywords = {GALS, LoLA},
abstract = {An asynchronous wrapper of a fabricated GALS system is analyzed for hazards. For this purpose a Petri net based modelling approach of this GALS wrapper is presented. In our model the question whether a hazard can occur in a gate is reduced to a model checking problem: the reachability of a particular marking in the Petri net. In order to alleviate state space explosion three techniques to reduce the model?s state space are presented. By use of these techniques we detected several potential hazards in the wrapper.} 
}

Studien- und Diplomarbeiten

  • Alexander Brade. ASMs und die Struktur und Dynamik von Web Services. Studienarbeit, Humboldt-Universität zu Berlin, January 2005. icon 

    @MastersThesis{ Brade2005_sa,
author = {Alexander Brade},
title = {{ASMs und die Struktur und Dynamik von Web Services}},
school = {Humboldt-Universität zu Berlin},
year = 2005,
type = {Studienarbeit},
month = jan,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Brade2005_sa.pdf},
keywords = {ASM, Geschäftsprozesse} 
}

  • Alexander Brade. Übersetzung graphischer Verhaltensbeschreibungen von Services in Abstract State Machines. Diplomarbeit, Humboldt-Universität zu Berlin, September 2005. icon 

    @MastersThesis{ Brade2005_da,
author = {Alexander Brade},
title = {{Übersetzung graphischer Verhaltensbeschreibungen von Services in Abstract State Machines}},
school = {Humboldt-Universität zu Berlin},
year = 2005,
type = {Diplomarbeit},
month = sep,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Brade2005_da.pdf},
keywords = {ASM},
abstract = {Zu Beginn dieser Arbeit werden wir kurz die Begriffe Service OrientedArchitecture und Service erklären. Den Begriff der Services werden wir genauer betrachten. Im Anschluss daran werden wir die Frage behandeln, wie das dynamische Verhalten eines Services mit UML 2-Diagrammen (UML = Unified Modeling Language) graphisch beschrieben werden kann. Dazu werden wir uns besonders auf die UML 2-Verhaltensdiagramme konzentrieren. Dabei werden wir auch einige Einschränkungen an den Verhaltensdiagrammen vornehmen. Wir werden dann das dynamische Verhalten eines beispielhaften DinnerServices mit Hilfe von Verhaltensdiagrammen beschreiben. Diese Verhaltensdiagramme des DinnerServices werden wir in Abstract State Machines (ASMs) übersetzen. Zwei der so erhaltenen ASMs werden wir im Anschluss an die Verhaltensbeschreibungen des DinnerServices in die Spezifikationssprache AsmL überführen und simulieren. Abschließend betrachten wir kurz die Verfeinerungsmöglichkeiten von ASMs.} 
}

  • Carsten Frenkler. Modellierung und Analyse transaktionaler Geschäftsprozesse. Diplomarbeit, Humboldt-Universität zu Berlin, July 2005. icon 

    @MastersThesis{ Frenkler2005_da,
author = {Carsten Frenkler},
title = {{Modellierung und Analyse transaktionaler Geschäftsprozesse}},
school = {Humboldt-Universität zu Berlin},
year = 2005,
type = {Diplomarbeit},
month = jul,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Frenkler2005_da.pdf},
keywords = {Geschäftsprozesse},
abstract = {Die vorliegende Arbeit beschäftigt sich mit zwei wichtigen Aspekten von Geschäftsprozessen. Das ist einerseits die Frage, ob die Funktionalität eines Prozesses genutzt werden kann und andererseits die Frage, ob die Transaktionen eines Prozesses vernünftig verarbeitet werden können. Für die Analyse der beiden Aspekte wird ein geeignetes Modell benötigt. Hierfür werden die auf Petrinetzen basierenden Workflow-Module erweitert, indem transaktionale Eigenschaften in ein Petrinetz übersetzt werden und in das Modul integriert werden. Letztlich liefert die Analyse der Bedienbarkeit des erweiterten Moduls eine Antwort auf beide Fragen.} 
}

  • Andreas Glausch. Varianten des ASM-Theorems. Diplomarbeit, Humboldt-Universität zu Berlin, June 2005. icon 

    @MastersThesis{ Glausch2005_da,
author = {Andreas Glausch},
title = {{Varianten des ASM-Theorems}},
school = {Humboldt-Universität zu Berlin},
year = 2005,
type = {Diplomarbeit},
month = jun,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Glausch2005_da.pdf},
keywords = {ASM},
abstract = {Abstract-State-Machines, kurz ASMs, sind eine Methode zur formalen Beschreibung von Algorithmen. Diese Methode hebt sich dabei deutlich von klassischen Algorithmusbegriffen wie Turingmaschinen und berechenbaren Funktionen ab. So lassen sich mit ASMs unter anderem auch nicht-terminierende Algorithmen beschreiben. Genauso wie es unterschiedliche Klassen von Algorithmen gibt, existieren auch eine ganze Reihe unterschiedlicher Klassen von ASMs, so zum Beispiel die sequentiellen, die nichtdeterministischen und die verteilten ASMs. Für die Klasse der sequentiellen ASMs exisitiert eine schöne Charakterisierung durch das sogenannte ASM-Theorem. Diese Charakterisierung basiert auf natürlichen und leicht verständlichen Forderungen und erleichtert somit dass Verständnis für die Ausdrucksmächtigkeit der sequentiellen ASMs und von Algorithmen im Allgemeinen. In dieser Arbeit erweitern wir das ASM-Theorem auf die Klasse der nichtdeterministischen ASMs und auf die Klasse der verteilten ASMs.} 
}

  • Sebastian Hinz. Implementierung einer Petrinetz-Semantik für BPEL. Diplomarbeit, Humboldt-Universität zu Berlin, March 2005. icon 

    @MastersThesis{ Hinz2005_da,
author = {Sebastian Hinz},
title = {{Implementierung einer Petrinetz-Semantik für BPEL}},
school = {Humboldt-Universität zu Berlin},
year = 2005,
type = {Diplomarbeit},
month = mar,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Hinz2005_da.pdf},
keywords = {BPEL, Geschäftsprozesse, BPEL-Semantik},
abstract = {BPEL ist eine Modellierungssprache zur Beschreibung von verteilten Geschäftsprozessen mit Webservices. Um mit formalen Methoden die Sprache selbst und in BPEL modellierte Prozesse verifizieren zu können, wird eine formale Semantik benötigt. Auf der Basis von Petrinetzen wurde bereits eine solche Semantik entwickelt. Um die Analyse eines Prozesses zu ermöglichen wird ein Werkzeug benötigt, das die Transformation des Prozesses in ein Petrinetz übernimmt. In der vorliegenden Arbeit wird ein solches Werkzeug entwickelt, vorgestellt und seine Funktionsweise erläutert.} 
}

  • Alexandra Julius. Entwurf und VHDL-Modellierung von mesochronen GALS-Schaltungen. Studienarbeit, Humboldt-Universität zu Berlin, December 2005. icon 

    @MastersThesis{ Julius2005_sa,
author = {Alexandra Julius},
title = {{Entwurf und VHDL-Modellierung von mesochronen GALS-Schaltungen}},
school = {Humboldt-Universit{\"{a}}t zu Berlin},
year = 2005,
type = {Studienarbeit},
month = dec,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Julius2005_sa.pdf},
keywords = {GALS},
abstract = {Die vorliegende Arbeit beschreibt Entwurf und VHDL-Modellierung global-asynchroner lokal-synchroner (GALS) Schaltungen, die sich von bisherigen Entwurfsmethoden abheben. Grundlage unserer Forschung ist der am IHP entwickelte request-getriebene GALSWrapper, dessen lokale Takterzeugung bisher unter Verwendung von Ring-Oszillatoren realisiert wurde. Dieser heterochrone Ansatz verkompliziert jedoch Entwurf und Inbetriebnahme der GALS-Schaltung. Zusätzlich steigt durch den Gebrauch von Ring-Oszillatoren der Energieverbrauch insgesamt an, und es wird mehr Chipfläche benötigt. Wir entwickeln daher einen GALS-Wrapper, der mesochron realisiert ist und mit einer globalen Taktversorgung auskommt. Der Wechsel von heterochronen zu mesochronen GALS-Schaltungen bringt unter anderem die Schwierigkeit mit sich, eine sinnvolle Taktsynchronisation herzustellen. Darüber hinaus ergibt sich die beim Design asynchroner Systeme übliche Aufgabe des korrekten Schaltungsentwurfs. Insbesondere muss darauf geachtet werden, dass in der Schaltung keine Hazards entstehen, die das System negativ beeinflussen können. In dieser Arbeit ersetzen wir den heterochronen GALS-Wrapper durch einen mesochronen. Wir zeigen insbesondere, dass durch den mesochronen Ansatz sowohl Datendurchsatz erhöht als auch Energieverbrauch gemindert werden. Die resultierenden Ergebnisse wurden in einem Papier [GWK+05] festgehalten, das für die Patmos Konferenz 2005 akzeptiert wurde.} 
}

  • Niels Lohmann. Formale Fundierung und effizientere Algorithmen für die schrittbasierte TLDA-Interleavingsemantik. Diplomarbeit, Humboldt-Universität zu Berlin, September 2005. icon 

    @MastersThesis{ Lohmann2005_da,
author = {Niels Lohmann},
title = {{Formale Fundierung und effizientere Algorithmen für die schrittbasierte TLDA-Interleavingsemantik}},
school = {Humboldt-Universität zu Berlin},
year = 2005,
type = {Diplomarbeit},
month = sep,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Lohmann2005_da.pdf},
keywords = {TLDA, Temporale Logik},
abstract = {Die Temporal Logic of Distributed Actions (TLDA) ist eine neue temporale Logik miteiner Halbordnungssemantik und eignet sich somit zur Spezifikation verteilter Systeme. Allerdings existieren für TLDA noch keine Werkzeuge, die die Spezifikation und Verifikation unterstützen. Die Verfügbarkeit solcher Werkzeuge trägt jedoch entscheidend zur Verbreitung der Logik bei. In [Loh05] wurde mit der Ausarbeitung und Implementierung einer schrittbasierten Interleavingsemantik für TLDA die Grundlage für die Entwicklung eines expliziten TLDA-Modelcheckers gelegt. Der genaue Zusammenhang zwischen der Halbordnungs- und Interleavingsemantik wurde jedoch nicht bewiesen. Außerdem handelt es sich bei der Implementierung der Interleavingsemantik um einen Brute-Force-Prototyp, der nur für sehr einfach Spezifikationen in der Lage ist das Transitionssystem zu konstruieren. Die formale Fundierung sowie die Ausarbeitung effizienter Algorithmen und Datenstrukturen ist Inhalt dieser Arbeit. Anhand mehrerer Fallstudien untersuchen wir die Leistungsfähigkeit des erweiterten Prototyps und illustrieren die Beziehung zwischen der Halbordnungs- und Interleavingsemantik.} 
}

  • Niels Lohmann. Implementierung einer schrittbasierten Interleavingsemantik für die Temporal Logic of Distributed Actions (TLDA). Studienarbeit, Humboldt-Universität zu Berlin, June 2005. icon 

    @MastersThesis{ Lohmann2005_sa,
author = {Niels Lohmann},
title = {{Implementierung einer schrittbasierten Interleavingsemantik für die Temporal Logic of Distributed Actions (TLDA)}},
school = {Humboldt-Universität zu Berlin},
year = 2005,
type = {Studienarbeit},
month = jun,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Lohmann2005_sa.pdf},
keywords = {TLDA, Temporale Logik},
abstract = {Die Temporal Logic of Distributed Actions (TLDA) ist eine temporale Logik mit einer Halbordnungssemantik und eignet sich somit zur Spezifikation verteilter Systeme. Allerdings gibt es noch wenig Erfahrung bei der computergestützten Verifikation halbordnungsbasierter Formalismen. Viele bekannte effiziente Algorithmen des expliziten Modelchecking setzen ein Transitionssystem und somit eine Interleavingsemantik voraus. In dieser Arbeit wird eine Interleavingsemantik für TLDA vorgeschlagen und ein Prototyp entwickelt, der für eine bestimmte Klasse von TLDA-Spezifikationen das Transitionssystem aufbaut. Die entwickelte Semantik soll zusammen mit dem Prototypen die Grundlage für die weitere Arbeit an einem Modelchecker für TLDA sein.} 
}

  • Elke Salecker and Nora Toussaint. Gegenbeispielgesteuerte Abstraktionsverfeinerung in High-Level-Petrinetzen. Diplomarbeit, Humboldt-Universität zu Berlin, September 2005. icon 

    @MastersThesis{ SaleckerT2005_da,
author = {Elke Salecker and Nora Toussaint},
title = {{Gegenbeispielgesteuerte Abstraktionsverfeinerung in High-Level-Petrinetzen}},
school = {Humboldt-Universität zu Berlin},
year = 2005,
type = {Diplomarbeit},
month = sep,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/SaleckerT2005_da.pdf} 


}

zurück zur Übersicht zurück zur Übersicht

Theorie der Programmierung | Kontakt | XHTML 1.0 | Thu Feb 18 13:30:02 2010