This dissertation addresses the problem of making system level design (SLD) methodology based on SystemC more useful to the complex embedded system design community by presenting a number of ingredients currently absent in the existing SLD methodologies and frameworks. The complexity of embedded systems have been increasing at a rapid rate due to proliferation of desired functionality of such systems (e.g., cell phones, game consoles, hand-held devices, etc., are providing more features every few months), and the device technology still riding the curve predicted by Moore's law. Design methodology is shifting slowly towards system level design (also called electronic system level (ESL)). A number of SLD languages and supporting frameworks are being proposed. SystemC is positioned as being one of the dominant SLD languages. The various design automation tool vendors are proposing frameworks for supporting SystemC-based design methodologies. We believe that compared to the necessity and potential of ESL, the success of the frameworks have been limited due to lack of support for a number of facilities and features in the languages and tool environments. This dissertation proposes, formulates, and provides proof of concept demonstrations of a number of ingredients that we have identified as essential for efficient and productive use of SystemC-based tools and techniques. These are heterogeneity in the form of multiple models of computation, behavioral hierarchy in addition to structural hierarchy, model-driven validation for SystemC designs and a service-oriented tool integration environment. In particular, we define syntactic extensions to the SystemC language, semantic modifications, and simulation algorithms, precise semantics for model based validation etc. For each of these we provide reference implementation for further experimentation on the utility of these extensions. / Ph. D.

Mit der aktuellen Überarbeitung der Sprache SDL (Specification and Description Language) der ITU-T wurde die semantische Fundierung der formalen Definition dieser Sprache vollständig überarbeitet; die formale Definition basiert nun auf dem Kalkül der Abstract State Machines (ASMs). Ebenfalls neu definiert wurde das um objekt-orientierte Konzepte erweiterte Datentypsystem. Damit musste eine formale semantische Fundierung für diese neuen Konzepte gefunden werden. Der bisher verwendete Kalkül ACT.ONE sollte nicht mehr verwendet werden, da er schwer verwendbar, nicht implementierbar und nicht auf Objektsysteme erweiterbar ist. In der vorliegenden Arbeit werden die Prinzipien einer formalen Sprachdefinition dargelegt und die Umsetzung dieser Prinzipien für die Sprache SDL-2000 vorgestellt. Dabei wird erläutert, dass eine konsistente Sprachdefinition nur dadurch erreicht werden konnte, dass die Definition der formalen Semantik der Sprache parallel mit der Entwicklung der informalen Definition erfolgte. Dabei deckt die formale Sprachdefinition alle Aspekte der Sprache ab: Syn-tax, statische Semantik und dynamische Semantik. Am Beispiel der Datentypsemantik wird erläutert, wie jeder dieser Aspekte informal beschrieben und dann formalisiert wurde. Von zentraler Rolle für die Anwendbarkeit der formalen Semantikdefinition in der Praxis ist der Einsatz von Werkzeugen. Die Arbeit erläutert, wie aus der formalen Sprachdefinition voll-automatisch ein Werkzeug generiert wurde, das die Sprache SDL implementiert, und wie die durch die Umsetzung der formalen Semantikdefinition in ein Werkzeug Fehler in dieser Definition aufgedeckt und behoben werden konnten. / With the latest revision of ITU-T SDL (Specification and Description Language), the semantic foundations of the formal language definition were completely revised; the formal definition is now based on the calculus of Abstract State Machines (ASMs). In addition, the data type system of SDL was revised, as object-oriented concepts were added. As a result, a new semantical foundation for these new concepts had to be defined. The ACT.ONE calculus that had been used so far was not suitable as a foundation any more, as it is hard to use, unimplementable and not extensible for the object oriented features. In this thesis, we elaborate the principles of a formal language definition, and the realisation of these principles in SDL-2000. We explains that a consistent language definition can only be achieved by developing the formal semantics definition in parallel with the development of the informal definition. The formal language definition covers all aspects of the language: syntax, static semantics, and dynamic semantics. Using the data type semantics as an example, we show how each of these aspects is informally described, and then formalized. For the applicability of the formal semantics definition for practitioners, usage of tools plays a central role. We explain how we transform the formal language definition fully automatically into a tool that implements the language SDL. We also explain how creating the tool allowed us to uncover and correct errors in the informal definition.

<p>This Ph.D. thesis addresses topics related to overlay networks, their de_nition,<br />formalization and applications. Descriptions of the Chord and Synapse protocols using<br />the ASM formalism is presented, and both a high-level and a re_ned proof of the<br />correctness of the Chord formalization is given. A probabilistic assessment of the<br />exhaustiveness of the Synapse protocol is performed. An updated version of the<br />Proposal of metadata schemata for movable cultural heritage as well as a Proposal of<br />metadata schemata for describing collections are provided. Based of the Chord protocol, a Distributed catalog of digitized collections of Serbian cultural herigate is implemented.</p> / <p>Doktorska disertacija se bavi temama vezanim za prekrivajuće mreže, njihovom<br />definicijom, formalizacijom i primenama. Dati su opisi Chord i Synapse protokola<br />kori&scaron;ćenjem ASM formalizma, kao i dokaz korektnosti formalizacije Chord protokola<br />na visokom nivou, kao i njegovo profinjenje. Izvr&scaron;ena je verovatnosna ocena uspe&scaron;nosti pretrage pomoću Synapse protokola. Predstavljena je ažurirana verzija Predloga sheme meta podataka za pokretna kulturna dobra, kao i Predlog sheme meta podataka za opis kolekcija. Implementiran je Distribuirani katalog digitalizovanih kolekcija kulturne ba&scaron;tine Srbije zasnovan na Chord protokolu.</p>

