union jack
Publikationen
Institut für Informatik

Publikationen des Jahres 2006

Bücher und Konferenzbände

  • Wolfgang Reisig and Johann-Christoph Freytag, editors. Informatik - Aktuelle Themen im historischen Kontext. Springer, May 2006. 

    @Book{ ReisigF2006_iathk,
editor = {Wolfgang Reisig and Johann-Christoph Freytag},
title = {{Informatik - Aktuelle Themen im historischen Kontext}},
publisher = {Springer},
year = 2006,
month = may,
isbn = {3-540-32742-8} 
}

Publikationen in Zeitschriften und Büchern

  • Wilfried Brauer and Wolfgang Reisig. Carl Adam Petri und die ``Petrinetze''. Informatik-Spektrum, 29(5):369--381, October 2006. icon 

    @Article{ BrauerR2006_is,
author = {Wilfried Brauer and Wolfgang Reisig},
title = {{Carl Adam Petri und die ``Petrinetze''}},
journal = {Informatik-Spektrum},
year = {2006},
volume = {29},
number = {5},
pages = {369--381},
month = {oct},
url = {http://www.springerlink.com/content/vkq33g14w7j05127/} 
}

  • Milos Krstic, Eckhard Grass, Christian Stahl, and Maxim Piz. System Integration by Request-driven GALS Design. IEE Proc. Computers & Digital Techniques, 153(5):362--372, September 2006. icon icon 

    @Article{ KrsticGSP2006_iee,
author = "Milo\v{s} Krsti\'{c} and Eckhard Grass and Christian Stahl and Maxim Piz",
title = "{System Integration by Request-driven GALS Design}",
journal = "{IEE} Proc. Computers \& Digital Techniques",
year = "2006",
volume = "153",
number = "5",
pages = "362--372",
month = "September",
url = "http://dx.doi.org/10.1049/ip-cdt:20050210",
pdf = "http://www.informatik.hu-berlin.de/top/download/publications/KrsticGSP2006_iee.pdf",
abstract = "A novel request-driven globally asynchronous locally synchronous (GALS) technique for the system integration of complex digital blocks is proposed. For this new GALS technique, an asynchronous wrapper compliant is developed and evaluated. This proposed GALS technique is applied to a baseband processor compatible with the wireless LAN standard IEEE 802.11a. The developed GALS baseband processor chip is fabricated and measured. Besides improvements of the system integration process, a 5 dB reduction in electromagnetic interference, 30\% reduction in instantaneous supply current variation, and similar dynamic power consumption as in the synchronous baseband processor is achieved.",
keywords = "GALS" 
}

  • Peter Massuthe and Karsten Wolf. Operating Guidelines for Services. Petri Net Newsletter, 70:9-14, April 2006. icon 

    @Article{ MassutheW2006_pnn70,
author = {Peter Massuthe and Karsten Wolf},
title = {{Operating Guidelines for Services}},
journal = {Petri Net Newsletter},
year = 2006,
volume = 70,
pages = {9-14},
month = apr,
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/MassutheW2006_pnn70.pdf} 


}

