Dieser Bericht präsentiert RACR-NET, eine Schnittstelle der Referenzattributgrammatik-gesteuerten Graphersetzungsbibliothek RACR für C#. RACR-NET ermöglicht die Nutzung der deklarativen, dynamischen Sprachspezifikations-, Instanziierungs- und Auswertungsmeachanismen der RACR Scheme-Bibliothek in der objektorientierten Programmierung. Dies umfasst insbesondere die automatische inkrementelle Auswertung attributbasierter semantischer Analysen und somit das automatische Cachen parametrisierter Funktionsmethoden. Graphersetzungen entsprechen hierbei Zustandsänderungen von Objektinstanzen und der Invalidierung abgeleiteter Berechnungen. Schwerpunkt dieses Berichts ist die objektorientierte Programmierschnittstelle von RACR-NET, dessen praktische Anwendung und Implementierung. Der Bericht ist ein Referenzhandbuch für RACR-NET Anwender und Entwickler.:1. Einleitung 1.1. Aufgabenstellung 1.2. Struktur der Arbeit 2. Konzeptionelle und technische Voraussetzungen 2.1. Überblick der RAG-gesteuerten Graphersetzung 2.2. Scheme 2.3. Die RACR Scheme-Bibliothek 2.4. Das .NET-Framework und die Common Language Infrastructure 2.5. IronScheme 3. RACR-NET Implementierung: Prozedurale Schnittstelle 3.1. Scheme in C# 3.2. RACR in C# 3.3. Anforderungsanalyse 3.4. Implementierung der prozeduralen Schnittstelle 4. RACR-NET Implementierung: Objektorientierte Schnittstelle 4.1. Überblick über die objektorientierte Schnittstelle 4.2. Anwendungsbeispiel 4.3. Herausforderungen bei der Implementierung 4.4. Implementierung 5. Evaluation 5.1. Testen der Schnittstelle 5.2. Performance-Messungen und -Vergleiche 6. Zusammenfassung und Ausblick 6.1. Eine objektorientierte Bibliothek für RAG-gesteuerte Graphersetzung 6.2. Zukünftige Arbeiten A. Literaturverzeichnis B. MIT Lizenz

We present a formal modeling approach for the design and simulation of Multi-Unmanned Aerial Vehicle (multi-UAV) inspection scenarios, where planning is based on model checking. As demonstration, we formalize and simulate a compositional UAV inspection system of a solar park using bigraphical reactive systems, which introduce the notion of time-varying bigraphs. Specifically, the UAV system is modeled as a process-algebraic expression, whose semantics is a bigraph state in a labeled transition system. The underlying Multi-Agent Path Finding problem is solved model-theoretically using Planning-by-Model-Checking. It solves the inherently connected collision-free path planning problem for multiple UAVs subject to contexts and local conditions. First, a bigraph is constructed algebraically, which can be decomposed systematically into separate parts with interfaces. The layered composite model accounts for location, navigation, UAVs, and contexts, which enables simple configuration and extension (changeability). Second, the executable operational semantics of our formal bigraph model are given by bigraphical reactive systems, where rules constitute the behavioral component of our model. Rules reconfigure the bigraph to simulate state changes, i.e., they allow to alter the conditions under which UAVs are permitted to move. Properties can be attached to nodes of the bigraph and evaluated in a simulation over the traces of the transition system according to some cost-based policies. In essence, the inherent multi-UAV path planning problem of our scenario is formulated as a reachability problem and solved by model checking the generated transition system. The bigraph-algebraic expression also allows us to reason about potential parallelization opportunities when moving UAVs. Moreover, we sketch how to directly simulate the bigraph specification in a ROS-based Gazebo simulation by examining the inspection and monitoring of a solar park as an application. The reactive system specification provides the blueprint for analysis, simulation, implementation and execution. Thus, the same algorithm used for verification is used as well for the simulation in ROS/Gazebo to execute plans.:1 Introduction 2 Overview: Scenario Description and Formal Modeling Approach 3 Background: Bigraphs and Model Checking 4 Construction of the UAV System via Composition 5 Making the Drones Fly: Executable Model Semantics 6 Collision-Free Path Planning Problem 7 Prototypical Implementation 8 Discussion 9 Related Work 10 Conclusion A UAV State Machine B Bigraphical Reactive Systems C RPO/IPO Semantic