Dans cette thèse nous proposons un modèle temporel dans le cadre des machines à états abstraits (ASM). Une extension du langage de spécification ASM est développé qui correspond à ce modéle temporel pour le temps continu. L'extension du langage avec des constructions de temps permet de diminuer la taille de la spécification et donc de réduire la probabilité d'erreurs. La sémantique de l'extension du langage ASM est fournie et prend en compte les définitions des fonctions externes, les valeurs des délais et les choix de résolution des non-déterminismes. Un sous-système de vérification des propriétés exprimées en logique FOTL (FirstOrder Timed Logic) est développé. Un simulateur d'ASMs temporisées est développé et implémenté, il comprend un analyseur syntaxique, un interprète du langage, un sous-système de vérification des propriétés ainsi qu'une interface graphique / In this thesis a temporal model for abstract state machines (ASM) method is pro- posed. An extension of ASM specification language on the base of the proposed temporal model with continuous time is developed. The language extension helps to reduce the size of the specification hence to diminish the probability of an error. The semantics of the extended ASM language is developed which takes into account the definitions of external functions, the values of time delays and the method of non-determinism resolving. A subsystem for verification of user properties in the FOTL language is developed. A simulator prototype for ASMs with time is developed and implemented. It includes the parser of the timed ASM language, the interpreter, the verification subsystem and the graphical user interface

In dieser Habilitationsschrift wird die formale Semantik der standardisierten Spezifikationssprache SDL (Specification and Description Language) beschrieben. Da SDL eine sehr umfangreiche Sprache ist, wurde eine repräsentative eingeschränkte Sprache RSDL (Restricted SDL) ausgewählt, um die Konzepte der formalen Definition von SDL darzustellen. Die vorliegende Habilitationsschrift umfaßt zwei große Teile: die Definition der formalen Semantik von RSDL und ihre Implementierung. Die formale Definition der Semantik von RSDL ist verständlich, leicht mit der informalen Beschreibung zu vergleichen und repräsentiert die grundsätzliche Vorstellung von RSDL. Für die Beschreibung werden zwei Teile unterschieden, nämlich die statische Semantik und die dynamische Semantik. Die statische formale Sprachdefinition besteht aus einer konkreten Syntax, einer Menge von Korrektheitsbedingungen, einer Menge von Transformationsregeln und einer abstrakten Syntax als Basis für die dynamische Semantik. Das Ergebnis der statischen Beschreibung ist eine Repräsentation der Spezifikation in abstrakter Syntax. Die Formalisierung der dynamischen Semantik beginnt mit der abstrakten Syntax. Aus dieser abstrakten Syntax wird ein Verhaltensmodell abgeleitet, das auf der mathematischen Theorie der Abstrakten Zustandmaschinen ASM (Abstract State Machines) basiert. Um die Definition der Semantik besonders übersichtlich zu gestalten, wird eine Spezielle Abstrakte Maschine (SAM) unter Nutzung von ASM definiert. Diese abstrakte Maschine stellt eine abstrakte SDL-Maschine dar. Die formale Semantik beschreibt die Eigenschaften von SDL exakt. Um jedoch herauszufinden, ob die Semantik korrekt ist, muß sie mit der Sprachbeschreibung und den Intentionen der Sprachentwickler verglichen werden. Dies geschieht am einfachsten durch eine korrekte Implementierung der Semantik. Die Implementierung der formalen Semantik basiert auf einer Repräsentation der Eingabe als abstrakter Syntaxbaum. Um die Semantik mit minimalem Aufwand zu implementieren, werden existierende Werkzeuge verwendet. Der Compiler wird mit den Standardwerkzeugen lex und yacc generiert. Nach der Syntaxanalyse wird die weitere Verarbeitung über dem abstrakten Syntaxbaum der Eingabe definiert. Die Verarbeitung von abstrakten Syntaxbäumen wird durch ein Werkzeug namens kimwitu erledigt. Mit der hier vorgestellten Technologie wurde die formale Semantik von RSDL implementiert. Entsprechend wird die formale Semantik von SDL implementiert. / In this habilitation thesis the formal semantics of the standardised specification language SDL (Specification and Description Language) is described. Because of the size of the language SDL a representative subset of the language called RSDL (Restricted SDL) was selected to present the concepts of the formal definition. In this thesis two major parts are covered: the definition of the formal semantics and its implementation. The RSDL formal semantics is intelligible, easily comparable with the informal description and represents the general understanding of RSDL. We distinguish between two phases of the definition, namely the static semantics and the dynamic semantics. The static semantics comprises the definition of a concrete grammar, a set of correctness constraints, a set of transformation rules and an abstract syntax as basis for the dynamic semantics. The result of the static semantics is a representation of the specification in abstract syntax. The dynamic semantics starts with the abstract syntax. From here a behaviour model is derived based on the theory of Abstract State Machines (ASM). In order to keep the presentation intelligible a special abstract machine is defined using ASM. This abstract machine in fact represents an abstract SDL-machine. The formal semantics describes the properties of SDL exactly. However, in order to check the correctness of the formalisation, it has to be compared with the informal language description and the intentions of the language designers. This is most easily done using a correct implementation of the semantics. The implementation of the semantics is based on a representation of the input as an abstract syntax tree. For implementing the semantics with minimal effort existing tools are used. The compiler is produced using the standard tools lex and yacc. After parsing the remaining processing is defined over abstract syntax trees, which is covered by a tool called kimwitu. The formal semantics of RSDL is implemented using these tools. The same approach is applicable for SDL.