direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments


Perspectives on Physical Modeling from Real World Applications
Dr. Michael Tiller, Dassault Systèmes
The material in this talk is based on experiences collected from practical applications involving real-world engineering problems. The first topic will be how practical formulations diverge from some of the typical theory for dynamic systems presented at the university level. From there, the discussion turns to how high-performance applications like Hardware-in-the-Loop are driving simulation technology increasingly in the direction of symbolic techniques in an effort generate to achieve the next level of performance as compared to purely numerical methods. Finally, some discussion of possible strategic goals for the evolution of Modelica will be discussed.
Optimization of Visitor Performance by Reflection-Based Analysis
Markus Lepper, semantics GmbH, Berlin
Visitors and Rewriters are a well-known and powerful design pattern for processing regular data structures in a declarative way, still writing imperative code.

The authors' "umod" model generator creates Java data models from a concise and algebraic notation. It is primarily used to model intermediate representations of computer languages.

The generated Java code includes safe setter/getter functions and constructors which check for legal values, visualization, serialization, etc.

The user defines visitor and rewriter code by extending skeletons classes, which are generated according to traversal annotations in the model.

Since the generated code (naturally) executes the pure traversal and no semantic activities, traversals are redundant unless some user-overridden method is eventually invoked.

We present a reflection-based control flow analysis to detect this situation and prune the traversal transparently. With a well-stratified model, this may lead to substantial increase in performance.
Modeling Kernel Language
David Broman, Universität Linköping
03. 03. 2011
Performing computational experiments on mathematical models instead of building and testing physical prototypes can drastically reduce the development cost for complex systems such as automobiles, aircraft, and powerplants. In the past three decades, a category of equation-based modeling languages has appeared that is based on acausal and
object-oriented modeling principles, enabling good reuse of models.
Examples of these languages are Modelica, VHDL-AMS, and gPROMS.
However, the modeling languages within this category have grown to be large and complex, where the specifications of the language's semantics are informally defined, typically described in natural languages. The lack of a formal semantics makes these languages hard to interpret unambiguously and to reason about.
  In this talk a new research language called the Modeling Kernel Language (MKL) is presented. By introducing the concept of higher-order acausal models (HOAMs), we show that it is possible to create expressive modeling libraries in a manner analogous to Modelica, but using a small and simple language concept. In contrast to the current state-of-the-art modeling languages, the semantics of how to use the models, including meta operations on models, are also specified in MKL libraries. This enables extensible formal executable specifications where important language features are expressed through libraries rather than by adding completely new language constructs. MKL is a statically typed language based on a typed lambda calculus. We define the core of the language formally using operational semantics and prove type safety.  An MKL interpreter is implemented and verified in comparison with a Modelica environment.
Programmierung als Leitbild in der Theorie der Ökosysteme
Baltasar Trancón y Widemann, Universität Bayreuth
12. 01. 2011
Die Umweltwissenschaften haben im Lauf ihrer Entstehung als Disziplin das Forschungsprogramm der klassischen Physik mit dem Paradigma der mechanistischen Systeme weitgehend unhinterfragt übernommen. Es zeigt sich, dass dieses Vorgehen umso problematischer ist, je mehr lebende Bestandteile das Verhalten des Systems dominieren. Andererseits gibt es zahlreiche alte, gesellschaftlich hochrelevante und erfolgreiche Nutzungstraditionen von Umweltsystemen, die theoriefrei und rein heuristisch funktionieren. Als Folge entsteht eine im Bereich der Naturwissenschaften einmalige Spannung zwischen Theorie und Praxis, und es zeigen sich Symptome einer wissenschaftlichen Krise, wie sie oft nur durch einen Paradigmenwechsel zu lösen ist. Dieser Vortrag soll
dreierlei zeigen: Erstens, dass aktuelle Entwicklungen im Bereich der computergestützten Umweltmodellierung sich dem Informatiker als Krisensymptome darstellen, die dem "laienhaften Anwender" verschlossen bleiben. Zweitens, dass Begriffe aus der Softwaretechnik und der Programmanalyse geeignet sind, die Rolle von Theorie und Modellierung von Ökosystemen metaphorisch zu beschreiben. Drittens, dass sich Formalismen aus dem Bereich der Semantik von Programmiersprachen und -kalkülen ganz konkret als Basis eines alternativen Paradigmas der Theorie der Ökosysteme eignen. Als Beispiel für den letzten Punkt dient die Anwendung der Theorie der bialgebraischen denotationellen Semantik von Turi und Plotkin auf populäre agentenbasierte Ökosystemmodelle.
Open Protocol Notation - Design and Implementation
Dr. Wolfgang Grieskamp, (Microsoft Research)
28. 10. 2010
OPN (Open Protocol Notation) is at the center of PEF, a model-driven engineering framework for communication protocols, and an incubation project currently running in the Windows Interoperability Engineering group. PEF enables scenarios such as runtime monitoring and verification, model-based testing, model analysis, documentation generation, etc. In this informal talk basics of the language design and implementation will be discussed.
Smart Dust to Smart Cars: Why Modeling Enables Next-Gen Systems