Synchronous languages such as Signal, Lustre and Esterel are dedicated to designing safety-critical systems. Their compilers are large and complicated programs that may be incorrect in some contexts, which might produce silently bad compiled code when compiling source programs. The bad compiled code can invalidate the safety properties that are guaranteed on the source programs by applying formal methods. Adopting the translation validation approach, this thesis aims at formally proving the correctness of the highly optimizing and industrial Signal compiler. The correctness proof represents both source program and compiled code in a common semantic framework, then formalizes a relation between the source program and its compiled code to express that the semantics of the source program are preserved in the compiled code.

Les langages synchrones tels que Signal, Lustre et Esterel sont dédiés à la conception de systèmes critiques. Leurs compilateurs, qui sont de très gros programmes complexes, peuvent a priori se révéler incorrects dans certains situations, ce qui donnerait lieu alors à des résultats de compilation erronés non détectés. Ces codes fautifs peuvent invalider des propriétés de sûreté qui ont été prouvées en appliquant des méthodes formelles sur les programmes sources. En adoptant une approche de validation de la traduction, cette thèse vise à prouver formellement la correction d'un compilateur optimisé et industriel de Signal. La preuve de correction représente dans un cadre sémantique commun le programme source et le code compilé, et formalise une relation entre eux pour exprimer la préservation des sémantiques du programme source dans le code compilé. / Synchronous languages such as Signal, Lustre and Esterel are dedicated to designing safety-critical systems. Their compilers are large and complicated programs that may be incorrect in some contexts, which might produce silently bad compiled code when compiling source programs. The bad compiled code can invalidate the safety properties that are guaranteed on the source programs by applying formal methods. Adopting the translation validation approach, this thesis aims at formally proving the correctness of the highly optimizing and industrial Signal compiler. The correctness proof represents both source program and compiled code in a common semantic framework, then formalizes a relation between the source program and its compiled code to express that the semantics of the source program are preserved in the compiled code.

This report presents RACR, a reference attribute grammar library for the programming language Scheme. RACR supports incremental attribute evaluation in the presence of abstract syntax tree rewrites. It provides a set of functions that can be used to specify abstract syntax tree schemes and their attribution and construct respective trees, query their attributes and node information and annotate and rewrite them. Thereby, both, reference attribute grammars and rewriting, are seamlessly integrated, such that rewrites can reuse attributes and attribute values change depending on performed rewrites – a technique we call Reference Attribute Grammar Controlled Rewriting. To reevaluate attributes influenced by abstract syntax tree rewrites, a demand-driven, incremental evaluation strategy, which incorporates the actual execution paths selected at runtime for control-flows within attribute equations, is used. To realize this strategy, a dynamic attribute dependency graph is constructed throughout attribute evaluation – a technique we call Dynamic Attribute Dependency Analyses. The report illustrates RACR's motivation, features, instantiation and usage. In particular its application programming interface is documented and exemplified. The report is a reference manual for RACR developers. Further, it presents RACR’s complete implementation and therefore provides a good foundation for readers interested into the details of reference attribute grammar controlled rewriting and dynamic attribute dependency analyses.:1. Introduction 1.1. RACR is Expressive, Elegant, Ecient, Flexible and Reliable 1.2. Structure of the Manual 2. Library Overview 2.1. Architecture 2.2. Instantiation 2.3. API 3. Abstract Syntax Trees 3.1. Specification 3.2. Construction 3.3. Traversal 3.4. Node Information 4. Attribution 4.1. Specification 4.2. Evaluation and Querying 5. Rewriting 5.1. Primitive Rewrite Functions 5.2. Rewrite Strategies 6. AST Annotations 6.1. Attachment 6.2. Querying 7. Support API A. RACR Source Code B. MIT License API Index