Konferenzbeiträge und Beiträge auf Workshops

  • Wil M. P. van der Aalst, Michael Beisiegel, Kees M. van Hee, Dieter König, and Christian Stahl. A SOA-Based Architecture Framework. In Frank Leymann, Wolfgang Reisig, Satish R. Thatte, and Wil M. P. van der Aalst, editors, The Role of Business Processes in Service Oriented Architectures, number 06291 of Dagstuhl Seminar Proceedings, November 2006. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany. 

    @InProceedings{ AalstBHKS2006_dagstuhl,
author = {{Wil} {M.} {P.} {van} {der} Aalst and Michael Beisiegel and {Kees} {M.} {van} Hee and Dieter K{\"o}nig and Christian Stahl},
title = {{A SOA-Based Architecture Framework}},
editor = {Frank Leymann and Wolfgang Reisig and Satish R. Thatte and {Wil} {M.} {P.} {van} {der} Aalst},
booktitle = {The Role of Business Processes in Service Oriented Architectures},
year = {2006},
series = {Dagstuhl Seminar Proceedings},
month = {nov},
publisher = {Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany},
number = {06291},
issn = {1862-4405},
optaddress = {Dagstuhl, Germany},
opturl = {http://drops.dagstuhl.de/opus/volltexte/2006/827[date of citation: 2006-01-01]},
keywords = {SOA, architecture framework},
abstract = {In this paper we present first results of a SOA-based architecture framework. The architecture framework is required to be close to industry standards, especially to service component architecture (SCA), language independent (i.e. it is adoptable) and the building blocks of each system, activities and data, are first class citizens. We present a meta model of the architecture framework and discuss its concepts in detail.} 
}

  • Baver Acu and Wolfgang Reisig. Compensation in Workflow Nets. In Susanna Donatelli and P. S. Thiagarajan, editors, Petri Nets and Other Models of Concurrency - ICATPN 2006, 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, Turku, Finland, June 26-30, 2006, Proceedings, volume 4024 of Lecture Notes in Computer Science, pages 65-83, 2006. Springer. icon 

    @InProceedings{ AcuR2006_icatpn,
author = {Baver Acu and Wolfgang Reisig},
title = {{Compensation in Workflow Nets}},
editor = {Susanna Donatelli and P. S. Thiagarajan},
booktitle = {{Petri Nets and Other Models of Concurrency - ICATPN 2006, 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, Turku, Finland, June 26-30, 2006, Proceedings}},
year = 2006,
series = {Lecture Notes in Computer Science},
volume = 4024,
pages = {65-83},
publisher = {Springer},
isbn = {3-540-34699-6},
url = {http://www.springerlink.com/content/91l0123472t2l261/} 
}

  • Andreas Glausch. Distributed Abstract State Machines - Status Report of a Doctoral Thesis. In Jörg Desel, editor, Proceedings of the Doctoral Consortium ACSD & PetriNets 2006, Turku, Finland, June 2006. Åbo Akademi. icon 

    @InProceedings{ Glausch2006_dc,
author = {Andreas Glausch},
title = {{Distributed Abstract State Machines - Status Report of a Doctoral Thesis}},
editor = {Jörg Desel},
booktitle = {{Proceedings of the Doctoral Consortium ACSD {\&} PetriNets 2006}},
year = 2006,
address = {Turku, Finland},
month = jun,
publisher = {Åbo Akademi},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Glausch2006_dc.pdf},
abstract = {In 1985, Gurevich introduced Abstract State Machines (ASMs) as a computational model more powerful and universal than classical computational models. Since then ASMs have been applied successfully both in theory and practice: On the theoretical side, ASMs evolved to a general basis for the study of different classes of algorithms and their expressive power. On the practical side, ASMs have been extended to a full-fledged design methodology, applied successfully in industry for the specification and analysis of real-world systems. In my doctoral thesis I examine the class of distributed ASMs and study their expressive power. I also intend to develop basic notions of refinement and composition for distributed ASMs.} 
}

  • Andreas Glausch and Wolfgang Reisig. How Expressive are Petri Net Schemata?. In Susanna Donatelli and P. S. Thiagarajan, editors, Petri Nets and Other Models of Concurrency - ICATPN 2006, 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, Turku, Finland, June 26-30, 2006, Proceedings, volume 4024 of Lecture Notes in Computer Science, pages 201-220, 2006. Springer. icon icon 

    @InProceedings{ GlauschR2006_icatpn,
author = {Andreas Glausch and Wolfgang Reisig},
title = {{How Expressive are Petri Net Schemata?}},
editor = {Susanna Donatelli and P. S. Thiagarajan},
booktitle = {{Petri Nets and Other Models of Concurrency - ICATPN 2006, 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, Turku, Finland, June 26-30, 2006, Proceedings}},
year = 2006,
series = {Lecture Notes in Computer Science},
volume = 4024,
pages = {201-220},
publisher = {Springer},
isbn = {3-540-34699-6},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/GlauschR2006_icatpn.pdf},
url = {http://www.springerlink.com/content/54224646621v5x10/},
abstract = {Petri net schemata are an intuitive and expressive approach to describe high-level Petri nets. A Petri net schema is a Petri net with edges and transitions inscribed by terms and Boolean expressions, respectively. A concrete high-level net is gained by interpreting the symbols in the inscriptions by a structure. Its semantics can then be described in terms of a transition system. Therefore, the semantics of a Petri Net schema can be conceived as a family of transition systems indexed by structures. In this paper we characterize the expressive power of a general version of Petri net schemata. For that purpose we examine families of transition systems in general and characterize the families as generated by Petri net schemata. It turns out that these families of transition systems can be characterized by simple and intuitive requirements.} 
}

  • Kathrin Kaschner, Peter Massuthe, and Karsten Wolf. Symbolische Repräsentation von Bedienungsanleitungen für Services. In Daniel Moldt, editor, 13. Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN 2006), Proceedings, pages 54-61, September 2006. Universität Hamburg. Note: In German. icon 

    @InProceedings{ KaschnerMW2006_awpn,
author = {Kathrin Kaschner and Peter Massuthe and Karsten Wolf},
title = {{Symbolische Repräsentation von Bedienungsanleitungen für Services}},
editor = {Daniel Moldt},
booktitle = {{13. Workshop "Algorithmen und Werkzeuge für Petrinetze" (AWPN 2006), Proceedings}},
year = 2006,
pages = {54-61},
month = sep,
publisher = {Universität Hamburg},
note = {in German},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/KaschnerMW2006_awpn.pdf},
keywords = {Services, Operating Guidelines, Matching, BDD} 
}

  • Oliver Kopp, Carsten Frenkler, and Niels Lohmann. Korrektheit und Zuverlässigkeit zusammengesetzter Web Services am Beispiel der Geschäftsprozess-Modellierungssprache BPEL. In Forschungsoffensive ''Software Engineering 2006'', Statuskonferenz, 26.-28. Juni 2006, July 2006. Bundesministerium für Bildung und Forschung (BMBF). icon 

    @INPROCEEDINGS{KoppFL2006_status,
author = {Oliver Kopp and Carsten Frenkler and Niels Lohmann},
title = {{Korrektheit und Zuverlässigkeit zusammengesetzter Web Services am Beispiel der Geschäftsprozess-Modellierungssprache BPEL}},
year = {2006},
booktitle = {Forschungsoffensive ''Software Engineering 2006'', Statuskonferenz, 26.-28. Juni 2006},
pdf = {ftp://ftp.informatik.uni-stuttgart.de/pub/library/ncstrl.ustuttgart_fi/INPROC-2006-67/INPROC-2006-67.pdf},
month = jul,
publisher = {Bundesministerium für Bildung und Forschung (BMBF)},
keywords = {Tools4BPEL} 
}

  • Niels Lohmann. A Local Cut-off Criterion for Unfoldings of Safe Petri Nets. In Jörg Desel, editor, Proceedings of the Doctoral Consortium ACSD & Petri Nets 2006, Turku, Finland, June 2006. Åbo Akademi. icon 

    @InProceedings{ Lohmann2006_dc,
author = {Niels Lohmann},
title = {{A Local Cut-off Criterion for Unfoldings of Safe Petri Nets}},
editor = {Jörg Desel},
booktitle = {{Proceedings of the Doctoral Consortium ACSD {\&} Petri Nets 2006}},
year = 2006,
address = {Turku, Finland},
month = jun,
publisher = {Åbo Akademi},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Lohmann2006_dc.pdf},
abstract = {Finite prefixes of branching processes are a compact way to represent the state space of finite safe systems. McMillan in [1] formulated a cut-off criterion stating under which conditions the (usually infinite) maximal branching process can be truncated without loosing reachable markings. However, this criterion depends on the reachable markings itself and thus suffers the state explosion problem. In this work, we propose local cut-off criteria that base on partial markings.} 
}

  • Niels Lohmann, Peter Massuthe, Christian Stahl, and Daniela Weinberg. Analyzing Interacting BPEL Processes. In Schahram Dustdar, José Luiz Fiadeiro, and Amit Sheth, editors, Business Process Management, 4th International Conference, BPM 2006, Vienna, Austria, September 5-7, 2006, Proceedings, volume 4102 of Lecture Notes in Computer Science, pages 17-32, September 2006. Springer-Verlag. icon icon 

    @InProceedings{ LohmannMSW2006_bpm,
author = {Niels Lohmann and Peter Massuthe and Christian Stahl and Daniela Weinberg},
title = {{Analyzing Interacting BPEL Processes}},
booktitle = {{Business Process Management, 4th International Conference, BPM 2006, Vienna, Austria, September 5-7, 2006, Proceedings}},
year = 2006,
series = {Lecture Notes in Computer Science},
volume = 4102,
pages = {17-32},
month = sep,
publisher = {Springer-Verlag},
editors = {Schahram Dustdar and José Luiz Fiadeiro and Amit Sheth},
abstract = {This paper addresses the problem of analyzing theinteraction between BPEL processes. We present a technology chain that starts out with a BPEL process and transforms it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). A case study demonstrates the value of this technology chain.},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/LohmannMSW2006_bpm.pdf},
url = {http://www.springerlink.com/content/u108j368336r787k/},
keywords = {BPEL-Semantik, BPEL, Services, Operating Guidelines, Matching, Tools4BPEL} 
}

  • Peter Massuthe and Karsten Wolf. An Algorithm for Matching Nondeterministic Services with Operating Guidelines. In Frank Leymann, Wolfgang Reisig, Satish R. Thatte, and Wil M. P. van der Aalst, editors, The Role of Business Processes in Service Oriented Architectures, number 06291 of Dagstuhl Seminar Proceedings, 2006. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany. icon 

    @InProceedings{ MassutheW2006_dagstuhl06291,
author = {Peter Massuthe and Karsten Wolf},
title = {{An Algorithm for Matching Nondeterministic Services with Operating Guidelines}},
editor = {Frank Leymann and Wolfgang Reisig and Satish R. Thatte and {Wil} {M.} {P.} {van} {der} Aalst},
booktitle = {{The Role of Business Processes in Service Oriented Architectures}},
year = {2006},
series = {Dagstuhl Seminar Proceedings},
publisher = {Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany},
number = {06291},
issn = {1862-4405},
optaddress = {Dagstuhl, Germany},
keywords = {Services, Operating Guidelines, Matching},
abstract = {Interorganizational cooperation is more and more organized by the paradigm of services. Service-oriented architectures (SOA) provide a general framework for service interaction. SOA describe three roles of services, the service provider, the service requester, and the service broker, together with the three operations publish, find, and bind. We provide a formal method based on nondeterministic automata to model services and their interaction. In this paper, we restrict ourselves to finite and acyclic automata. We suggest operating guidelines as a convenient and intuitive artifact to realize the publish operation. In our approach, the find operation reduces to a matching problem between the requester's service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlock-free communication. In this paper, matching of deterministic as well as nondeterministic automata with operating guidelines is presented.},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/MassutheW2006_dagstuhl06291.pdf} 


}

  • Wolfgang Reisig. Abstract State Machines for the Classroom, The Basics. In , Mai 2006. Note: To appear:. icon 

    @InProceedings{ Reisig2006_classroom,
author = {Wolfgang Reisig},
title = {{Abstract State Machines for the Classroom, The Basics}},
year = {2006},
month = {Mai},
note = {to appear:},
keywords = {ASM},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Reisig2006_classroom.pdf} 


}

  • Wolfgang Reisig, Dirk Fahland, Niels Lohmann, Peter Massuthe, Christian Stahl, Daniela Weinberg, Karsten Wolf, and Kathrin Kaschner. Analysis Techniques for Service Models. In Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006 (ISoLA 2006), 15-19 November 2006, Paphos, Cyprus, pages 11-17, November 2006. IEEE Computer Society. icon icon 

    @inproceedings{ReisigFLMSWWK_2006_isola,
Author = {Wolfgang Reisig and Dirk Fahland and Niels Lohmann and Peter Massuthe and Christian Stahl and Daniela Weinberg and Karsten Wolf and Kathrin Kaschner},
Booktitle = {Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006 (ISoLA 2006), 15-19 November 2006, Paphos, Cyprus},
Month = nov,
Pages = {11-17},
url = {http://dx.doi.org/10.1109/ISoLA.2006.58},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/ReisigFLMSWWK2006_atfsm.pdf},
Publisher = {IEEE Computer Society},
Title = {Analysis Techniques for Service Models},
Year = 2006,
Abstract = {The paradigm of Service-Oriented Computing (SOC) provides a framework for interorganizational business processes and for the emerging programming-in-the-large. The basic idea of SOC, the interaction of services, rises a lot of issues such as proper termination of interacting services or substitution of a service by another one. Such issues can be addressed by means of models of services. We show how services can intelligibly be modeled, and we present algorithms and tools to analyze properties of service models. To make sure that our models properly reflect real world issues of services, we model and investigate services represented in established languages such as WS-BPEL.}
}

  • Stephan Roch and Karsten Schmidt. On the step explosion problem. In Susanna Donatelli and P. S. Thiagarajan, editors, Petri Nets and Other Models of Concurrency - ICATPN 2006, 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, Turku, Finland, June 26-30, 2006, Proceedings, volume 4024 of Lecture Notes in Computer Science, pages 342-361, 2006. Springer. icon 

    @InProceedings{ RochS2006_icatpn,
author = {Stephan Roch and Karsten Schmidt},
title = {{On the step explosion problem}},
editor = {Susanna Donatelli and P. S. Thiagarajan},
booktitle = {{Petri Nets and Other Models of Concurrency - ICATPN 2006, 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, Turku, Finland, June 26-30, 2006, Proceedings}},
year = 2006,
series = {Lecture Notes in Computer Science},
volume = 4024,
pages = {342-361},
publisher = {Springer},
isbn = {3-540-34699-6},
url = {http://www.springerlink.com/content/nwv80u740x43212v/} 
}

Technische Berichte

  • Andreas Glausch and Wolfgang Reisig. Distributed Abstract State Machines and Their Expressive Power. Informatik-Berichte 196, Humboldt-Universität zu Berlin, January 2006. icon 

    @TechReport{ GlauschR2006_hub_tr196,
author = {Andreas Glausch and Wolfgang Reisig},
title = {{Distributed Abstract State Machines and Their Expressive Power}},
institution = {Humboldt-Universit{\"{a}}t zu Berlin},
year = 2006,
type = {Informatik-Berichte},
number = 196,
month = jan,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/GlauschR2006_hub_tr196.pdf},
keywords = {ASM},
abstract = {Gurevich's sequential Abstract State Machines (ASMs)are taken as a basis for the construction of distributed ASMs as sets of sequential ASMs. A theorem on the expressive power of distributed ASMs is proven in analogy to Gurevich's classical theorem on the expressive power of sequential ASMs.} 
}

  • Andreas Glausch and Wolfgang Reisig. On the Expressive Power of Unbounded-Nondeterministic Abstract State Machines. Informatik-Berichte 211, Humboldt-Universität zu Berlin, December 2006. icon 

    @TechReport{ GlauschR2006_hub_tr211,
author = {Andreas Glausch and Wolfgang Reisig},
title = {{On the Expressive Power of Unbounded-Nondeterministic Abstract State Machines}},
institution = {Humboldt-Universität zu Berlin},
year = 2006,
type = {Informatik-Berichte},
number = 211,
month = dec,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/GlauschR2006_hub_tr211.pdf},
abstract = {Conventional computational models assume a symbolical representation of states. Gurevich's Abstract State Machines (ASMs) take a more liberal position: any mathematical structure may serve as a state. Gurevich characterizes the expressive power of sequential ASMs in a non-trivial theorem: he defines the class of \emph{sequential algorithms} by help of only a few, amazingly general requirements and proves this class to be equivalent to sequential ASMs. Later, this result has been extended to the class of bounded-nondeterministic ASMs. This paper considers the general case of unbounded-nondeterministic 

ASMs: in each step, an unbounded-nondeterministic ASM may choose among infinitely many alternatives. We define the class of unbounded-nondeterministic algorithms by a conservative extension of Gurevich's original requirements to sequential algorithms. We show that this class is equivalent to unbounded-nondeterministic ASMs.} 
}

  • Niels Lohmann, Peter Massuthe, and Karsten Wolf. Operating Guidelines for Finite-State Services. Informatik-Berichte 210, Humboldt-Universität zu Berlin, December 2006. icon 

    @TechReport{ LohmannMW2006_hub_tr210,
author = {Niels Lohmann and Peter Massuthe and Karsten Wolf},
title = {{Operating Guidelines for Finite-State Services}},
institution = {Humboldt-Universität zu Berlin},
year = 2006,
type = {Informatik-Berichte},
number = 210,
month = dec,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/LohmannMW2006_hub_tr210.pdf},
keywords = {Services, Operating Guidelines, Matching, Tools4BPEL},
abstract = {We introduce the concept of an operating guideline for an arbitrary finite-state service P, extending the work of [1, 2] which was restricted to acyclic services. 

An operating guideline gives complete information about how to correctly (in this paper: deadlock-free) communicate with P. It can further be executed or used for service discovery. 

An operating guideline for P is a particular service S that is enriched with annotations. S communicates deadlock-free with P and is able to simulate every other service that communicates deadlock-free with P. The attached annotations give complete information about whether or not a simulated service is deadlock-free, too.} 
}

  • Peter Massuthe and Karsten Wolf. An Algorithm for Matching Nondeterministic Services with Operating Guidelines. Informatik-Berichte 202, Humboldt-Universität zu Berlin, 2006. icon 

    @TechReport{ MassutheW2006_hub_tr202,
author = {Peter Massuthe and Karsten Wolf},
title = {{An Algorithm for Matching Nondeterministic Services with Operating Guidelines}},
institution = {Humboldt-Universität zu Berlin},
year = 2006,
type = {Informatik-Berichte},
number = 202,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/MassutheW2006_hub_tr202.pdf},
keywords = {Services, Operating Guidelines, Matching},
abstract = {Interorganizational cooperation is more and more organizedby the paradigm of services. Service-oriented architectures (SOA) provide a general framework for service interaction. SOA describe three roles of services, the service provider, the service requester, and the service broker, together with the three operations publish, find, and bind. We provide a formal method based on nondeterministic automata to model services and their interaction. In this paper, we restrict ourselves to finite and acyclic automata. We suggest operating guidelines as a convenient and intuitive artifact to realize the publish operation. In our approach, the find operation reduces to a matching problem between the requester's service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlockfree communication. In this paper, matching of deterministic as well as nondeterministic automata with operating guidelines is presented.} 
}

  • Daniela Weinberg. Reduction Rules for Interaction Graphs. Informatik-Berichte 198, Humboldt-Universität zu Berlin, February 2006. icon 

    @TechReport{ Weinberg2006_hub_tr198,
author = {Daniela Weinberg},
title = {{Reduction Rules for Interaction Graphs}},
institution = {Humboldt-Universität zu Berlin},
year = 2006,
type = {Informatik-Berichte},
number = 198,
month = feb,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Weinberg2006_hub_tr198.pdf},
abstract = {The internet today has grown to be more than just being a basis for 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. That means, we study whether a controller can actually use the functionality provided by the 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 shown in this paper are implemented and have been integrated into an analysis tool kit for web services.} 
}

Studien- und Diplomarbeiten

  • Jan Bretschneider. Modellierung und Synthese eines geschwindigkeitsinvarianten GALS-Wrappers. Studienarbeit, Humboldt-Universität zu Berlin, February 2006. icon 

    @MastersThesis{ Bretschneider2006_sa,
author = {Jan Bretschneider},
title = {{Modellierung und Synthese eines geschwindigkeitsinvarianten GALS-Wrappers}},
school = {Humboldt-Universität zu Berlin},
year = 2006,
type = {Studienarbeit},
month = feb,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Bretschneider2006_sa.pdf},
keywords = {GALS},
abstract = {Global asynchrone, lokal synchrone (GALS) Systeme vereinen dieVorteile synchroner und asynchroner Schaltungen und mindern zugleich ihre Nachteile. Ein GALS-System besteht aus mehreren lokal synchron arbeitenden Modulen, von denen jedes von einem asynchron arbeitenden Wrapper umhüllt wird. Durch diese Wrapper kommunizieren die Module asynchron miteinander. Das IHP Frankfurt hat auf Grundlage einer informalen Spezifikation einen GALS-Wrapper entwickelt. Erst nachträglich wurde ein formales Modell für diesen Wrapper erstellt und auf Korrektheit überprüft. Dabei wurden Fehler in der Implementierung gefunden und korrigiert. Wir beschreiben den Entwurf eines per Konstruktion korrekten Wrappers, der sich an der Schnittstelle zu seiner Umgebung genauso verhält, wie der Wrapper des IHP. Dazu modellieren wir erst sein Verhalten als Petrinetz und generieren danach aus diesem Modell mit dem Werkzeug petrify eine geschwindigkeitsinvariante Schaltung, die per Konstruktion korrekt arbeitet.} 
}

  • Dirk Fahland. Unfoldings for Timed Automata. Diplomarbeit, Humboldt-Universität zu Berlin, July 2006. icon 

    @MastersThesis{ Fahland2006_da,
author = {Dirk Fahland},
title = {Unfoldings for Timed Automata},
school = {Humboldt-Universit\"{a}t zu Berlin},
year = {2006},
type = {Diplomarbeit},
month = {July},
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Fahland2006_da.pdf},
abstract = {In this thesis we develop a state space reduction technique for networks of timed automata based on unfoldings to alleviate the state space explosion problem due to concurrently enabled actions. For the purpose of verifying a system, standard model checking techniques construct its sequential state space that suffers an exponential growth when applied to distributed systems because of concurrently enabled, independent actions: during the construction of the state space these actions are ordered arbitrarily to simulate concurrency in the sequential model. For untimed systems, state space reduction techniques like stubborn sets that omit the construction of redundant information, and unfoldings that represent concurrent events in a partial order have successfully been applied to alleviate the exponential growth. These techniques apply a simple syntactical criterion to identify independent actions. This criterion is not applicable to networks of timed automata as simple examples show, which renders the existing techniques unapplicable. But networks of timed automata face the state space explosion problem as well which raises the demand for a specific reduction technique for these systems. In this thesis, we consider a special, but practically relevant class of networks of timed automata as a formal model for discrete, distributed, timed systems. We develop a novel technique that constructs a complete, finite representation of such a system's state space. This representation is the complete, finite prefix of an unfolding in which concurrently enabled actions are partially ordered. We show that this technique is capable of reducing the size of the state space by magnitude. We are presently not aware of any state space reduction technique for timed automata with similar results.} 
}

  • Kathrin Kaschner. BDD-basiertes Matching von Services. Diplomarbeit, Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II, March 2006. icon 

    @MastersThesis{ Kaschner2006_da,
author = {Kathrin Kaschner},
title = {{BDD-basiertes Matching von Services}},
school = {Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II},
year = 2006,
type = {Diplomarbeit},
month = mar,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Kaschner2006_da.pdf},
abstract = {Moderne Software-Systeme werden zunehmend nach dem Paradigma der ServiceorientiertenArchitektur (SOA) aus unabhängigen Services zusammengesetzt, die definierte Funktionen zur Verfügung stellen und Nachrichten miteinander austauschen. Eine Möglichkeit zur Gewährleistung der reibungslosen Kommunikation besteht in der Bereitstellung einer Bedienungsanleitung durch den Service Provider, mit der der Service Broker anhand eines Prüfverfahrens - dem Matching - entscheiden kann, ob der Service eines Service Requesters zu dem angebotenen Service passt. Für die praktische Anwendung müssen Bedienungsanleitungen in geeigneter Weise kodiert werden. In der vorliegenden Arbeit werden dazu Binäre Entscheidungsdiagramme (BDDs) genutzt. Für das Matching wird der Service des Service Requesters durch einen Serviceautomaten modelliert, der seinerseits ebenfalls in eine BDD-Darstellung überführt wird. Darauf aufbauend wird schließlich ein Matching-Algorithmus entwickelt und seine Korrektheit bewiesen. Die Effizienz der Kodierung durch BDDs und die Funktionsweise des BDD-basierten Matching-Algorithmus wird an Beispielen gezeigt.} 
}

  • Kathrin Kaschner. Repräsentation von Bedienungsanleitungen durch BDDs. Studienarbeit, Humboldt-Universität zu Berlin, January 2006. icon 

    @MastersThesis{ Kaschner2006_sa,
author = {Kathrin Kaschner},
title = {{Repr{\"{a}}sentation von Bedienungsanleitungen durch BDDs}},
school = {Humboldt-Universit{\"{a}}t zu Berlin},
year = 2006,
type = {Studienarbeit},
month = jan,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Kaschner2006_sa.pdf} 


}

  • Jens Kleine. Abstrakte Petrinetzmuster für BPEL unter Bewahrung von Verklemmungen. Studienarbeit, Humboldt-Universität zu Berlin, October 2006. icon 

    @MastersThesis{ Kleine2006_sa,
author = {Jens Kleine},
title = {{Abstrakte Petrinetzmuster für BPEL unter Bewahrung von Verklemmungen}},
school = {Humboldt-Universität zu Berlin},
year = 2006,
type = {Studienarbeit},
month = oct,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Kleine2006_sa.pdf},
keywords = {BPEL, BPEL-Semantik},
abstract = {Wir präsentieren die Reduktion einer Petrinetzsemantik für die Business Process Execution Language for Web Services, die alle Verklemmungen bewahrt und dabei die Petrinetzmuster so stark verkleinert, dass Model-Checking größerer Geschäftsprozesse ermöglicht wird. Dies geschieht, indem wir jedes Petrinetzmuster einzeln betrachten und verkleinern. Bisherige Versuche der computergestützten Analyse scheiterten auf Grund der Größe und Komplexität der entstandenen Petrinetze.} 
}

  • Peter Laufer. Grundlagen für die Anpassung der Petrinetz-Semantik an WS-BPEL 2.0. Studienarbeit, Humboldt-Universität zu Berlin, May 2006. icon 

    @MastersThesis{ Laufer2006_sa,
author = {Peter Laufer},
title = {{Grundlagen für die Anpassung der Petrinetz-Semantik an WS-BPEL 2.0}},
school = {Humboldt-Universität zu Berlin},
year = 2006,
type = {Studienarbeit},
month = may,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Laufer2006_sa.pdf},
keywords = {BPEL, BPEL-Semantik},
abstract = {Die Business Process Execution Language for Web Services (BPEL) ist eine Sprache zur Definitionvon Geschäftsprozessen als Web Services. Um Eigenschaften eines BPEL-Prozesses verifizieren zu können, entwickelte Stahl eine Transformation von BPEL4WS 1.1 in Petrinetze. Als Ergebnis des Standardisierungsprozesses von BPEL wird demnächst die Version WS-BPEL 2.0 verabschiedet werden. Da auch WS-BPEL 2.0 eine textuelle informelle Spezifikation zugrunde liegen wird, wäre eine angepasste Petrinetz-Semantik für Verifikationszwecke weiterhin sehr hilfreich. Ziel dieser Arbeit ist es deshalb, die nderungen von WS-BPEL 2.0 im Vergleich zum Vorgänger BPEL4WS 1.1 zu dokumentieren und Vorschläge in Bezug auf die Anpassung der vorhandenen Petrinetz-Semantik zu geben. Die Betrachtungen beziehen sich dabei auf eine Entwurfsfassung der kommenden Spezifikation von WS-BPEL 2.0 vom 16. März 2006.} 
}

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

Theorie der Programmierung | Kontakt | XHTML 1.0 | Wed Nov 5 08:30:01 2008