Wolfram Schulte
Microsoft Research, Redmond, USA
The economics of the automotive, aerospace and defense sectors depend on delivering value-added features through software. Already, 90% of innovations in the automotive market occur in software. However, the next waves of innovations are risky; they require exposing and networking safety-critical subsystems. These subsystems include the software controlling propulsion, maneuvering, and emergency systems. Existing software development approaches do not provide sufficient guarantees of end-to-end correctness to enable these scenarios. Therefore, modeling is a key enabler offering new techniques for architecting complex systems correctly.
In this talk I will give an overview of our model-based development (MBD) framework called FORMULA. Our framework provides a unique set of innovations aimed at developers of these next-gen systems, including: (1) Formal modeling for multi-faceted architectures with non-functional requirements, (2) Design space exploration for automatically enumerating architectures satisfying complex requirements, (3) Safe reuse of modeling artifacts as requirements evolve.
Analyzing and Understanding Nondeterministic Systems with Hierarchical Graph Rewriting

Kazunori Ueda, Department of Computer Science and Engineering, Waseda University, Tokyo, Japan
This talk is a gentle introduction to state-space search and model checking with LMNtal, with live demos using our LMNtal IDE powered by a visualizer.
LMNtal is a language based on (a class of) hierarchical graph rewriting, whose goal is to provide a unifying formalism of diverse computational models involving concurrency, mobility and multiset rewriting. To broaden its applications, our publicly available LMNtal implementation has recently evolved into a model checker that employs LMNtal as the modeling language and PLTL as the specification language.
The strengths of our LMNtal model checker are its powerful data structures, highly nondeterministic computation it can express, and little discrepancy between programming and modeling languages. Models expressed in Promela, MSR, and Coloured Petri Nets can be easily encoded into LMNtal. The visualizer of the LMNtal IDE turned out to be extremely useful in understanding models by state space browsing, which is in sharp contrast with other black-box model checkers. The LMNtal IDE has been used to run and visualize diverse examples taken from the fields of model checking, concurrency and AI search.
Authentication in pervasive and social computation

Dusko Pavlovic
Kestrel Institute
In computer networks, information flows through a virtual space. In pervasive and social computation, information is also carried through physical space. This completely changes the security landscape. In computer networks, the problem of authentication arises from the fact that all observations are local: a computer Alice can only observe her own actions, and therefore needs some solid cryptographic assumptions to prove to herself, say, that a computer Bob has indeed sent this message. However, if Alice and Bob are not computers on the Internet, but, say, PDAs in a cafe, then they can use their respective humans to observe each other's actions and in particular to directly authenticate some messages. This is something that computers on the Internet couldn't even dream about. In this talk, I shall describe a framework for reasoning about authentication in the systems where some of the communication channels are deployed in a physical space.
Multi-Paradigmatic Model-Based Testing

