TY - THES A1 - Kluth, Stephan T1 - Quantitative modeling and analysis with FMC-QE T1 - Quantitative Modellierung und Analyse mit FMC-QE N2 - The modeling and evaluation calculus FMC-QE, the Fundamental Modeling Concepts for Quanti-tative Evaluation [1], extends the Fundamental Modeling Concepts (FMC) for performance modeling and prediction. In this new methodology, the hierarchical service requests are in the main focus, because they are the origin of every service provisioning process. Similar to physics, these service requests are a tuple of value and unit, which enables hierarchical service request transformations at the hierarchical borders and therefore the hierarchical modeling. Through reducing the model complexity of the models by decomposing the system in different hierarchical views, the distinction between operational and control states and the calculation of the performance values on the assumption of the steady state, FMC-QE has a scalable applica-bility on complex systems. According to FMC, the system is modeled in a 3-dimensional hierarchical representation space, where system performance parameters are described in three arbitrarily fine-grained hierarchi-cal bipartite diagrams. The hierarchical service request structures are modeled in Entity Relationship Diagrams. The static server structures, divided into logical and real servers, are de-scribed as Block Diagrams. The dynamic behavior and the control structures are specified as Petri Nets, more precisely Colored Time Augmented Petri Nets. From the structures and pa-rameters of the performance model, a hierarchical set of equations is derived. The calculation of the performance values is done on the assumption of stationary processes and is based on fundamental laws of the performance analysis: Little's Law and the Forced Traffic Flow Law. Little's Law is used within the different hierarchical levels (horizontal) and the Forced Traffic Flow Law is the key to the dependencies among the hierarchical levels (vertical). This calculation is suitable for complex models and allows a fast (re-)calculation of different performance scenarios in order to support development and configuration decisions. Within the Research Group Zorn at the Hasso Plattner Institute, the work is embedded in a broader research in the development of FMC-QE. While this work is concentrated on the theoretical background, description and definition of the methodology as well as the extension and validation of the applicability, other topics are in the development of an FMC-QE modeling and evaluation tool and the usage of FMC-QE in the design of an adaptive transport layer in order to fulfill Quality of Service and Service Level Agreements in volatile service based environments. This thesis contains a state-of-the-art, the description of FMC-QE as well as extensions of FMC-QE in representative general models and case studies. In the state-of-the-art part of the thesis in chapter 2, an overview on existing Queueing Theory and Time Augmented Petri Net models and other quantitative modeling and evaluation languages and methodologies is given. Also other hierarchical quantitative modeling frameworks will be considered. The description of FMC-QE in chapter 3 consists of a summary of the foundations of FMC-QE, basic definitions, the graphical notations, the FMC-QE Calculus and the modeling of open queueing networks as an introductory example. The extensions of FMC-QE in chapter 4 consist of the integration of the summation method in order to support the handling of closed networks and the modeling of multiclass and semaphore scenarios. Furthermore, FMC-QE is compared to other performance modeling and evaluation approaches. In the case study part in chapter 5, proof-of-concept examples, like the modeling of a service based search portal, a service based SAP NetWeaver application and the Axis2 Web service framework will be provided. Finally, conclusions are given by a summary of contributions and an outlook on future work in chapter 6. [1] Werner Zorn. FMC-QE - A New Approach in Quantitative Modeling. In Hamid R. Arabnia, editor, Procee-dings of the International Conference on Modeling, Simulation and Visualization Methods (MSV 2007) within WorldComp ’07, pages 280 – 287, Las Vegas, NV, USA, June 2007. CSREA Press. ISBN 1-60132-029-9. N2 - FMC-QE (Fundamental Modeling Concepts for Quantitative Evaluation [1]) ist eine auf FMC, den Fundamental Modeling Concepts, basierende Methodik zur Modellierung des Leistungsverhaltens von Systemen mit einem dazugehörenden Kalkül zur Erstellung von Leistungsvorhersagen wie Antwortzeiten und Durchsatz. In dieser neuen Methodik steht die Modellierung der hierarchischen Bedienanforderungen im Mittelpunkt, da sie der Ursprung aller dienstbasierenden Systeme sind. Wie in der Physik sind in FMC-QE die Bedienanforderungen Tupel aus Wert und Einheit, um Auftragstransformationen an Hierarchiegrenzen zu ermöglichen. Da die Komplexität durch eine Dekomposition in mehreren Sichten und in verschiedene hierarchische Schichten, die Unterscheidung von Operations- und Kontrollzuständen, sowie dazugehörige Berechungen unter Annahme der Stationarität reduziert wird, skaliert die Anwendbarkeit von FMC-QE auf komplexe Systeme. Gemäß FMC wird das zu modellierende System in einem 3-dimensionalen hierarchischen Beschreibungsraum dargestellt. Die quantitativen Kenngrößen der Systeme werden in drei beliebig frei-granularen hierarchischen bi-partiten Graphen beschrieben. Die hierarchische Struktur der Bedienanforderungen wird in Entity Relationship Diagrammen beschrieben. Die statischen Bedienerstrukturen, unterteilt in logische und reale Bediener, sind in Aufbaudiagrammen erläutert. Außerdem werden Petri Netze, genauer Farbige Zeit-behaftete Petri Netze, dazu verwendet, die dynamischen Abläufe, sowie die Kontrollflüsse im System zu beschreiben. Anschließend wird eine Menge von hierarchischen Gleichungen von der Struktur und den Parametern des Modells abgeleitet. Diese Gleichungen, die auf dem stationären Zustand des Systems beruhen, basieren auf den beiden Fundamental Gesetzen der Leistungsanalyse, dem Gesetz von Little und dem Verkehrsflussgesetz. Das Gesetz von Little definiert hierbei Beziehungen innerhalb einer hierarchischen Schicht (horizontal) und das Verkehrsflussgesetz wiederum Beziehungen zwischen hierarchischen Schichten (vertikal). Die Berechungen erlauben Leistungsvorhersagen für komplexe Systeme durch eine effiziente Berechnung von Leistungsgrößen für eine große Auswahl von System- und Lastkonfigurationen. Innerhalb der Forschungsgruppe von Prof. Dr.-Ing Werner Zorn am Hasso Plattner Institut an der Universität Potsdam ist die vorliegende Arbeit in einen größeren Forschungskontext im Bereich FMC-QE eingebettet. Während hier ein Fokus auf dem theoretischen Hintergrund, der Beschreibung und der Definition der Methodik als auch der Anwendbarkeit und Erweiterung gelegt wurde, sind andere Arbeiten auf dem Gebiet der Entwicklung einer Anwendung zur Modellierung und Evaluierung von Systemen mit FMC-QE bzw. der Verwendung von FMC-QE zur Entwicklung einer adaptiven Transportschicht zur Einhaltung von Dienstgüten (Quality of Service) und Dienstvereinbarungen (Service Level Agreements) in volatilen dienstbasierten Systemen beheimatet. Diese Arbeit umfasst einen Einblick in den Stand der Technik, die Beschreibung von FMC-QE sowie die Weiterentwicklung von FMC-QE in repräsentativen allgemeinen Modellen und Fallstudien. Das Kapitel 2: Stand der Technik gibt einen Überblick über die Warteschlangentheorie, Zeit-behaftete Petri Netze, weitere Leistungsbeschreibungs- und Leistungsvorhersagungstechniken sowie die Verwendung von Hierarchien in Leistungsbeschreibungstechniken. Die Beschreibung von FMC-QE in Kapitel 3 enthält die Erläuterung der Grundlagen von FMC-QE, die Beschreibung einiger Grundannahmen, der graphischen Notation, dem mathematischen Modell und einem erläuternden Beispiel. In Kapitel 4: Erweiterungen von FMC-QE wird die Behandlung weiterer allgemeiner Modelle, wie die Modellklasse von geschlossenen Netzen, Synchronisierung und Mehrklassen-Modelle beschrieben. Außerdem wird FMC-QE mit dem Stand der Technik verglichen. In Kapitel 5 werden Machbarkeitsstudien beschrieben. Schließlich werden in Kapitel 6 eine Zusammenfassung und ein Ausblick gegeben. [1] Werner Zorn. FMC-QE - A New Approach in Quantitative Modeling. In Hamid R. Arabnia, editor, Proceedings of the International Conference on Modeling, Simulation and Visualization Methods (MSV 2007) within WorldComp ’07, 280 – 287, Las Vegas, NV, USA, Juni 2007. CSREA Press. ISBN 1-60132-029-9. KW - FMC-QE KW - Quantitative Modellierung KW - Leistungsvorhersage KW - Warteschlangentheorie KW - Zeitbehaftete Petri Netze KW - FMC-QE KW - Quantitative Modeling KW - Performance Prediction KW - Queuing Theory KW - Time Augmented Petri Nets Y1 - 2011 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-52987 ER - TY - THES A1 - Off, Thomas T1 - Durchgängige Verfolgbarkeit im Vorfeld der Softwareentwicklung von E-Government-Anwendungen : ein ontologiebasierter und modellgetriebener Ansatz am Beispiel von Bürgerdiensten T1 - Continuous pre-requirements specification traceability for e-government : ontology based and model driven approach using the example of citizen services N2 - Die öffentliche Verwaltung setzt seit mehreren Jahren E-Government-Anwendungssysteme ein, um ihre Verwaltungsprozesse intensiver mit moderner Informationstechnik zu unterstützen. Da die öffentliche Verwaltung in ihrem Handeln in besonderem Maße an Recht und Gesetz gebunden ist verstärkt und verbreitet sich der Zusammenhang zwischen den Gesetzen und Rechtsvorschriften einerseits und der zur Aufgabenunterstützung eingesetzten Informationstechnik andererseits. Aus Sicht der Softwaretechnik handelt es sich bei diesem Zusammenhang um eine spezielle Form der Verfolgbarkeit von Anforderungen (engl. Traceability), die so genannte Verfolgbarkeit im Vorfeld der Anforderungsspezifikation (Pre-Requirements Specification Traceability, kurz Pre-RS Traceability), da sie Aspekte betrifft, die relevant sind, bevor die Anforderungen in eine Spezifikation eingeflossen sind (Ursprünge von Anforderungen). Der Ansatz dieser Arbeit leistet einen Beitrag zur Verfolgbarkeit im Vorfeld der Anforderungsspezifikation von E-Government-Anwendungssystemen. Er kombiniert dazu aktuelle Entwicklungen und Standards (insbesondere des World Wide Web Consortium und der Object Management Group) aus den Bereichen Verfolgbarkeit von Anforderungen, Semantic Web, Ontologiesprachen und modellgetriebener Softwareentwicklung. Der Lösungsansatz umfasst eine spezielle Ontologie des Verwaltungshandeln, die mit den Techniken, Methoden und Werkzeugen des Semantic Web eingesetzt wird, um in Texten von Rechtsvorschriften relevante Ursprünge von Anforderungen durch Annotationen mit einer definierten Semantik zu versehen. Darauf aufbauend wird das Ontology Definition Metamodel (ODM) verwendet, um die Annotationen als spezielle Individuen einer Ontologie auf Elemente der Unified Modeling Language (UML) abzubilden. Dadurch entsteht ein neuer Modelltyp Pre-Requirements Model (PRM), der das Vorfeld der Anforderungsspezifikation formalisiert. Modelle diesen Typs können auch verwendet werden, um Aspekte zu formalisieren die sich nicht oder nicht vollständig aus dem Text der Rechtsvorschrift ergeben. Weiterhin bietet das Modell die Möglichkeit zum Anschluss an die modellgetriebene Softwareentwicklung. In der Arbeit wird deshalb eine Erweiterung der Model Driven Architecture (MDA) vorgeschlagen. Zusätzlich zu den etablierten Modelltypen Computation Independent Model (CIM), Platform Independent Model (PIM) und Platform Specific Model (PSM) könnte der Einsatz des PRM Vorteile für die Verfolgbarkeit bringen. Wird die MDA mit dem PRM auf das Vorfeld der Anforderungsspezifikation ausgeweitet, kann eine Transformation des PRM in ein CIM als initiale Anforderungsspezifikation erfolgen, indem der MOF Query View Transformation Standard (QVT) eingesetzt wird. Als Teil des QVT-Standards ist die Aufzeichnung von Verfolgbarkeitsinformationen bei Modelltransformationen verbindlich. Um die semantische Lücke zwischen PRM und CIM zu überbrücken, erfolgt analog zum Einsatz des Plattformmodells (PM) in der PIM nach PSM Transformation der Einsatz spezieller Hilfsmodelle. Es kommen dafür die im Projekt "E-LoGo" an der Universität Potsdam entwickelten Referenzmodelle zum Einsatz. Durch die Aufzeichnung der Abbildung annotierter Textelemente auf Elemente im PRM und der Transformation der Elemente des PRM in Elemente des CIM kann durchgängige Verfolgbarkeit im Vorfeld der Anforderungsspezifikation erreicht werden. Der Ansatz basiert auf einer so genannten Verfolgbarkeitsdokumentation in Form verlinkter Hypertextdokumente, die mittels XSL-Stylesheet erzeugt wurden und eine Verbindung zur graphischen Darstellung des Diagramms (z. B. Anwendungsfall-, Klassendiagramm der UML) haben. Der Ansatz unterstützt die horizontale Verfolgbarkeit zwischen Elementen unterschiedlicher Modelle vorwärts- und rückwärtsgerichtet umfassend. Er bietet außerdem vertikale Verfolgbarkeit, die Elemente des gleichen Modells und verschiedener Modellversionen in Beziehung setzt. Über den offensichtlichen Nutzen einer durchgängigen Verfolgbarkeit im Vorfeld der Anforderungsspezifikation (z. B. Analyse der Auswirkungen einer Gesetzesänderung, Berücksichtigung des vollständigen Kontextes einer Anforderung bei ihrer Priorisierung) hinausgehend, bietet diese Arbeit eine erste Ansatzmöglichkeit für eine Feedback-Schleife im Prozess der Gesetzgebung. Stehen beispielsweise mehrere gleichwertige Gestaltungsoptionen eines Gesetzes zur Auswahl, können die Auswirkungen jeder Option analysiert und der Aufwand ihrer Umsetzung in E-Government-Anwendungen als Auswahlkriterium berücksichtigt werden. Die am 16. März 2011 in Kraft getretene Änderung des NKRG schreibt eine solche Analyse des so genannten „Erfüllungsaufwands“ für Teilbereiche des Verwaltungshandelns bereits heute verbindlich vor. Für diese Analyse kann die vorliegende Arbeit einen Ansatz bieten, um zu fundierten Aussagen über den Änderungsaufwand eingesetzter E-Government-Anwendungssysteme zu kommen. N2 - Public administration is using electronic government (e-government) application systems for several years to support their processes more intensive with modern information and communication technology than ever before. This increases and broadens the relationship between law and legislation executed by the administration on the one hand and requirements to e-government application systems used to support administrative execution on the other hand. This relationship is subject matter of pre-requirements specification traceability (pre-RS traceability). This work introduces an approach to pre-RS traceabiliy for e-government application. It combines research efforts and standards (i.e. of World Wide Web Consortium and Object Management Group) from different fields: traceability, semantic web, ontology engineering and model driven software engineering. Using this approach it is possible to add a semantic to elements of law and legislation texts using annotations. Annotation semantics is based on an ontology of public administration execution developed especially for this approach. A mapping from annotated text elements as a special kind of ontology individuals to elements of Unified Modeling Language (UML) is created using the Ontology Definition Metamodel (ODM). This mapping results in a new model type referred to as Pre-Requirements Model (PRM). This model uses elements that exist before requirements are explicitly documented in a requirements specification. Therefore it can be primary used to formalize elements and their relationships in the pre-requirements scope. Through the mapping rules of ODM it keeps a traceable relationship from each model element to its corresponding annotated text elements. PRM can also be used to model and refine elements that are not or not completely derived directly from text of law and legislation. In this work is argued that Model Driven Architecture (MDA) might profit from extending the existing model types Computation Independent Model (CIM), Platform Independent Model (PIM) and Platform Specific Model (PSM) by using a PRM. This extension leads to an Architecture that starts with a pre-requirements viewpoint before any requirements are formalized and documented in models of type CIM. It offers also the opportunity to use model transformation to create an initial CIM from PRM by allying the MOF Query View Transformation standard (QVT). Using QVT ensures the traceability of model transformation because standard enforces recording of traceability information. A Transformation from PRM to CIM creates an initial requirements specification that can be refined using common techniques, methods and tools. To bridge the semantic gap between PRM and CIM the approach follows the pattern of PIM to PSM transformation which uses the Platform Model (PM). Analogues PRM to CIM transformation uses special reference models for e-government developed in the project "E-LoGo" at university of Potsdam. By recoding traces of mapping annotation to elements in PRM and transforming elements of PRM to elements in CIM using reference models continuous pre-RS traceability can be achieved. The approach uses simple Extensible Stylesheet Language Transformations (XSLT) to create a hypertext documentation that links all relevant elements. Navigating along these links makes it possible for example to start with an annotated element of a law text and follow to all resulting requirements in a CIM. Using the opposite direction it is possible to see for each requirement from which text element of a law it is derived or even if there is no relation to law. By integrating the graphical representation of a model element this navigation can even start directly in a UML diagram. This illustrates that the approach offers vertical and horizontal traceability in forward and backward direction. Besides the obvious use cases continuous pre-requirements specification traceability offers in general (i.e. impact analysis on changes of law and legislation, consider context of a requirements when prioritizing them) is also offers the chance to create a feedback on the consequences of a change in law to existing e-government systems. As long as alternatives and the necessary scope in legislative process are still left, a feedback can be used to choose an alternative with less effort or faster implementation. For federal law it is in Germany since 2011 obligatory to make a similar estimation referred to as achievement effort (“Erfüllungsaufwand”). This work contributes to the first step of making a solid estimation of this kind of effort using pre-RS traceability. KW - Modellgetriebene Architektur KW - Pre-RS Traceability KW - Ontologie KW - semantisches Netz KW - Model Driven Architecture KW - Pre-RS Traceability KW - Ontology KW - Semantic Web Y1 - 2011 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-57478 ER - TY - THES A1 - Thiele, Sven T1 - Modeling biological systems with Answer Set Programming T1 - Modellierung biologischer Systeme mit Answer Set Programming N2 - Biology has made great progress in identifying and measuring the building blocks of life. The availability of high-throughput methods in molecular biology has dramatically accelerated the growth of biological knowledge for various organisms. The advancements in genomic, proteomic and metabolomic technologies allow for constructing complex models of biological systems. An increasing number of biological repositories is available on the web, incorporating thousands of biochemical reactions and genetic regulations. Systems Biology is a recent research trend in life science, which fosters a systemic view on biology. In Systems Biology one is interested in integrating the knowledge from all these different sources into models that capture the interaction of these entities. By studying these models one wants to understand the emerging properties of the whole system, such as robustness. However, both measurements as well as biological networks are prone to considerable incompleteness, heterogeneity and mutual inconsistency, which makes it highly non-trivial to draw biologically meaningful conclusions in an automated way. Therefore, we want to promote Answer Set Programming (ASP) as a tool for discrete modeling in Systems Biology. ASP is a declarative problem solving paradigm, in which a problem is encoded as a logic program such that its answer sets represent solutions to the problem. ASP has intrinsic features to cope with incompleteness, offers a rich modeling language and highly efficient solving technology. We present ASP solutions, for the analysis of genetic regulatory networks, determining consistency with observed measurements and identifying minimal causes for inconsistency. We extend this approach for computing minimal repairs on model and data that restore consistency. This method allows for predicting unobserved data even in case of inconsistency. Further, we present an ASP approach to metabolic network expansion. This approach exploits the easy characterization of reachability in ASP and its various reasoning methods, to explore the biosynthetic capabilities of metabolic reaction networks and generate hypotheses for extending the network. Finally, we present the BioASP library, a Python library which encapsulates our ASP solutions into the imperative programming paradigm. The library allows for an easy integration of ASP solution into system rich environments, as they exist in Systems Biology. N2 - In den letzten Jahren wurden große Fortschritte bei der Identifikation und Messung der Bausteine des Lebens gemacht. Die Verfügbarkeit von Hochdurchsatzverfahren in der Molekularbiology hat das Anwachsen unseres biologischen Wissens dramatisch beschleunigt. Durch die technische Fortschritte in Genomic, Proteomic und Metabolomic wurde die Konstruktion komplexer Modelle biologischer Systeme ermöglicht. Immer mehr biologische Datenbanken sind über das Internet verfügbar, sie enthalten tausende Daten biochemischer Reaktionen und genetischer Regulation. System Biologie ist ein junger Forschungszweig der Biologie, der versucht Biologische Systeme in ihrer Ganzheit zu erforschen. Dabei ist man daran interessiert möglichst viel Wissen aus den unterschiedlichsten Bereichen in ein Modell zu aggregieren, welches das Zusammenwirken der verschiedensten Komponenten nachbildet. Durch das Studium derartiger Modelle erhofft man sich ein Verständnis der aufbauenden Eigenschaften, wie zum Beispiel Robustheit, des Systems zu erlangen. Es stellt sich jedoch die Problematik, das sowohl die biologischen Modelle als auch die verfügbaren Messwerte, oft unvollständig, miteinander unvereinbar oder fehlerhaft sind. All dies macht es schwierig biologisch sinnvolle Schlussfolgerungen zu ziehen. Daher, möchten wir in dieser Arbeit Antwortmengen Programmierung (engl. Answer Set Programming; ASP) als Werkzeug zur diskreten Modellierung system biologischer Probleme vorschlagen. ASP verfügt über eingebaute Eigenschaften zum Umgang mit unvollständiger Information, eine reichhaltige Modellierungssprache und hocheffiziente Berechnungstechniken. Wir präsentieren ASP Lösungen zur Analyse von Netzwerken genetischer Regulierungen, zur Prüfung der Konsistenz mit gemessene Daten, und zur Identifikation von Gründen für Inkonsistenz. Diesen Ansatz erweitern wir um die Möglichkeit zur Berechnung minimaler Reparaturen an Modell und Daten, welche Konsistenz erzeugen. Mithilfe dieser Methode werden wir in die Lage versetzt, auch im Fall von Inkonsistenz, noch ungemessene Daten vorherzusagen. Weiterhin, präsentieren wir einen ASP Ansatz zur Analyse metabolischer Netzwerke. Bei diesem Ansatz, nutzen wir zum einen aus das sich Erreichbarkeit mit ASP leicht spezifizieren lässt und das ASP mehrere mächtige Methoden zur Schlussfolgerung bereitstellt, welche sich auch kombiniert lassen. Dadurch wird es möglich die Synthese Möglichkeiten eines Metabolischen Netzwerks zu erforschen und Hypothesen für Erweiterungen des metabolischen Netzwerks zu berechnen. Zu guter Letzt, präsentieren wir die BioASP Softwarebibliothek. Die BioASP-Bibliothek kapselt unsere ASP Lösungen in das imperative Programmierparadigma und vereinfacht eine Integration von ASP Lösungen in heterogene Betriebsumgebungen, wie sie in der System Biologie vorherrschen. KW - Antwortmengen Programmierung KW - System Biologie KW - Inkonsistenz KW - Unvollständigkeit KW - Reparatur KW - answer set programming KW - systems biology KW - inconsistency KW - incompleteness KW - repair Y1 - 2011 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-59383 ER - TY - THES A1 - Bordihn, Henning T1 - Contributions to the syntactical analysis beyond context-freeness T1 - Beiträge zur syntaktischen Analyse nicht-kontextfreier Sprachen N2 - Parsability approaches of several grammar formalisms generating also non-context-free languages are explored. Chomsky grammars, Lindenmayer systems, grammars with controlled derivations, and grammar systems are treated. Formal properties of these mechanisms are investigated, when they are used as language acceptors. Furthermore, cooperating distributed grammar systems are restricted so that efficient deterministic parsing without backtracking becomes possible. For this class of grammar systems, the parsing algorithm is presented and the feature of leftmost derivations is investigated in detail. N2 - Ansätze zum Parsing verschiedener Grammatikformalismen, die auch nicht-kontextfreie Sprachen erzeugen können, werden diskutiert. Chomsky-Grammatiken, Lindenmayer-Systeme, Grammatiken mit gesteuerten Ersetzungen und Grammatiksysteme werden behandelt. Formale Eigenschaften dieser Mechanismen als Akzeptoren von Sprachen werden untersucht. Weiterhin werden kooperierende verteilte (CD) Grammatiksysteme derart beschränkt, dass effizientes deterministisches Parsing ohne Backtracking möglich ist. Für diese Klasse von Grammatiksystemen wird der Parsingalgorithmus vorgestellt und die Rolle von Linksableitungen wird detailliert betrachtet. KW - Parsing KW - Akzeptierende Grammatiken KW - Gesteuerte Ableitungen KW - Grammatiksysteme KW - Linksableitungen KW - Parsing KW - Accepting Grammars KW - Controlled Derivations KW - Grammar Systems KW - Leftmost Derivations Y1 - 2011 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-59719 ER - TY - VIDEO A1 - Kujath, Bertold T1 - Keine Angst vor Informatikproblemen BT - Hochleistern über die Schulter geschaut N2 - Dieses Lehrvideo zeigt aus der Perspektive einer Übertischkamera den fiktiven informatischen Hochleister Tom bei der Bearbeitung eines schwierigen Färbeproblems. Dabei kann man die fortlaufend von ihm angefertigten Skizzen beobachten und seine Gedankengänge genau verfolgen. Denn dieser Problemlöser arbeitet unter lautem Denken, d. h. er spricht alle seine Gedankengänge laut aus. Man kann zuschauen, wie Tom zunächst die Aufgabe analysiert und die dadurch gewonnenen Erkenntnisse in der anschließenden Problembearbeitung gewinnbringend einsetzt. Der Zuschauer wird dabei aber nicht allein gelassen. An markanten Stellen wird das Video unterbrochen und Toms zurückliegende Aktivitäten mit animierten Bildsequenzen vertiefend erläutert. Schwache Problemlöser können so die in Unterricht oder Vorlesung vermittelten Kenntnisse über informatische Problemlösemethoden vertiefen und deren Anwendung durch einen starken Problemlöser beispielhaft miterleben. Entstanden ist dieses Video aus einer Vergleichsstudie mit starken und schwachen Problemlösern. Die effizienten Methoden der Hochleister wurden didaktisch aufgearbeitet und zu einem modellhaften Problemlöseprozess zusammengesetzt. Der wissenschaftliche Hintergrund des Lehrvideos wird durch eine als Bildergeschichte erzählte Rahmenhandlung verdeutlicht. Bei Erstsemesterstudenten der Informatik, denen dieses Video zur Bewertung vorgespielt wurde, fand dieses Konzept große Zustimmung. Tenor: Unterhaltsam und lehrreich zugleich. KW - Graphfärbung KW - Theoretische Informatik KW - Problemlösen Y1 - 2011 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-326380 SN - 978-3-86956-150-9 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - THES A1 - Mühlbauer, Felix T1 - Entwurf, Methoden und Werkzeuge für komplexe Bildverarbeitungssysteme auf Rekonfigurierbaren System-on-Chip-Architekturen T1 - Design, methodologies and tools for complex image processing systems on reconfigurable system-on-chip-architectures N2 - Bildverarbeitungsanwendungen stellen besondere Ansprüche an das ausführende Rechensystem. Einerseits ist eine hohe Rechenleistung erforderlich. Andererseits ist eine hohe Flexibilität von Vorteil, da die Entwicklung tendentiell ein experimenteller und interaktiver Prozess ist. Für neue Anwendungen tendieren Entwickler dazu, eine Rechenarchitektur zu wählen, die sie gut kennen, anstatt eine Architektur einzusetzen, die am besten zur Anwendung passt. Bildverarbeitungsalgorithmen sind inhärent parallel, doch herkömmliche bildverarbeitende eingebettete Systeme basieren meist auf sequentiell arbeitenden Prozessoren. Im Gegensatz zu dieser "Unstimmigkeit" können hocheffiziente Systeme aus einer gezielten Synergie aus Software- und Hardwarekomponenten aufgebaut werden. Die Konstruktion solcher System ist jedoch komplex und viele Lösungen, wie zum Beispiel grobgranulare Architekturen oder anwendungsspezifische Programmiersprachen, sind oft zu akademisch für einen Einsatz in der Wirtschaft. Die vorliegende Arbeit soll ein Beitrag dazu leisten, die Komplexität von Hardware-Software-Systemen zu reduzieren und damit die Entwicklung hochperformanter on-Chip-Systeme im Bereich Bildverarbeitung zu vereinfachen und wirtschaftlicher zu machen. Dabei wurde Wert darauf gelegt, den Aufwand für Einarbeitung, Entwicklung als auch Erweiterungen gering zu halten. Es wurde ein Entwurfsfluss konzipiert und umgesetzt, welcher es dem Softwareentwickler ermöglicht, Berechnungen durch Hardwarekomponenten zu beschleunigen und das zu Grunde liegende eingebettete System komplett zu prototypisieren. Hierbei werden komplexe Bildverarbeitungsanwendungen betrachtet, welche ein Betriebssystem erfordern, wie zum Beispiel verteilte Kamerasensornetzwerke. Die eingesetzte Software basiert auf Linux und der Bildverarbeitungsbibliothek OpenCV. Die Verteilung der Berechnungen auf Software- und Hardwarekomponenten und die daraus resultierende Ablaufplanung und Generierung der Rechenarchitektur erfolgt automatisch. Mittels einer auf der Antwortmengenprogrammierung basierten Entwurfsraumexploration ergeben sich Vorteile bei der Modellierung und Erweiterung. Die Systemsoftware wird mit OpenEmbedded/Bitbake synthetisiert und die erzeugten on-Chip-Architekturen auf FPGAs realisiert. N2 - Image processing applications have special requirements to the executing computational system. On the one hand a high computational power is necessary. On the other hand a high flexibility is an advantage because the development tends to be an experimental and interactive process. For new applications the developer tend to choose a computational architecture which they know well instead of using that one which fits best to the application. Image processing algorithms are inherently parallel while common image processing systems are mostly based on sequentially operating processors. In contrast to this "mismatch", highly efficient systems can be setup of a directed synergy of software and hardware components. However, the construction of such systems is complex and lots of solutions, like gross-grained architectures or application specific programming languages, are often too academic for the usage in commerce. The present work should contribute to reduce the complexity of hardware-software-systems and thus increase the economy of and simplify the development of high-performance on-chip systems in the domain of image processing. In doing so, a value was set on keeping the effort low on making familiar to the topic, on development and also extensions. A design flow was developed and implemented which allows the software developer to accelerate calculations with hardware components and to prototype the whole embedded system. Here complex image processing systems, like distributed camera sensor networks, are examined which need an operating system. The used software is based upon Linux and the image processing library OpenCV. The distribution of the calculations to software and hardware components and the resulting scheduling and generation of architectures is done automatically. The design space exploration is based on answer set programming which involves advantages for modelling in terms of simplicity and extensions. The software is synthesized with the help of OpenEmbedded/Bitbake and the generated on-chip architectures are implemented on FPGAs. KW - Bildverarbeitung KW - FPGA KW - on-chip KW - Entwurfsraumexploration KW - Hardware-Software-Co-Design KW - Antwortmengenprogrammierung KW - image processing KW - FPGA KW - on-chip KW - design space exploration KW - hardware-software-codesign KW - answer set programming Y1 - 2011 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-59923 ER - TY - THES A1 - Rabenalt, Thomas T1 - Datenkompaktierung für Diagnose und Test Y1 - 2011 CY - Potsdam ER - TY - THES A1 - AbuJarour, Mohammed T1 - Enriched service descriptions: sources, approaches and usages Y1 - 2011 CY - Potsdam ER - TY - THES A1 - Roschke, Sebastian T1 - Towards high quality security event correlation using in-memory and multi-core processing Y1 - 2011 CY - Potsdam ER - TY - THES A1 - Lübbe, Alexander T1 - Tangible business process modeling : design and evaluation of a process model elicitation Technique Y1 - 2011 CY - Potsdam ER - TY - BOOK A1 - Schubert, Sigrid A1 - Schwill, Andreas T1 - Didaktik der Informatik Y1 - 2011 SN - 978-3-8274-2652-9 PB - Spektrum Akademischer Verlag CY - Heidelberg ER - TY - THES A1 - Quasthoff, Matthias T1 - Effizientes Entwickeln von Semantic-Web-Software mit Object Triple Mapping Y1 - 2011 CY - Potsdam ER - TY - BOOK A1 - Plattner, Hasso A1 - Zeier, Alexander T1 - In-memory data managment : an inflection point for enterprise applications Y1 - 2011 SN - 978-3-642-19362-0 PB - Springer CY - Heidelberg, New York ER - TY - JOUR A1 - Uflacker, Matthias A1 - Kowark, Thomas A1 - Zeier, Alexander T1 - An instrument for real-time design interaction capture Y1 - 2011 SN - 978-3-642-13756-3 ER - TY - JOUR A1 - Luebbe, Alexander A1 - Weske, Mathias T1 - Bringing design thinking to business process modeling Y1 - 2011 SN - 978-3-642-13756-3 ER - TY - JOUR A1 - Hirschfeld, Robert A1 - Steinert, Bastian A1 - Lincke, Jens T1 - Agile software development in virtual collaboration environments Y1 - 2011 SN - 978-3-642-13756-3 ER - TY - JOUR A1 - Gabrysiak, Gregor A1 - Giese, Holger A1 - Seibel, Andreas T1 - Towards next generation design thinking : scenario-based prototyping for designing complex software systems with multiple users Y1 - 2011 SN - 978-3-642-13756-3 ER - TY - THES A1 - Alnemr, Rehab T1 - Reputation object representation model for enabling reputation interoperability Y1 - 2011 CY - Potsdam ER - TY - THES A1 - Schünemann, Björn T1 - The V2X simulation runtime infrastructure: VSimRTI Y1 - 2011 CY - Potsdam ER - TY - THES A1 - Richter, Michael T1 - Anwendung nichtlinearer Codes zur Fehlererkennung und -korrektur Y1 - 2011 CY - Potsdam ER - TY - JOUR A1 - Hocher, Berthold A1 - Heiden, S. A1 - von Websky, Karoline A1 - Rahnenführer, Jörg A1 - Kalk, Philipp A1 - Pfab, T. T1 - Dual endothelin-converting enzyme/neutral endopeptidase blockade in rats with D-galactosamine-induced liver failure JF - European journal of medical research : official organ "Deutsche AIDS-Gesellschaft" N2 - Secondary activation of the endothelin system is thought to be involved in toxic liver injury. This study tested the hypothesis that dual endothelin-converting enzyme / neutral endopeptidase blockade might: be able to attenuate acute toxic liver injury. Male Sprague-Dawley rats were implanted with subcutaneous minipumps to deliver the novel compound SLV338 (10 mg/kg*d) or vehicle. Four days later they received two intraperitoneal injections of D-galactosamine (1.3 g/kg each) or vehicle at an interval of 12 hours. The animals were sacrificed 48 hours after the first injection. Injection of D-galactosamine resulted in very severe liver injury, reflected by strongly elevated plasma liver enzymes, hepatic necrosis and inflammation, and a mortality rate of 42.9 %. SLV338 treatment did not show any significant effect on the extent of acute liver injury as judged from plasma parameters, hepatic histology and mortality. Plasma measurements of SLV338 confirmed adequate drug delivery. Plasma concentrations of big endothelin-1 and endothelin-1 were significantly elevated in animals with liver injury (5-fold and 62-fold, respectively). Plasma endothelin-1 was significantly correlated with several markers of liver injury. SLV338 completely prevented the rise of plasma big endothelin-1 (p<0.05) and markedly attenuated the rise of endothelin-1 (p = 0.055). In conclusion, dual endothelin-converting enzyme / neutral endopeptidase blockade by SLV338 did not significantly attenuate D-galactosamine-induced acute liver injury, although it largely prevented the activation of the endothelin system. An evaluation of SLV338 in a less severe model of liver injury would be of interest, since very severe intoxication might not be relevantly amenable to pharmacological interventions. KW - endothelin KW - endothelin-converting enzyme KW - neutral endopeptidase KW - D-galactosamine KW - acute liver failure Y1 - 2011 SN - 0949-2321 VL - 16 IS - 6 SP - 275 EP - 279 PB - Med. Scientific Publ. Holzapfel CY - München ER - TY - JOUR A1 - Weidlich, Matthias A1 - Mendling, Jan A1 - Weske, Mathias T1 - Efficient consistency measurement based on behavioral profiles of process models JF - IEEE transactions on software engineering N2 - Engineering of process-driven business applications can be supported by process modeling efforts in order to bridge the gap between business requirements and system specifications. However, diverging purposes of business process modeling initiatives have led to significant problems in aligning related models at different abstract levels and different perspectives. Checking the consistency of such corresponding models is a major challenge for process modeling theory and practice. In this paper, we take the inappropriateness of existing strict notions of behavioral equivalence as a starting point. Our contribution is a concept called behavioral profile that captures the essential behavioral constraints of a process model. We show that these profiles can be computed efficiently, i.e., in cubic time for sound free-choice Petri nets w.r.t. their number of places and transitions. We use behavioral profiles for the definition of a formal notion of consistency which is less sensitive to model projections than common criteria of behavioral equivalence and allows for quantifying deviation in a metric way. The derivation of behavioral profiles and the calculation of a degree of consistency have been implemented to demonstrate the applicability of our approach. We also report the findings from checking consistency between partially overlapping models of the SAP reference model. KW - Process model analysis KW - process model alignment KW - behavioral abstraction KW - consistency checking KW - consistency measures Y1 - 2011 U6 - https://doi.org/10.1109/TSE.2010.96 SN - 0098-5589 VL - 37 IS - 3 SP - 410 EP - 429 PB - Inst. of Electr. and Electronics Engineers CY - Los Alamitos ER - TY - JOUR A1 - Mileo, Alessandra A1 - Schaub, Torsten H. A1 - Merico, Davide A1 - Bisiani, Roberto T1 - Knowledge-based multi-criteria optimization to support indoor positioning JF - Annals of mathematics and artificial intelligence N2 - Indoor position estimation constitutes a central task in home-based assisted living environments. Such environments often rely on a heterogeneous collection of low-cost sensors whose diversity and lack of precision has to be compensated by advanced techniques for localization and tracking. Although there are well established quantitative methods in robotics and neighboring fields for addressing these problems, they lack advanced knowledge representation and reasoning capacities. Such capabilities are not only useful in dealing with heterogeneous and incomplete information but moreover they allow for a better inclusion of semantic information and more general homecare and patient-related knowledge. We address this problem and investigate how state-of-the-art localization and tracking methods can be combined with Answer Set Programming, as a popular knowledge representation and reasoning formalism. We report upon a case-study and provide a first experimental evaluation of knowledge-based position estimation both in a simulated as well as in a real setting. KW - Knowledge representation KW - Answer Set Programming KW - Wireless Sensor Networks KW - Localization KW - Tracking Y1 - 2011 U6 - https://doi.org/10.1007/s10472-011-9241-2 SN - 1012-2443 SN - 1573-7470 VL - 62 IS - 3-4 SP - 345 EP - 370 PB - Springer CY - Dordrecht ER - TY - JOUR A1 - Polyvyanyy, Artem A1 - Weidlich, Matthias A1 - Weske, Mathias T1 - Connectivity of workflow nets the foundations of stepwise verification JF - Acta informatica N2 - Behavioral models capture operational principles of real-world or designed systems. Formally, each behavioral model defines the state space of a system, i.e., its states and the principles of state transitions. Such a model is the basis for analysis of the system's properties. In practice, state spaces of systems are immense, which results in huge computational complexity for their analysis. Behavioral models are typically described as executable graphs, whose execution semantics encodes a state space. The structure theory of behavioral models studies the relations between the structure of a model and the properties of its state space. In this article, we use the connectivity property of graphs to achieve an efficient and extensive discovery of the compositional structure of behavioral models; behavioral models get stepwise decomposed into components with clear structural characteristics and inter-component relations. At each decomposition step, the discovered compositional structure of a model is used for reasoning on properties of the whole state space of the system. The approach is exemplified by means of a concrete behavioral model and verification criterion. That is, we analyze workflow nets, a well-established tool for modeling behavior of distributed systems, with respect to the soundness property, a basic correctness property of workflow nets. Stepwise verification allows the detection of violations of the soundness property by inspecting small portions of a model, thereby considerably reducing the amount of work to be done to perform soundness checks. Besides formal results, we also report on findings from applying our approach to an industry model collection. Y1 - 2011 U6 - https://doi.org/10.1007/s00236-011-0137-8 SN - 0001-5903 VL - 48 IS - 4 SP - 213 EP - 242 PB - Springer CY - New York ER - TY - JOUR A1 - Durzinsky, Markus A1 - Marwan, Wolfgang A1 - Ostrowski, Max A1 - Schaub, Torsten H. A1 - Wagler, Annegret T1 - Automatic network reconstruction using ASP JF - Theory and practice of logic programming N2 - Building biological models by inferring functional dependencies from experimental data is an important issue in Molecular Biology. To relieve the biologist from this traditionally manual process, various approaches have been proposed to increase the degree of automation. However, available approaches often yield a single model only, rely on specific assumptions, and/or use dedicated, heuristic algorithms that are intolerant to changing circumstances or requirements in the view of the rapid progress made in Biotechnology. Our aim is to provide a declarative solution to the problem by appeal to Answer Set Programming (ASP) overcoming these difficulties. We build upon an existing approach to Automatic Network Reconstruction proposed by part of the authors. This approach has firm mathematical foundations and is well suited for ASP due to its combinatorial flavor providing a characterization of all models explaining a set of experiments. The usage of ASP has several benefits over the existing heuristic algorithms. First, it is declarative and thus transparent for biological experts. Second, it is elaboration tolerant and thus allows for an easy exploration and incorporation of biological constraints. Third, it allows for exploring the entire space of possible models. Finally, our approach offers an excellent performance, matching existing, special-purpose systems. Y1 - 2011 U6 - https://doi.org/10.1017/S1471068411000287 SN - 1471-0684 VL - 11 SP - 749 EP - 766 PB - Cambridge Univ. Press CY - New York ER - TY - JOUR A1 - Gebser, Martin A1 - Kaminski, Roland A1 - Schaub, Torsten H. T1 - Complex optimization in answer set programming JF - Theory and practice of logic programming N2 - Preference handling and optimization are indispensable means for addressing nontrivial applications in Answer Set Programming (ASP). However, their implementation becomes difficult whenever they bring about a significant increase in computational complexity. As a consequence, existing ASP systems do not offer complex optimization capacities, supporting, for instance, inclusion-based minimization or Pareto efficiency. Rather, such complex criteria are typically addressed by resorting to dedicated modeling techniques, like saturation. Unlike the ease of common ASP modeling, however, these techniques are rather involved and hardly usable by ASP laymen. We address this problem by developing a general implementation technique by means of meta-prpogramming, thus reusing existing ASP systems to capture various forms of qualitative preferences among answer sets. In this way, complex preferences and optimization capacities become readily available for ASP applications. KW - Answer Set Programming KW - Preference Handling KW - Complex optimization KW - Meta-Programming Y1 - 2011 U6 - https://doi.org/10.1017/S1471068411000329 SN - 1471-0684 VL - 11 IS - 3 SP - 821 EP - 839 PB - Cambridge Univ. Press CY - New York ER - TY - INPR A1 - Kröning, Daniel A1 - Margaria, Tiziana A1 - Woodcock, Jim T1 - Untitled T2 - Formal aspects of computing : the international journal of formal methods Y1 - 2011 U6 - https://doi.org/10.1007/s00165-011-0201-8 SN - 0934-5043 VL - 23 IS - 5 SP - 585 EP - 588 PB - Springer CY - New York ER - TY - JOUR A1 - Jörges, Sven A1 - Margaria, Tiziana A1 - Steffen, Bernhard T1 - Assuring property conformance of code generators via model checking JF - Formal aspects of computing : the international journal of formal methods N2 - Automatic code generation is an essential cornerstone of today's model-driven approaches to software engineering. Thus a key requirement for the success of this technique is the reliability and correctness of code generators. This article describes how we employ standard model checking-based verification to check that code generator models developed within our code generation framework Genesys conform to (temporal) properties. Genesys is a graphical framework for the high-level construction of code generators on the basis of an extensible library of well-defined building blocks along the lines of the Extreme Model-Driven Development paradigm. We will illustrate our verification approach by examining complex constraints for code generators, which even span entire model hierarchies. We also show how this leads to a knowledge base of rules for code generators, which we constantly extend by e.g. combining constraints to bigger constraints, or by deriving common patterns from structurally similar constraints. In our experience, the development of code generators with Genesys boils down to re-instantiating patterns or slightly modifying the graphical process model, activities which are strongly supported by verification facilities presented in this article. KW - Extreme Model-Driven Development KW - Code generation KW - Model checking KW - Verification Y1 - 2011 U6 - https://doi.org/10.1007/s00165-010-0169-9 SN - 0934-5043 VL - 23 IS - 5 SP - 589 EP - 606 PB - Springer CY - New York ER - TY - JOUR A1 - Gebser, Martin A1 - Schaub, Torsten H. A1 - Thiele, Sven A1 - Veber, Philippe T1 - Detecting inconsistencies in large biological networks with answer set programming JF - Theory and practice of logic programming N2 - We introduce an approach to detecting inconsistencies in large biological networks by using answer set programming. To this end, we build upon a recently proposed notion of consistency between biochemical/genetic reactions and high-throughput profiles of cell activity. We then present an approach based on answer set programming to check the consistency of large-scale data sets. Moreover, we extend this methodology to provide explanations for inconsistencies by determining minimal representations of conflicts. In practice, this can be used to identify unreliable data or to indicate missing reactions. KW - answer set programming KW - bioinformatics KW - consistency KW - diagnosis Y1 - 2011 U6 - https://doi.org/10.1017/S1471068410000554 SN - 1471-0684 VL - 11 IS - 5-6 SP - 323 EP - 360 PB - Cambridge Univ. Press CY - New York ER - TY - JOUR A1 - Rabenalt, Thomas A1 - Goessel, Michael A1 - Leininger, Andreas T1 - Masking of X-Values by use of a hierarchically configurable register JF - Journal of electronic testing : theory and applications N2 - In this paper we consider masking of unknowns (X-values) for VLSI circuits. We present a new hierarchical method of X-masking which is a major improvement of the method proposed in [4], called WIDE1. By the method proposed, the number of observable scan cells is optimized and data volume for X-masking can be significantly reduced in comparison to WIDEL This is demonstrated for three industrial designs. In cases where all X-values have to be masked the novel approach is especially efficient. KW - Masking of X-values KW - Hierarchically configurable mask register Y1 - 2011 U6 - https://doi.org/10.1007/s10836-010-5179-2 SN - 0923-8174 VL - 27 IS - 1 SP - 31 EP - 41 PB - Springer CY - Dordrecht ER - TY - GEN A1 - Patil, Kaustubh R. A1 - Haider, Peter A1 - Pope, Phillip B. A1 - Turnbaugh, Peter J. A1 - Morrison, Mark A1 - Scheffer, Tobias A1 - McHardy, Alice C. T1 - Taxonomic metagenome sequence assignment with structured output models T2 - Nature methods : techniques for life scientists and chemists Y1 - 2011 U6 - https://doi.org/10.1038/nmeth0311-191 SN - 1548-7091 VL - 8 IS - 3 SP - 191 EP - 192 PB - Nature Publ. Group CY - London ER - TY - JOUR A1 - Bordihn, Henning A1 - Holzer, Markus A1 - Kutrib, Martin T1 - Decidability of operation problems for TOL languages and subclasses JF - Information and computation N2 - We investigate the decidability of the operation problem for TOL languages and subclasses. Fix an operation on formal languages. Given languages from the family considered (OL languages, TOL languages, or their propagating variants), is the application of this operation to the given languages still a language that belongs to the same language family? Observe, that all the Lindenmayer language families in question are anti-AFLs, that is, they are not closed under homomorphisms, inverse homomorphisms, intersection with regular languages, union, concatenation, and Kleene closure. Besides these classical operations we also consider intersection and substitution, since the language families under consideration are not closed under these operations, too. We show that for all of the above mentioned language operations, except for the Kleene closure, the corresponding operation problems of OL and TOL languages and their propagating variants are not even semidecidable. The situation changes for unary OL languages. In this case we prove that the operation problems with respect to Kleene star, complementation, and intersection with regular sets are decidable. KW - L systems KW - Operation problem KW - Decidability KW - Unary languages Y1 - 2011 U6 - https://doi.org/10.1016/j.ic.2010.11.008 SN - 0890-5401 VL - 209 IS - 3 SP - 344 EP - 352 PB - Elsevier CY - San Diego ER - TY - INPR A1 - Rosamond, Frances A1 - Bardohl, Roswitha A1 - Diehl, Stephan A1 - Geisler, Uwe A1 - Bolduan, Gordon A1 - Lessmoellmann, Annette A1 - Schwill, Andreas A1 - Stege, Ulrike T1 - Virtual extension reaching out to the media become a computer science ambassador T2 - Communications of the ACM / Association for Computing Machinery Y1 - 2011 U6 - https://doi.org/10.1145/1897852.1897880 SN - 0001-0782 VL - 54 IS - 3 SP - 113 EP - 116 PB - Association for Computing Machinery CY - New York ER - TY - JOUR A1 - Catchpole, Gareth A1 - Platzer, Alexander A1 - Weikert, Cornelia A1 - Kempkensteffen, Carsten A1 - Johannsen, Manfred A1 - Krause, Hans A1 - Jung, Klaus A1 - Miller, Kurt A1 - Willmitzer, Lothar A1 - Selbig, Joachim A1 - Weikert, Steffen T1 - Metabolic profiling reveals key metabolic features of renal cell carcinoma JF - Journal of cellular and molecular medicine : a journal of translational medicine N2 - Recent evidence suggests that metabolic changes play a pivotal role in the biology of cancer and in particular renal cell carcinoma (RCC). Here, a global metabolite profiling approach was applied to characterize the metabolite pool of RCC and normal renal tissue. Advanced decision tree models were applied to characterize the metabolic signature of RCC and to explore features of metastasized tumours. The findings were validated in a second independent dataset. Vitamin E derivates and metabolites of glucose, fatty acid, and inositol phosphate metabolism determined the metabolic profile of RCC. alpha-tocopherol, hippuric acid, myoinositol, fructose-1-phosphate and glucose-1-phosphate contributed most to the tumour/normal discrimination and all showed pronounced concentration changes in RCC. The identified metabolic profile was characterized by a low recognition error of only 5% for tumour versus normal samples. Data on metastasized tumours suggested a key role for metabolic pathways involving arachidonic acid, free fatty acids, proline, uracil and the tricarboxylic acid cycle. These results illustrate the potential of mass spectroscopy based metabolomics in conjunction with sophisticated data analysis methods to uncover the metabolic phenotype of cancer. Differentially regulated metabolites, such as vitamin E compounds, hippuric acid and myoinositol, provide leads for the characterization of novel pathways in RCC. KW - kidney cancer KW - metabolism KW - metabolomics KW - metastasis Y1 - 2011 U6 - https://doi.org/10.1111/j.1582-4934.2009.00939.x SN - 1582-1838 VL - 15 IS - 1 SP - 109 EP - 118 PB - Wiley-Blackwell CY - Malden ER - TY - JOUR A1 - Gebser, Martin A1 - Lee, Joohyung A1 - Lierler, Yuliya T1 - On elementary loops of logic programs JF - Theory and practice of logic programming N2 - Using the notion of an elementary loop, Gebser and Schaub (2005. Proceedings of the Eighth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'05), 53-65) refined the theorem on loop formulas attributable to Lin and Zhao (2004) by considering loop formulas of elementary loops only. In this paper, we reformulate the definition of an elementary loop, extend it to disjunctive programs, and study several properties of elementary loops, including how maximal elementary loops are related to minimal unfounded sets. The results provide useful insights into the stable model semantics in terms of elementary loops. For a nondisjunctive program, using a graph-theoretic characterization of an elementary loop, we show that the problem of recognizing an elementary loop is tractable. On the other hand, we also show that the corresponding problem is coNP-complete for a disjunctive program. Based on the notion of an elementary loop, we present the class of Head-Elementary-loop-Free (HEF) programs, which strictly generalizes the class of Head-Cycle-Free (HCF) programs attributable to Ben-Eliyahu and Dechter (1994. Annals of Mathematics and Artificial Intelligence 12, 53-87). Like an Ha: program, an HEF program can be turned into an equivalent nondisjunctive program in polynomial time by shifting head atoms into the body. KW - stable model semantics KW - loop formulas KW - unfounded sets Y1 - 2011 U6 - https://doi.org/10.1017/S1471068411000019 SN - 1471-0684 VL - 11 IS - 2 SP - 953 EP - 988 PB - Cambridge Univ. Press CY - New York ER - TY - JOUR A1 - Bordihn, Henning A1 - Kutrib, Martin A1 - Malcher, Andreas T1 - Undecidability and hierarchy results for parallel communicating finite automata JF - International journal of foundations of computer science N2 - Parallel communicating finite automata (PCFAs) are systems of several finite state automata which process a common input string in a parallel way and are able to communicate by sending their states upon request. We consider deterministic and nondeterministic variants and distinguish four working modes. It is known that these systems in the most general mode are as powerful as one-way multi-head finite automata. It is additionally known that the number of heads corresponds to the number of automata in PCFAs in a constructive way. Thus, undecidability results as well as results on the hierarchies induced by the number of heads carry over from multi-head finite automata to PCFAs in the most general mode. Here, we complement these undecidability and hierarchy results also for the remaining working modes. In particular, we show that classical decidability questions are not semi-decidable for any type of PCFAs under consideration. Moreover, it is proven that the number of automata in the system induces infinite hierarchies for deterministic and nondeterministic PCFAs in three working modes. KW - Automata systems KW - cooperating systems KW - formal languages KW - decidability questions Y1 - 2011 U6 - https://doi.org/10.1142/S0129054111008891 SN - 0129-0541 VL - 22 IS - 7 SP - 1577 EP - 1592 PB - World Scientific CY - Singapore ER - TY - JOUR A1 - Gebser, Martin A1 - Kaufmann, Benjamin A1 - Kaminski, Roland A1 - Ostrowski, Max A1 - Schaub, Torsten H. A1 - Schneider, Marius T1 - Potassco the Potsdam answer set solving collection JF - AI communications : AICOM ; the European journal on artificial intelligence N2 - This paper gives an overview of the open source project Potassco, the Potsdam Answer Set Solving Collection, bundling tools for Answer Set Programming developed at the University of Potsdam. KW - Answer set programming KW - declarative problem solving Y1 - 2011 U6 - https://doi.org/10.3233/AIC-2011-0491 SN - 0921-7126 VL - 24 IS - 2 SP - 107 EP - 124 PB - IOS Press CY - Amsterdam ER - TY - JOUR A1 - Gebser, Martin A1 - Sabuncu, Orkunt A1 - Schaub, Torsten H. T1 - An incremental answer set programming based system for finite model computation JF - AI communications : AICOM ; the European journal on artificial intelligence N2 - We address the problem of Finite Model Computation (FMC) of first-order theories and show that FMC can efficiently and transparently be solved by taking advantage of a recent extension of Answer Set Programming (ASP), called incremental Answer Set Programming (iASP). The idea is to use the incremental parameter in iASP programs to account for the domain size of a model. The FMC problem is then successively addressed for increasing domain sizes until an answer set, representing a finite model of the original first-order theory, is found. We implemented a system based on the iASP solver iClingo and demonstrate its competitiveness by showing that it slightly outperforms the winner of the FNT division of CADE's 2009 Automated Theorem Proving (ATP) competition on the respective benchmark collection. KW - Incremental answer set programming KW - finite model computation Y1 - 2011 U6 - https://doi.org/10.3233/AIC-2011-0496 SN - 0921-7126 VL - 24 IS - 2 SP - 195 EP - 212 PB - IOS Press CY - Amsterdam ER - TY - JOUR A1 - Bakera, Marco A1 - Margaria, Tiziana A1 - Renner, Clemens D. A1 - Steffen, Bernhard T1 - Game-Based model checking for reliable autonomy in space JF - Journal of aerospace computing, information, and communication N2 - Autonomy is an emerging paradigm for the design and implementation of managed services and systems. Self-managed aspects frequently concern the communication of systems with their environment. Self-management subsystems are critical, they should thus be designed and implemented as high-assurance components. Here, we propose to use GEAR, a game-based model checker for the full modal mu-calculus, and derived, more user-oriented logics, as a user friendly tool that can offer automatic proofs of critical properties of such systems. Designers and engineers can interactively investigate automatically generated winning strategies resulting from the games, this way exploring the connection between the property, the system, and the proof. The benefits of the approach are illustrated on a case study that concerns the ExoMars Rover. Y1 - 2011 U6 - https://doi.org/10.2514/1.32013 SN - 1940-3151 VL - 8 IS - 4 SP - 100 EP - 114 PB - American Institute of Aeronautics and Astronautics CY - Reston ER - TY - JOUR A1 - Arrighi, Pablo A1 - Nesme, Vincent A1 - Werner, Reinhard F. T1 - One-Dimensional quantum cellular automata JF - International journal of unconventional computing : non-classical computation and cellular automata N2 - We define and study quantum cellular automata (QCA). We show that they are reversible and that the neighborhood of the inverse is the opposite of the neighborhood. We also show that QCA always admit, modulo shifts, a two-layered block representation. Note that the same two-layered block representation result applies also over infinite configurations, as was previously shown for one-dimensional systems in the more elaborate formalism of operators algebras [18]. Here the proof is simpler and self-contained, moreover we discuss a counterexample QCA in higher dimensions. KW - cellular automata KW - quantum KW - neighborhood KW - block representation Y1 - 2011 SN - 1548-7199 VL - 7 IS - 4 SP - 223 EP - 244 PB - Old City Publishing Science CY - Philadelphia ER - TY - THES A1 - Smirnov, Sergey T1 - Business process model abstraction T1 - Abstraktion von Geschäftsprozessmodellen N2 - Business process models are used within a range of organizational initiatives, where every stakeholder has a unique perspective on a process and demands the respective model. As a consequence, multiple process models capturing the very same business process coexist. Keeping such models in sync is a challenge within an ever changing business environment: once a process is changed, all its models have to be updated. Due to a large number of models and their complex relations, model maintenance becomes error-prone and expensive. Against this background, business process model abstraction emerged as an operation reducing the number of stored process models and facilitating model management. Business process model abstraction is an operation preserving essential process properties and leaving out insignificant details in order to retain information relevant for a particular purpose. Process model abstraction has been addressed by several researchers. The focus of their studies has been on particular use cases and model transformations supporting these use cases. This thesis systematically approaches the problem of business process model abstraction shaping the outcome into a framework. We investigate the current industry demand in abstraction summarizing it in a catalog of business process model abstraction use cases. The thesis focuses on one prominent use case where the user demands a model with coarse-grained activities and overall process ordering constraints. We develop model transformations that support this use case starting with the transformations based on process model structure analysis. Further, abstraction methods considering the semantics of process model elements are investigated. First, we suggest how semantically related activities can be discovered in process models-a barely researched challenge. The thesis validates the designed abstraction methods against sets of industrial process models and discusses the method implementation aspects. Second, we develop a novel model transformation, which combined with the related activity discovery allows flexible non-hierarchical abstraction. In this way this thesis advocates novel model transformations that facilitate business process model management and provides the foundations for innovative tool support. N2 - Geschäftsprozessmodelle werden in einer Fülle organisatorischer Initiativen eingesetzt, wobei verschiedene Stakeholder individuelle Ansprüche an die Sicht auf den jeweiligen Prozess haben. Dies führt dazu, dass zu einem Geschäftsprozess eine Vielzahl unterschiedlicher Modelle existiert. In einer sich ständig verändernden Geschäftsumgebung ist es daher schwierig, diese Vielzahl von Modellen konsistent zu halten: Ändert sich sich ein Prozess, müssen alle Modelle, die ihn beschreiben, aktualisiert werden. Aufgrund der schieren Menge an Prozessmodellen und ihrer komplexen Beziehungen zueinander, erhöhen sich Aufwand und Kosten zur Pflege aller Modelle enorm. Vor diesem Hintergrund ermöglicht die Abstraktion von Geschäftsprozessmodellen, die Menge der Modelle zu reduzieren und damit ihre Verwaltung zu vereinfachen. Abstraktion von Geschäftsprozessmodellen bezeichnet eine Transformation eines Prozessmodells, so dass es für einen bestimmten Zweck besonders geeignet ist. Bei der Abstraktion von Geschäftsprozessen bleiben essentielle Eigenschaften eines Modells erhalten, während irrelevante Eigenschaften verworfen werden. Mehrere Studien stellen Prozessmodellabstraktion in den Fokus und konzentrieren sich auf konkrete Anwendungsfälle, für die sie geeignete Transformationen entwickelt haben. Diese Dissertation untersucht das Problem der Prozessmodellabstraktion und systematisiert die Lösung in einem Framework. Aktuelle Anforderungen der Industrie an die Abstraktion von Prozessmodellen wurden recherchiert und in einem Katalog von Anwendungsfällen zusammengefasst, von denen ein besonderer für die weiteren Untersuchungen ausgewählt wurde. In diesem Fall erwartet der Nutzer ein Modell niedrigeren Detailgrades, in welchem die Kontrollflussbeziehungen des Ursprungsmodells erhalten bleiben. Beginnend bei Modelltransformationen, die auf der Analyse der Prozessmodellstruktur aufbauen, entwickeln wir neuartige Abstraktionsoperationen zur Unterstützung dieses Anwendungsfalles. Darüber hinaus untersuchen wir Abstraktionsmethoden, welche die Semantik von Prozessmodellelementen berücksichtigen. Zum einen zeigen wir, wie Aktivitäten ermittelt werden können, die miteinander in semantischer Beziehung stehen - ein Problem, das bisher nur unzureichend betrachtet wurde. Die vorgeschlagenen Methoden werden mithilfe industrieller Prozessmodellsammlungen validiert und deren Umsetzung diskutiert. Zum anderen schlagen wir eine innovative Modelltransformation zur nicht-hierarchischen Abstraktion von Prozessmodellen vor. Dieser liegt die Ermittlung in Beziehung stehender Aktivitäten zugrunde. Demzufolge präsentiert diese Arbeit eine originäre Methode zur Prozessmodellabstraktion, die die Verwaltung von Geschäftsprozessmodellen vereinfacht und den Grundstein für innovative Softwarewerkzeuge legt. KW - Abstraktion KW - Prozess KW - Modell KW - Transformation KW - Komplexität KW - abstraction KW - process KW - model KW - transformation KW - complexity Y1 - 2011 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-60258 ER - TY - THES A1 - Gebser, Martin T1 - Proof theory and algorithms for answer set programming T1 - Beweistheorie und Algorithmen für die Antwortmengenprogrammierung N2 - Answer Set Programming (ASP) is an emerging paradigm for declarative programming, in which a computational problem is specified by a logic program such that particular models, called answer sets, match solutions. ASP faces a growing range of applications, demanding for high-performance tools able to solve complex problems. ASP integrates ideas from a variety of neighboring fields. In particular, automated techniques to search for answer sets are inspired by Boolean Satisfiability (SAT) solving approaches. While the latter have firm proof-theoretic foundations, ASP lacks formal frameworks for characterizing and comparing solving methods. Furthermore, sophisticated search patterns of modern SAT solvers, successfully applied in areas like, e.g., model checking and verification, are not yet established in ASP solving. We address these deficiencies by, for one, providing proof-theoretic frameworks that allow for characterizing, comparing, and analyzing approaches to answer set computation. For another, we devise modern ASP solving algorithms that integrate and extend state-of-the-art techniques for Boolean constraint solving. We thus contribute to the understanding of existing ASP solving approaches and their interconnections as well as to their enhancement by incorporating sophisticated search patterns. The central idea of our approach is to identify atomic as well as composite constituents of a propositional logic program with Boolean variables. This enables us to describe fundamental inference steps, and to selectively combine them in proof-theoretic characterizations of various ASP solving methods. In particular, we show that different concepts of case analyses applied by existing ASP solvers implicate mutual exponential separations regarding their best-case complexities. We also develop a generic proof-theoretic framework amenable to language extensions, and we point out that exponential separations can likewise be obtained due to case analyses on them. We further exploit fundamental inference steps to derive Boolean constraints characterizing answer sets. They enable the conception of ASP solving algorithms including search patterns of modern SAT solvers, while also allowing for direct technology transfers between the areas of ASP and SAT solving. Beyond the search for one answer set of a logic program, we address the enumeration of answer sets and their projections to a subvocabulary, respectively. The algorithms we develop enable repetition-free enumeration in polynomial space without being intrusive, i.e., they do not necessitate any modifications of computations before an answer set is found. Our approach to ASP solving is implemented in clasp, a state-of-the-art Boolean constraint solver that has successfully participated in recent solver competitions. Although we do here not address the implementation techniques of clasp or all of its features, we present the principles of its success in the context of ASP solving. N2 - Antwortmengenprogrammierung (engl. Answer Set Programming; ASP) ist ein Paradigma zum deklarativen Problemlösen, wobei Problemstellungen durch logische Programme beschrieben werden, sodass bestimmte Modelle, Antwortmengen genannt, zu Lösungen korrespondieren. Die zunehmenden praktischen Anwendungen von ASP verlangen nach performanten Werkzeugen zum Lösen komplexer Problemstellungen. ASP integriert diverse Konzepte aus verwandten Bereichen. Insbesondere sind automatisierte Techniken für die Suche nach Antwortmengen durch Verfahren zum Lösen des aussagenlogischen Erfüllbarkeitsproblems (engl. Boolean Satisfiability; SAT) inspiriert. Letztere beruhen auf soliden beweistheoretischen Grundlagen, wohingegen es für ASP kaum formale Systeme gibt, um Lösungsmethoden einheitlich zu beschreiben und miteinander zu vergleichen. Weiterhin basiert der Erfolg moderner Verfahren zum Lösen von SAT entscheidend auf fortgeschrittenen Suchtechniken, die in gängigen Methoden zur Antwortmengenberechnung nicht etabliert sind. Diese Arbeit entwickelt beweistheoretische Grundlagen und fortgeschrittene Suchtechniken im Kontext der Antwortmengenberechnung. Unsere formalen Beweissysteme ermöglichen die Charakterisierung, den Vergleich und die Analyse vorhandener Lösungsmethoden für ASP. Außerdem entwerfen wir moderne Verfahren zum Lösen von ASP, die fortgeschrittene Suchtechniken aus dem SAT-Bereich integrieren und erweitern. Damit trägt diese Arbeit sowohl zum tieferen Verständnis von Lösungsmethoden für ASP und ihrer Beziehungen untereinander als auch zu ihrer Verbesserung durch die Erschließung fortgeschrittener Suchtechniken bei. Die zentrale Idee unseres Ansatzes besteht darin, Atome und komposite Konstrukte innerhalb von logischen Programmen gleichermaßen mit aussagenlogischen Variablen zu assoziieren. Dies ermöglicht die Isolierung fundamentaler Inferenzschritte, die wir in formalen Charakterisierungen von Lösungsmethoden für ASP selektiv miteinander kombinieren können. Darauf aufbauend zeigen wir, dass unterschiedliche Einschränkungen von Fallunterscheidungen zwangsläufig zu exponentiellen Effizienzunterschieden zwischen den charakterisierten Methoden führen. Wir generalisieren unseren beweistheoretischen Ansatz auf logische Programme mit erweiterten Sprachkonstrukten und weisen analytisch nach, dass das Treffen bzw. Unterlassen von Fallunterscheidungen auf solchen Konstrukten ebenfalls exponentielle Effizienzunterschiede bedingen kann. Die zuvor beschriebenen fundamentalen Inferenzschritte nutzen wir zur Extraktion inhärenter Bedingungen, denen Antwortmengen genügen müssen. Damit schaffen wir eine Grundlage für den Entwurf moderner Lösungsmethoden für ASP, die fortgeschrittene, ursprünglich für SAT konzipierte, Suchtechniken mit einschließen und darüber hinaus einen transparenten Technologietransfer zwischen Verfahren zum Lösen von ASP und SAT erlauben. Neben der Suche nach einer Antwortmenge behandeln wir ihre Aufzählung, sowohl für gesamte Antwortmengen als auch für Projektionen auf ein Subvokabular. Hierfür entwickeln wir neuartige Methoden, die wiederholungsfreies Aufzählen in polynomiellem Platz ermöglichen, ohne die Suche zu beeinflussen und ggf. zu behindern, bevor Antwortmengen berechnet wurden. KW - Wissensrepräsentation und -verarbeitung KW - Antwortmengenprogrammierung KW - Beweistheorie KW - Algorithmen KW - Knowledge Representation and Reasoning KW - Answer Set Programming KW - Proof Theory KW - Algorithms Y1 - 2011 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-55425 ER - TY - THES A1 - Wist, Dominic T1 - Attacking complexity in logic synthesis of asynchronous circuits T1 - Komplexitätsbewältigung in der Logiksynthese asynchroner Schaltungen N2 - Most of the microelectronic circuits fabricated today are synchronous, i.e. they are driven by one or several clock signals. Synchronous circuit design faces several fundamental challenges such as high-speed clock distribution, integration of multiple cores operating at different clock rates, reduction of power consumption and dealing with voltage, temperature, manufacturing and runtime variations. Asynchronous or clockless design plays a key role in alleviating these challenges, however the design and test of asynchronous circuits is much more difficult in comparison to their synchronous counterparts. A driving force for a widespread use of asynchronous technology is the availability of mature EDA (Electronic Design Automation) tools which provide an entire automated design flow starting from an HDL (Hardware Description Language) specification yielding the final circuit layout. Even though there was much progress in developing such EDA tools for asynchronous circuit design during the last two decades, the maturity level as well as the acceptance of them is still not comparable with tools for synchronous circuit design. In particular, logic synthesis (which implies the application of Boolean minimisation techniques) for the entire system's control path can significantly improve the efficiency of the resulting asynchronous implementation, e.g. in terms of chip area and performance. However, logic synthesis, in particular for asynchronous circuits, suffers from complexity problems. Signal Transitions Graphs (STGs) are labelled Petri nets which are a widely used to specify the interface behaviour of speed independent (SI) circuits - a robust subclass of asynchronous circuits. STG decomposition is a promising approach to tackle complexity problems like state space explosion in logic synthesis of SI circuits. The (structural) decomposition of STGs is guided by a partition of the output signals and generates a usually much smaller component STG for each partition member, i.e. a component STG with a much smaller state space than the initial specification. However, decomposition can result in component STGs that in isolation have so-called irreducible CSC conflicts (i.e. these components are not SI synthesisable anymore) even if the specification has none of them. A new approach is presented to avoid such conflicts by introducing internal communication between the components. So far, STG decompositions are guided by the finest output partitions, i.e. one output per component. However, this might not yield optimal circuit implementations. Efficient heuristics are presented to determine coarser partitions leading to improved circuits in terms of chip area. For the new algorithms correctness proofs are given and their implementations are incorporated into the decomposition tool DESIJ. The presented techniques are successfully applied to some benchmarks - including 'real-life' specifications arising in the context of control resynthesis - which delivered promising results. N2 - Moderner Schaltungsentwurf fokussiert hauptsächlich synchrone Schaltungstechnik mit allen inhärenten Problemen. Asynchone (d.h. ungetaktete) Schaltungen zeichnen sich jedoch nicht nur durch das Fehlen der Taktversatzproblematik gegenüber ihren synchronen Pendents aus, sondern auch insbesondere durch geringeren Energieverbrauch, günstigere EMV-Eigenschaften, hohe Performance, Modularität und Robustheit gegenüber Schwankungen in der Spannungsversorgung, im Herstellungsprozess sowie Temperaturunterschieden. Diese Vorteile werden mit höherer Integration sowie höheren Taktraten signifikanter. Jedoch ist der Entwurf und auch der Test asynchroner Schaltungen erheblich schwieriger verglichen mit synchronen Schaltungen. Entwurfswerkzeuge zur Synthese asynchroner Schaltungen aus Hochsprachen-Spezifikationen sind zwar inzwischen verfügbar, sie sind jedoch noch nicht so ausgereift und bei weitem noch nicht so akzeptiert in der Industrie, wie ihre Äquivalente für den synchronen Schaltungsentwurf. Insbesondere fehlt es an Werkzeugunterstützung im Bereich der Logiksynthese komplexer Steuerungen („Controller“), welche kritisch für die Effizienz – z.B. in Bezug auf Chipfläche und Geschwindigkeit – der resultierenden Schaltungen oder Systeme ist. Zur Spezifikation von Steuerungen haben sich Signalflankengraphen („signal transition graphs“, STGs) bewährt, die auch als Entwurfseinstieg für eine Logiksynthese von SI-Schaltungen („speed independent“) verwendet werden. (SI-Schaltungen gelten als sehr robuste asynchrone Schaltungen.) Aus den STGs werden zwecks Logiksynthese Automaten abgeleitet werden, deren Zustandszahl aber oft prohibitiv groß werden kann. Durch sogenannte STG-Dekomposition wird die Logiksynthese einer komplexen Schaltung ermöglicht, was bislang aufgrund von Zustandsexplosion oft nicht möglich war. Dabei wird der Spezifikations-STG laut einer gegebenen Partition von Ausgangssignalen in viele kleinere Teilnetze dekomponiert, wobei zu jedem Partitionsblock ein Teilnetz – mit normalerweise signifikant kleinerem Zustandsraum im Vergleich zur Spezifikation – erzeugt wird. Zu jedem Teilnetz wird dann eine Teilschaltung (Komponente) mittels Logiksynthese generiert. Durch die Anwendung von STG-Dekomposition können jedoch Teilnetze erzeugt werden, die sogenannte irreduzible CSC-Konflikte aufweisen (d.h. zu diesen Teilnetzen kann keine SI-Schaltung erzeugt werden), obwohl die Spezifikation keine solchen Konflikte hatte. Diese Arbeit präsentiert einen neuen Ansatz, welcher die Entstehung solcher irreduziblen Konflikte vermeidet, und zwar durch die Einführung interner Kommunikation zwischen den (zu den Teilnetzen gehörenden) Schaltungskomponenten. Bisher werden STG-Dekompositionen total durchgeführt, d.h. pro resultierender Komponente wird ein Ausgangssignal erzeugt. Das führt gewöhnlich nicht zu optimalen Schaltungsimplementierungen. In dieser Arbeit werden Heuristiken zur Bestimmung gröberer Ausgabepartitionen (d.h. Partitionsblöcke mit mehreren Ausgangssignalen) vorgestellt, die zu kleineren Schaltungen führen. Die vorgestellten Algorithmen werden formal abgesichert und wurden in das bereits vorhandene Dekompositionswerkzeug DESIJ integriert. An praxisrelevanten Beispielen konnten die vorgestellten Verfahren erfolgreich erprobt werden. KW - Asynchrone Schaltung KW - Logiksynthese KW - Komplexitätsbewältigung KW - STG-Dekomposition KW - CSC KW - asynchronous circuit KW - logic synthesis KW - speed independence KW - STG decomposition KW - CSC Y1 - 2011 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-59706 ER - TY - THES A1 - Lorenz, Haik T1 - Texturierung und Visualisierung virtueller 3D-Stadtmodelle T1 - Texturing and Visualization of Virtual 3D City Models N2 - Im Mittelpunkt dieser Arbeit stehen virtuelle 3D-Stadtmodelle, die Objekte, Phänomene und Prozesse in urbanen Räumen in digitaler Form repräsentieren. Sie haben sich zu einem Kernthema von Geoinformationssystemen entwickelt und bilden einen zentralen Bestandteil geovirtueller 3D-Welten. Virtuelle 3D-Stadtmodelle finden nicht nur Verwendung als Mittel für Experten in Bereichen wie Stadtplanung, Funknetzplanung, oder Lärmanalyse, sondern auch für allgemeine Nutzer, die realitätsnah dargestellte virtuelle Städte in Bereichen wie Bürgerbeteiligung, Tourismus oder Unterhaltung nutzen und z. B. in Anwendungen wie GoogleEarth eine räumliche Umgebung intuitiv erkunden und durch eigene 3D-Modelle oder zusätzliche Informationen erweitern. Die Erzeugung und Darstellung virtueller 3D-Stadtmodelle besteht aus einer Vielzahl von Prozessschritten, von denen in der vorliegenden Arbeit zwei näher betrachtet werden: Texturierung und Visualisierung. Im Bereich der Texturierung werden Konzepte und Verfahren zur automatischen Ableitung von Fototexturen aus georeferenzierten Schrägluftbildern sowie zur Speicherung oberflächengebundener Daten in virtuellen 3D-Stadtmodellen entwickelt. Im Bereich der Visualisierung werden Konzepte und Verfahren für die multiperspektivische Darstellung sowie für die hochqualitative Darstellung nichtlinearer Projektionen virtueller 3D-Stadtmodelle in interaktiven Systemen vorgestellt. Die automatische Ableitung von Fototexturen aus georeferenzierten Schrägluftbildern ermöglicht die Veredelung vorliegender virtueller 3D-Stadtmodelle. Schrägluftbilder bieten sich zur Texturierung an, da sie einen Großteil der Oberflächen einer Stadt, insbesondere Gebäudefassaden, mit hoher Redundanz erfassen. Das Verfahren extrahiert aus dem verfügbaren Bildmaterial alle Ansichten einer Oberfläche und fügt diese pixelpräzise zu einer Textur zusammen. Durch Anwendung auf alle Oberflächen wird das virtuelle 3D-Stadtmodell flächendeckend texturiert. Der beschriebene Ansatz wurde am Beispiel des offiziellen Berliner 3D-Stadtmodells sowie der in GoogleEarth integrierten Innenstadt von München erprobt. Die Speicherung oberflächengebundener Daten, zu denen auch Texturen zählen, wurde im Kontext von CityGML, einem international standardisierten Datenmodell und Austauschformat für virtuelle 3D-Stadtmodelle, untersucht. Es wird ein Datenmodell auf Basis computergrafischer Konzepte entworfen und in den CityGML-Standard integriert. Dieses Datenmodell richtet sich dabei an praktischen Anwendungsfällen aus und lässt sich domänenübergreifend verwenden. Die interaktive multiperspektivische Darstellung virtueller 3D-Stadtmodelle ergänzt die gewohnte perspektivische Darstellung nahtlos um eine zweite Perspektive mit dem Ziel, den Informationsgehalt der Darstellung zu erhöhen. Diese Art der Darstellung ist durch die Panoramakarten von H. C. Berann inspiriert; Hauptproblem ist die Übertragung des multiperspektivischen Prinzips auf ein interaktives System. Die Arbeit stellt eine technische Umsetzung dieser Darstellung für 3D-Grafikhardware vor und demonstriert die Erweiterung von Vogel- und Fußgängerperspektive. Die hochqualitative Darstellung nichtlinearer Projektionen beschreibt deren Umsetzung auf 3D-Grafikhardware, wobei neben der Bildwiederholrate die Bildqualität das wesentliche Entwicklungskriterium ist. Insbesondere erlauben die beiden vorgestellten Verfahren, dynamische Geometrieverfeinerung und stückweise perspektivische Projektionen, die uneingeschränkte Nutzung aller hardwareseitig verfügbaren, qualitätssteigernden Funktionen wie z.~B. Bildraumgradienten oder anisotroper Texturfilterung. Beide Verfahren sind generisch und unterstützen verschiedene Projektionstypen. Sie ermöglichen die anpassungsfreie Verwendung gängiger computergrafischer Effekte wie Stilisierungsverfahren oder prozeduraler Texturen für nichtlineare Projektionen bei optimaler Bildqualität. Die vorliegende Arbeit beschreibt wesentliche Technologien für die Verarbeitung virtueller 3D-Stadtmodelle: Zum einen lassen sich mit den Ergebnissen der Arbeit Texturen für virtuelle 3D-Stadtmodelle automatisiert herstellen und als eigenständige Attribute in das virtuelle 3D-Stadtmodell einfügen. Somit trägt diese Arbeit dazu bei, die Herstellung und Fortführung texturierter virtueller 3D-Stadtmodelle zu verbessern. Zum anderen zeigt die Arbeit Varianten und technische Lösungen für neuartige Projektionstypen für virtueller 3D-Stadtmodelle in interaktiven Visualisierungen. Solche nichtlinearen Projektionen stellen Schlüsselbausteine dar, um neuartige Benutzungsschnittstellen für und Interaktionsformen mit virtuellen 3D-Stadtmodellen zu ermöglichen, insbesondere für mobile Geräte und immersive Umgebungen. N2 - This thesis concentrates on virtual 3D city models that digitally encode objects, phenomena, and processes in urban environments. Such models have become core elements of geographic information systems and constitute a major component of geovirtual 3D worlds. Expert users make use of virtual 3D city models in various application domains, such as urban planning, radio-network planning, and noise immision simulation. Regular users utilize virtual 3D city models in domains, such as tourism, and entertainment. They intuitively explore photorealistic virtual 3D city models through mainstream applications such as GoogleEarth, which additionally enable users to extend virtual 3D city models by custom 3D models and supplemental information. Creation and rendering of virtual 3D city models comprise a large number of processes, from which texturing and visualization are in the focus of this thesis. In the area of texturing, this thesis presents concepts and techniques for automatic derivation of photo textures from georeferenced oblique aerial imagery and a concept for the integration of surface-bound data into virtual 3D city model datasets. In the area of visualization, this thesis presents concepts and techniques for multiperspective views and for high-quality rendering of nonlinearly projected virtual 3D city models in interactive systems. The automatic derivation of photo textures from georeferenced oblique aerial imagery is a refinement process for a given virtual 3D city model. Our approach uses oblique aerial imagery, since it provides a citywide highly redundant coverage of surfaces, particularly building facades. From this imagery, our approach extracts all views of a given surface and creates a photo texture by selecting the best view on a pixel level. By processing all surfaces, the virtual 3D city model becomes completely textured. This approach has been tested for the official 3D city model of Berlin and the model of the inner city of Munich accessible in GoogleEarth. The integration of surface-bound data, which include textures, into virtual 3D city model datasets has been performed in the context of CityGML, an international standard for the exchange and storage of virtual 3D city models. We derive a data model from a set of use cases and integrate it into the CityGML standard. The data model uses well-known concepts from computer graphics for data representation. Interactive multiperspective views of virtual 3D city models seamlessly supplement a regular perspective view with a second perspective. Such a construction is inspired by panorama maps by H. C. Berann and aims at increasing the amount of information in the image. Key aspect is the construction's use in an interactive system. This thesis presents an approach to create multiperspective views on 3D graphics hardware and exemplifies the extension of bird's eye and pedestrian views. High-quality rendering of nonlinearly projected virtual 3D city models focuses on the implementation of nonlinear projections on 3D graphics hardware. The developed concepts and techniques focus on high image quality. This thesis presents two such concepts, namely dynamic mesh refinement and piecewise perspective projections, which both enable the use of all graphics hardware features, such as screen space gradients and anisotropic texture filtering under nonlinear projections. Both concepts are generic and customizable towards specific projections. They enable the use of common computer graphics effects, such as stylization effects or procedural textures, for nonlinear projections at optimal image quality and interactive frame rates. This thesis comprises essential techniques for virtual 3D city model processing. First, the results of this thesis enable automated creation of textures for and their integration as individual attributes into virtual 3D city models. Hence, this thesis contributes to an improved creation and continuation of textured virtual 3D city models. Furthermore, the results provide novel approaches to and technical solutions for projecting virtual 3D city models in interactive visualizations. Such nonlinear projections are key components of novel user interfaces and interaction techniques for virtual 3D city models, particularly on mobile devices and in immersive environments. KW - Computergrafik KW - virtuelle 3D-Stadtmodelle KW - CityGML KW - nichtlineare Projektionen KW - Texturen KW - computer graphics KW - virtual 3D city models KW - CityGML KW - nonlinear projections KW - textures Y1 - 2011 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-53879 ER - TY - THES A1 - Menzel, Michael T1 - Model-driven security in service-oriented architectures : leveraging security patterns to transform high-level security requirements to technical policies T1 - Modell-getriebene Sicherheit in Service-orientierten Architekturen N2 - Service-oriented Architectures (SOA) facilitate the provision and orchestration of business services to enable a faster adoption to changing business demands. Web Services provide a technical foundation to implement this paradigm on the basis of XML-messaging. However, the enhanced flexibility of message-based systems comes along with new threats and risks. To face these issues, a variety of security mechanisms and approaches is supported by the Web Service specifications. The usage of these security mechanisms and protocols is configured by stating security requirements in security policies. However, security policy languages for SOA are complex and difficult to create due to the expressiveness of these languages. To facilitate and simplify the creation of security policies, this thesis presents a model-driven approach that enables the generation of complex security policies on the basis of simple security intentions. SOA architects can specify these intentions in system design models and are not required to deal with complex technical security concepts. The approach introduced in this thesis enables the enhancement of any system design modelling languages – for example FMC or BPMN – with security modelling elements. The syntax, semantics, and notion of these elements is defined by our security modelling language SecureSOA. The metamodel of this language provides extension points to enable the integration into system design modelling languages. In particular, this thesis demonstrates the enhancement of FMC block diagrams with SecureSOA. To enable the model-driven generation of security policies, a domain-independent policy model is introduced in this thesis. This model provides an abstraction layer for security policies. Mappings are used to perform the transformation from our model to security policy languages. However, expert knowledge is required to generate instances of this model on the basis of simple security intentions. Appropriate security mechanisms, protocols and options must be chosen and combined to fulfil these security intentions. In this thesis, a formalised system of security patterns is used to represent this knowledge and to enable an automated transformation process. Moreover, a domain-specific language is introduced to state security patterns in an accessible way. On the basis of this language, a system of security configuration patterns is provided to transform security intentions related to data protection and identity management. The formal semantics of the security pattern language enable the verification of the transformation process introduced in this thesis and prove the correctness of the pattern application. Finally, our SOA Security LAB is presented that demonstrates the application of our model-driven approach to facilitate a dynamic creation, configuration, and execution of secure Web Service-based composed applications. N2 - Im Bereich der Enterprisearchitekturen hat das Paradigma der Service-orientierten Architektur (SOA) in den vergangenen Jahren eine große Bedeutung erlangt. Dieser Ansatz ermöglicht die Strukturierung und Umsetzung verteilter, IT-basierter Geschäftsfunktionen, um einen effizienten und flexiblen Einsatz von IT-Ressourcen zu ermöglichen. Während in der Vergangenheit fachliche Anforderungen in monolithischen Applikationen umgesetzt wurden, setzt dieser Architekturansatz auf wiederverwendbare Dienste, die spezifische Geschäftsfunktionen implementieren. Diese Dienste können dann dynamisch zur Umsetzung von Geschäftsprozessen herangezogen werden und ermöglichen eine schnelle Reaktion auf verändernde geschäftliche Rahmenbedingungen durch Anpassung der Prozesse. Die einzelnen Dienste existieren unabhängig voneinander und sind lose über einen Nachrichtenaustausch gekoppelt. Diese Unabhängigkeit unterscheidet den SOA-Ansatz von der bisherigen Entwicklung klassischer verteilter Anwendungen. Die Verwendung unabhängiger Dienste geht aber auch mit einem größeren Gefährdungspotential einher, da eine Vielzahl von Schnittstellen bereitgestellt wird, die mittels komplexer Protokolle angesprochen werden können. Somit ist die korrekte Umsetzung von Sicherheitsmechanismen in allen Diensten und SOA-Infrastrukturkomponeten essentiell. Kommunikationspartner müssen an jedem Kommunikationsendpunkt authentifiziert und autorisiert werden und ausgetauschte Nachrichten müssen immer geschützt werden. Solche Sicherheitsanforderungen werden in technischen Sicherheitskonfigurationen (Policydokumenten) mittels einer Policysprache kodiert und werden an die Dienste verteilt, die diese Anforderungen durchsetzen. Da Policysprachen für SOA aber durch die Vielzahl und Vielfalt an Sicherheitsmechanismen, -protokollen und -standards eine hohe Komplexität aufweisen, sind Sicherheitskonfigurationen höchst fehleranfällig und mit viel Fachwissen zu erstellen. Um die Generierung von Sicherheitskonfigurationen in komplexen Systemen zu vereinfachen, wird in dieser Arbeit ein modellgetriebener Ansatz vorgestellt, der eine visuelle Modellierung von Sicherheitsanforderungen in Architekturmodellen ermöglicht und eine automatisierte Generierung von Sicherheitskonfigurationen auf Basis dieser Anforderungen unterstützt. Die Modellierungsebene ermöglicht eine einfache und abstrakte Darstellung von Sicherheitsanforderungen, die sich auch für Systemarchitekten erschließen, welche keine Sicherheits-experten sind. Beispielsweise können modellierte Daten einfach mit einem Schloss annotiert werden, um den Schutz dieser Daten zu fordern. Die Syntax, die Semantik und die Darstellung dieser Anforderungen werden durch die in dieser Arbeit vorgestellte Sicherheitsmodellierungssprache SecureSOA spezifiziert. Der vorgestellte modellgetriebene Ansatz transformiert die modellierten Anforderungen auf ein domänen-unabhängiges Policymodell, das eine Abstraktionsschicht zu konkreten Policysprachen bildet. Diese Abstrak-tionsschicht vereinfacht die Generierung von Sicherheitspolicies in verschiedenen Policysprachen. Allerdings kann diese Transformation nur erfolgen, wenn im System Expertenwissen hinterlegt ist, das die Auswahl von konkreten Sicherheitsmechanismen und -optionen bestimmt. Im Rahmen dieser Arbeit werden Entwurfsmuster für SOA-Sicherheit zur Transformation herangezogen, die dieses Wissen repräsentieren. Dazu wird ein Katalog von Entwurfsmustern eingeführt, der die Abbildung von abstrakten Sicherheitsanforderungen auf konkrete Konfigurationen ermöglicht. Diese Muster sind mittels einer Entwurfsmustersprache definiert, die in dieser Arbeit eingeführt wird. Die formale Semantik dieser Sprache ermöglicht die formale Verifikation des Transformationsprozesses, um die Korrektheit der Entwurfsmusteranwendung nachzuweisen. Die Definition dieses Entwurfsmusterkatalogs und der darauf basierende Transformationsprozess ermöglichen die Abbildung von abstrakten Sicherheitsanforderungen auf konkrete technische Sicherheitskonfigurationen und stellen den Beitrag dieser Arbeit dar. Abschließend wird in dieser Arbeit das SOA-Security-Lab vorgestellt, das die Umsetzung dieses Ansatzes demonstriert. KW - IT-Sicherheit KW - Service-Orientierte Architekturen KW - Modell-getriebene Sicherheit KW - Sicherheitsmodellierung KW - Entwurfsmuster für SOA-Sicherheit KW - IT-Security KW - Service-oriented Architectures KW - Modell-driven Security KW - Security Modelling KW - SOA Security Pattern Y1 - 2011 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-59058 ER - TY - JOUR A1 - Lindberg, Tilmann A1 - Meinel, Christoph A1 - Wagner, Ralf T1 - Design thinking : a fruitful concept for IT development? Y1 - 2011 SN - 978-3-642-13756-3 ER - TY - BOOK A1 - Linckels, Serge A1 - Meinel, Christoph T1 - E-Librarian service : user-friendly semantic search in digital libraries Y1 - 2011 SN - 978-3-642-17742-2 U6 - https://doi.org/10.1007/978-3-642-17743-9 PB - Springer-Verlag Berlin Heidelberg CY - Berlin, Heidelberg ER - TY - JOUR A1 - Meinel, Christoph A1 - Leifer, Larry T1 - Design thinking research Y1 - 2011 SN - 978-3-642-13756-3 ER - TY - GEN ED - Plattner, Hasso ED - Meinel, Christoph ED - Leifer, Larry T1 - Design thinking : understand - improve - apply Y1 - 2011 SN - 978-3-642-13756-3 PB - Springer-Verlag Berlin Heidelberg CY - Berlin, Heidelberg ER - TY - JOUR A1 - Gumienny, Raja A1 - Meinel, Christoph A1 - Gericke, Lutz A1 - Quasthoff, Matthias A1 - LoBue, Peter A1 - Willems, Christian T1 - Tele-board : enabling efficient collaboration in digital design spaces across time and distance Y1 - 2011 SN - 978-3-642-13756-3 ER -