Wolfgang Grieskamp
Microsoft Research
For half a decade model-based testing has been applied at Microsoft in the internal develop- ment process. Though a success story compared to other formal quality assurance approaches like verification, a break-through of the technology on a broader scale is not yet in sight. What are the obstacles? Some lessons can be learned from the past and will be discussed. An approach to MBT is described which is based on multi-paradigmatic modeling, which gives users the freedom to choose among programmatic and diagrammatic notations, as well as state-based and scenario- based styles, reflecting the different concerns in the process. The diverse model styles can be combined by model composition in order to achieve an integrated and collaborative model-based testing process. The approach is realized in the successor of Microsoft Research's MBT tool Spec Explorer, and has a formal foundation in the framework of action machines.
Program verification and testing at Microsoft Research

Nikolai Tillmann
Microsoft Research
This talk gives an overview of the ongoing research activities at Microsoft Research devoted to improving software development productivity using formal methods. In particular, I will introduce three methodologies which support the software development process in different stages. Each methodology is supported by tools: (1) Spec Explorer: system modeling and testing with model programs. (2) MUTT: better unit testing using symbolic execution to analyze existing implementations. (3) Spec# programming system: program verification by extending C# with pre/postconditions and invariants.
Tree Transducers - From Practice to Theory to Practice

Dr.-Ing. Armin Kühnemann
Institut für Theoretische Informatik Technische Universität Dresden
Ausgehend von vier praktischen Problemen, (i) der Definition einer formalen Semantik für imperative Programmiersprachen, (ii) der Spezifikation von XML-Transformationen, (iii) der Verbesserung der Effizienz funktionaler Programme, und (iv) der Verbesserung des automatischen Beweisbarkeit von Programmeigenschaften, motivieren wir die Theorie der Tree Transducer. Wir wählen zwei gegenläufige theoretische Resultate für Tree Transducer, die Komposition und die Dekomposition, aus und zeigen, daß sich diese auch in der Praxis anwenden lassen. Insbesondere demonstrieren wir, wie die Komposition und deren Weiterentwicklung Akkumulation die Effizienz von Programmen verbessern kann, und wie die Deakkumulation, eine Weiterentwicklung der Dekomposition, die automatische Verifizierbarkeit verbessern kann.
Drei Dimensionen der Array-Optimierung in SAC

www.isp.uni-luebeck.de/%7EgrelckDr. rer. nat. Clemens Grelck
Institut für Softwaretechnik und Programmiersprachen der Universität zu Lübeck
SAC (Single Assignment C) ist eine rein-funktionale Arraysprache mit der Zielsetzung, Programmspezifikationen auf einem hohen Abstraktionsniveau mit einem hochperformanten Laufzeitverhalten zu verbinden. Der klassischen, von Maschinen-orientierten Progrmmiersprachen geprägten Sichtweise von Arrays als direkte Abbildungen in den Speicher mit lediglich rudimentären Indizierungsmöglichkeiten stellt SAC multidimensionale Arrays als abstrakte Datenstrukturen mit gewissen algebraischen Eigenschaften gegenüber. An die Stelle unübersichtlicher Schachtelungen von Schleifen zur Lösung eines individuellen Problems tritt das Prinzip der Komposition. Anwendungsprogramme entstehen durch stufenweise Komposition von einfachen und Problem-unspezifischen Array-Operationen zu immer komplexeren und immer Problem-spezifischeren Operationen. Dieses Prinzip führt nicht nur zu sehr knappen und abstrakten Programmspezifikationen, sondern erlaubt auch ein hohes Maß an Code-Wiederverwendung auf den verschiedenen Abstraktionsstufen.
Leider läuft das Programmierkonzept der Komposition von Array-Operationen dem zweiten Ziel von SAC, dem effizienten Laufzeitverhalten kompilierter Programme, zuwider. Die direkte Übersetzung führt zwangsläufig zu ausführbarem Code, der zur Laufzeit eine sehr große Anzahl temporärer oder intermediärer Datenstrukturen erzeugt. Diese führen zu erheblichem organisatorischem Mehraufwand für Speicherverwaltung und Schleifenausführung, zu einer geringen Datenlokalität und insgesamt zu einem mehr als unbefriedigenden Laufzeitverhalten.
Im Anschluss an eine kurze Einführung in die Prinzipien der Programmiersprache SAC identifizieren wir in dem Vortrag drei verschiedene Arten der Komposition von Array-Operationen und untersuchen jeweils die dadurch entstehenden Probleme und Herausforderungen für eine Übersetzung in effizienten Code. Für jede der drei Achsen des Problemfeldes wird eine konkrete Optimierungstechnik vorgestellt. Ihre aggregierte Wirkung wird an Hand einer Fallstudie untersucht.
Fehlersuche beim Debuggen nebenläufiger Programme

www.informatik.uni-kiel.de/%7EfhuDr. Frank Huch
Institut für Informatik und Praktische Mathematik Christian-Albrechts-Universität zu Kiel
Nebenläufige Systeme können neue, bei sequentiellen Systemen nicht auftretende Fehler enthalten, wie z.B. Deadlocks, Lifelocks oder die Nichteinhaltung von wechselseitigem Ausschluss. Im Gegensatz zu klassischen Fehlern sequentieller Programme, hängen diese Fehler vom Prozess-Scheduling ab und treten möglicherweise nur in bestimmten Systemläufen auf.
Zum Finden von Fehlern werden in der Regel Debugger verwendet, welche den Programmablauf visualisieren und so ein besseres Verständnis der Fehlersituation ermöglichen sollen. Wir haben einen Debugger für Concurrent Haskell (eine nebenläufige Erweiterung der lazy- funktionalen Programmiersprache Haskell ) entwickelt. Dieser ermöglicht es, nebenläufige Haskell Programme auszuführen und manuell unterschiedliche Prozess-Scheduls auf Fehler zu überprüfen.
Ein Nachteil dieses (auch bei den meisten anderen nebenläufigen Sprachen verwendeten) Ansatzes ist, dass sich ein System beispielsweise kurz vor einem Deadlock befinden kann, der Benutzer aber ein falsches Scheduling wählt und so den Programmfehler nicht findet. Als Lösung für dieses Problem soll der Debugger (alle) möglichen Schedules simulieren und im Fehlerfall den Benutzer in den Fehler leiten. Da nicht nur Deadlocks mögliche Fehler sind, soll die Linearzeit Logik (LTL) zur Spezifikation allgemeiner Fehlerzustände verwendet werden.
Im Vortrag präsentieren wir die prototypische Implementierung des Debuggers, welche ohne eine Veränderung des Laufzeitsystems von Concurrent Haskell vorgenommen werden konnte.
Selektor-erzeugte Modelle verallgemeinerter logischer Programme

Sibylle Schwarz
Institut für Informatik der Universität Leipzig
Logische Programme sind gut geeignet zur Repräsentation von Fach- und Alltagswissen in Fakten- und Regelform. Im Vortrag wird eine Klasse modelltheoretischer Semantiken für verallgemeinerte logische Programme vorgestellt. Bei der Untersuchung einzelner Vertreter wird klar, daß sich viele prominente Semantiken (wie zum Beispiel die inflationäre Fixpunkt- und die stabile Semantik) als Spezialfälle davon darstellen lassen.
DNA-Computing - Rechnen mit Molekülen

Dr.-Ing. Monika Sturm
Technische Universität Dresden, Institut für Theoretische Informatik
In den letzten Jahren wurden in der Informatik verschiedene Ideen zur Entwicklung unkonventioneller Rechenmodelle verfolgt und realisiert. Alternativ zu klassischen Modellen basieren einige dieser Entwicklungen auf der Abstraktion biochemischer Prozesse. DNA-Computing stellt in diesem Zusammenhang eine spezielle Form für das Rechnen mit Molekülen dar. DNA dient dabei als Datenträger und die Rechenoperationen werden durch geeignete molekularbiologische und biochemische Prozesse realisiert.
Ziel der Arbeiten an der TU Dresden ist die Entwicklung eines Modells für einen universellen DNA-Computer und dessen Implementierung im molekularbiologischen Labor. Algorithmen, die konstruiert werden, nutzen eine massive Datenparallelität, die es ermöglicht, mit DNA-Computern Rechengeschwindigkeiten zu erreichen, die einen Vergleich zu bekannter elektronischer Rechentechnik herausfordern. Der Vortrag thematisiert zunächst die Entwicklung des interdisziplinären Forschungsgebietes und stellt drei wichtige Aspekte in den Mittelpunkt. Die Vorstellung experimenteller Arbeiten soll zeigen, welche mathematischen Problemstellungen für DNA-Computing charakteristisch sind und welche Ergebnisse bisher erreicht wurden. Ein weiterer Aspekt beschäftigt sich mit der Fragestellung, wie ein theoretisches Modell aufgebaut sein könnte, welches DNA-Computing formal beschreibt, notwendige molekularbiologische Operationen umfaßt und laborpraktisch realisierbar ist. In einem letzten Aspekt soll betrachtet werden, wie ein funktional implementiertes Tool zur Konstruktion von DNA-Algorithmen und ein probabilistisches Simulationsmodell zur Vorbereitung von Experimenten eingesetzt werden.
Verification Diagrams: Graph+Logic+Automata

Zohar Manna
Stanford University
Verification Diagrams combine deductive ("theorem-proving") and algorithmic ("model-checking") verification to establish general temporal-logic properties of infinite-state reactive systems. The diagram serves as an abstraction of the system, while its underlying automaton represents the desired temporal behavior. We present two approaches: the use of w-automata (exponential) and alternating automata (linear).
Typisierung in Assemblersprachen mit Explizitem Forwarding

Lennart Beringer
University of Edinburgh, UK
Parallele Ausführung von Instruktionen und Result forwarding sind verbreitete Implementierungstechniken für moderne Prozessoren. In asynchronen Architekturen mit Operandenschlangen führt die gleichzeitige Benutzung beider Konzepte zu Komplikationen wie Deadlock oder Nichtdeterminismus. Um solche Interaktionen besser zu analysieren, führe ich eine Assemblersprache ALEF ein, in der beide Aspekte explizit sichtbar sind. Verschiedene Ausführungsmodelle können als unterschiedliche operationale Semantiken für diese Sprache aufgefaßt werden, und folglich mit programmiersprachlichen Methoden analysiert werden.
Neben sequentieller Ausführung (instruction set architecture) werden wir parallele Ausführung betrachten, sowie Ausführungen, bei denen die Länge der Operandenschlangen begrenzt sind.
Die für das jeweilige Ausführungsmodell auftretenden charakteristischen Fehlersituationen können in Analogie zum Vorgehen bei der Entwicklung von Programmiersprachen durch Typsysteme charakterisiert werden und so zur Compilezeit eliminiert werden. Typen beschreiben dabei Abstraktionen von Laufzeitkonfigurationen, basierend auf Notation aus Linearer Logik.
Die Komponierbarkeit von Basisblöcken wird durch ein einfaches Unifikationsproblem dargestellt, ähnlich zu verwandten Problemen beim Typisieren von JVM code. Sollte die Zeit ausreichen, werde ich kurz Aspekte der Programmanalyse diskutieren, die bei der Übersetzung mit Zielsprache ALEF auftreten.

Zusatzinformationen / Extras


Schnellnavigation zur Seite über Nummerneingabe


Prof. Dr. Peter Pepper
Sprechstd.: keine mehr


Christine Beyer
Raum EN 538
Tel: +49 30 314-22280


mail/tel. vereinbaren


Technische Universität Berlin
Fakultät IV - Elektrotechnik und Informatik - ÜBB
Sekr. EN 13
Raum EN 538
Einsteinufer 17
D-10587 Berlin