No description available.

Master of Science / Department of Computing and Information Sciences / Torben Amtoft / An EFSM (Extended Finite State Machine) is a tuple (S, T, E, V) where S is a finite set of states, T is a finite set of transitions, E is a finite set of events, and V is a finite set of variables. Every transition t in T has a source state and a target state, both in S. There is a need to develop a GUI which aids in building such machines and simulating them so that a slicing algorithm can be implemented on such graphs. This was the main idea of Dr. Torben Amtoft, who has actually written the slicing algorithm and wanted this to be implemented in code. The project aims at implementing a GUI which is effective to simulate and build the graph with minimum user effort. Poor design often fails to attract users. So, the initial effort is to build a simple and effective GUI which serves the purpose of taking input from the user, building graphs and simulating it. The scope of this project is to build and implement an interface so that the users can do the following in an effective way:  Input a specification of an EFSM  Store and later retrieve EFSMs  Displaying an EFSM in a graphical form  Simulating the EFSM  Modify an EFSM  Implement the slicing algorithm All the above mentioned features must be integrated into the GUI and it should only fail if the input specification is wrong.

The Unified Modeling Language (UML) has become the standard language for the design of object-oriented software systems over the past decade. Even though there exist various tools which claim to support design with UML, their functionality is usually focused on drawing UML diagrams and generating code from the UML model. The task of choosing a suitable design which fulfils the requirements still has to be accomplished by the human designer alone. The aim of this thesis is to develop concepts for UML design tools which assist the modeller in improving the system design and requirements incrementally. For this approach a variant of formal games called exploration games is introduced as underlying technique. Exploration games can be defined on the basis of incomplete and imprecise UML models as they occur frequently in practice. The designer repeatedly plays an exploration game to detect flaws or incompleteness in the design and its specification, which are both incorporated in the game definition. At any time the game definition can be incremented by the modeller which allows him to react to the discoveries made during a play and experiment with new design solutions. Exploration games can be applied to UML in different variants. For each variant must be specified how the UML diagrams are used to set up the game and how the semantic variation points of UML should be interpreted. Furthermore some parts of the game definition may not be contained in the UML model and have to be provided separately. The emphasis of this thesis is on game variants which make use of UML diagrams for modelling system behaviour, especially state machines and activity diagrams. A prototypical implementation demonstrates how the concepts developed in this thesis can be put into practice. The tool supports the user in defining, playing and incrementing a game. Moreover it can compute winning strategies for the players and may act as opponent of the modeller. As example a game variant based on UML state machines has been implemented. The architecture that has been chosen for the tool leaves room for extension by additional game variants and alternative algorithms.

This thesis investigates the building of a textual tracing language that operates at the model level to allow trace specification of textually modeled UML constructs. Current tracing approaches focus on manually injecting tracepoints into targeted systems at the source code level. Such approaches are useful in code-centric development styles where the majority of the code is handwritten. However, in the case of Model Driven Development (MDD), where models are utilized to generate some or all of the code, current tracing technology results in low level trace specification and generation of execution traces that are not aware of or linked to the originating model-level constructs. Dynamic analysis hence becomes harder for a modeler adopting an MDD approach. This field, which we call model-oriented tracing, is currently immature, with little pre-existing research. In this thesis, we present a textual model-level tracing language, implemented as part of Umple, that overcomes some of the limitations of existing tracing methods. The language facilitates model-level tracing, in a fashion very similar to code tracing. The language, which we call MOTL (Model-Oriented Tracing Language) allows tracing of UML associations, attributes and state machines. Constraints can be imposed to limit the scope of tracing. As a result of this work, modelers will gain the ability to specify traces of UML constructs at the model level without the need to modify the generated code, and then generate execution traces when the generated system is run. The resulting trace links back to the model constructs. Modelers can choose from among several tracing technologies including basic file or console output, Java logging framework, Log4J and LTTng. This thesis defines the language syntactically and semantically. Model-Driven Development (MDD) and Test-Driven Development (TDD) were followed to implement the language architecture to ensure high quality code generation. MOTL was used in the development in two of Umple subprojects. An empirical evaluation was conducted to evaluate the language’s usability.

Efficient memory access is critical for computing systems, yet the CPU's management of data transfers can create bottlenecks. To counter this, most advanced high-throughput systems utilize Direct Memory Access (DMA) controllers, where peripherals (such as network interfaces and USB devices) can access memory independently of the CPU, improving transfer speeds. However, this bypass also introduces security vulnerabilities if the DMA controller is not configured correctly, as DMA devices may be used to overwrite critical data or leak information. This thesis proposes a method to represent complex DMA driver source code as an abstract mathematical model in the formal analysis tool HOL4 (where users can define models and prove properties about them with HOL4 and checking the correctness of the proofs). This model enables the formal verification of the DMA driver source code's critical properties like memory isolation, initial configurations, and many more. Additionally, the thesis introduces a methodology to convert the verified HOL4 models into executable C source code, thus obtaining a formally verified C source code. The synthesized code is evaluated against the original driver source code by emulating the DMA operation in software and using fuzzing techniques for any compile and runtime errors. This validates the approach, demonstrating that converting a C driver source code into a HOL4 model and then back into C source code after verification yields a formally verified C source code. This thesis applies this methodology to DMA controllers for four devices namely Intel 8237a, Intel IXGBE x550 Ethernet Controller, MPC 5200 SoC, and STM32 DMAC. / Master of Science / This thesis addresses the critical issue of ensuring secure memory access in computing systems, focusing on Direct Memory Access (DMA) controllers. DMA devices can bypass the CPU to access a range of memory directly, enhancing transfer speeds but introducing security vulnerabilities like overwriting or leaking critical data if not configured correctly. This thesis proposes a method to model complex DMA driver source codes such that they can be rigorously analyzed with computer assistance. This approach is significant as it provides a structured methodology for analyzing DMA driver source code, reducing the risk of errors and vulnerabilities. The thesis also proposes a method to convert the abstract representation into executable source code, thus improving the reliability and security of DMA operations in computing systems.

Yes / Kernel P systems have been introduced as a unifying formalism allowing to specify, simulate and analyse various problems. Several applications of this model have been considered and a powerful tool built in order to support their development and analysis. Testing represents an important aspect of any system analysis and correctness. In this paper we introduce for the first time a bounded test generation approach for kernel P systems by considering bounded input sequences. A learning algorithm for kernel P systems is based on learning X-machine models that are equivalent to these systems for sequences of steps up to a certain limit, ℓ. The Lℓ learning algorithm is used. The testing approach is then devised from the inferred X-machines. The method is applied to a case study illustrating the key parts of the approach. / This research was supported by the European Regional Development Fund, Competitiveness Operational Program 2014-2020 through project IDBC (code SMIS 2014+: 121512). Raluca Lefticaru, Savas Konur and Marian Gheorghe have been partially supported by the Royal Society grant IES╲R3╲213176, 2022-2024. The work of Savas Konur is also supported by EPSRC (EP/R043787/1).

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.

Integrated circuit design has progressed significantly over the last few decades. This increasing complexity of hardware systems poses several challenges to the digital hardware verification. Functional verification has become the most expensive and time-consuming task in the overall product development cycle. Almost 70\% of the total verification time is being consumed by design verification and it is projected to worsen further. One of the reasons for this complexity is the synthesis and optimization (automated as well as manual) techniques used to improve performance, area, delay, and other measures have made the final implementation of the design very different from the golden (reference) model. Determining the functional correctness between the reference and implementation using exhaustive simulation can almost always be infeasible. An alternative approach is to prove that the optimized design is functionally equivalent to the reference model, which is known to be functionally correct. The most widely used formal method to perform this process is equivalence checking. The success of combinational equivalence checking (CEC) has contributed to aggressive combinational logic synthesis and optimizations for circuits with millions of logic gates. However, without powerful sequential equivalence checking (SEC) techniques, the potential and extent of sequential optimization is quite limited. In other words, the success of SEC can unleash a plethora of aggressive sequential optimizations that can take circuit design to the next level. Currently, SEC remains extremely difficult compared to CEC, due to the huge search space of the problem. Sequential Equivalence Checking remains a challenging problem, in this thesis we address the problem using efficient learning techniques. The first approach is to mine missing multi-node patterns from the mining database, verify them and add those proved as true during the unbounded SEC framework. The second approach is to mine powerful and generalized Boolean relationships among flip-flops and internal signals in a sequential circuit using a data mining algorithm. In contrast to traditional learning methods, our mining algorithms can extract illegal state cubes and inductive invariants. These invariants can be arbitrary Boolean expressions and can help in pruning a large don't-care space for equivalence checking. The two approaches are complementary to each other in nature. One computes the subset of illegal states that cannot occur in the normal function mode and the other approach mines legal constraints that represent the characteristics of the miter circuit and can never be violated. These powerful relations, when added as new constraint clauses to the original formula, help to significantly increase the deductive power for the SAT engine, thereby pruning a larger portion of the search space. Likewise, the memory required and time taken to solve the SEC problem is alleviated. / Master of Science

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> </p><p>MTsim (Mobile Traffic Simulator) is an Ericsson AB internal software application that is part of 2Gsim. It is used to simulate elements of a GSM (Global System for Mobile communications) network for feature testing and automated testing. It is written in the programming language TSS Language, also known as SMILE which is a proprietary Ericsson programming language. SMILE is based on the principles of state matrix programming which in essence means that each program is on its own a finite state machine. The language is old and was originally intended as a macro language for smaller test programs, not for applications the size of MTsim.</p><p>It is of interest to evaluate the feasibility of performing an automatic conversion of applications written in SMILE, with special interest in converting MTsim, to a Java framework since Java has many advantages compared to SMILE. Java, as a language, is well suited for larger applications, there are numerous well supported tools and there is a much wider spread competence than there is for SMILE.</p><p>It is clear that in order to do a full conversion of a SMILE program to a Java framework two applications must be implemented. First a Java framework, which acts as a run time environment, must be designed which can host the translated programs. The other part is an actual translator which takes a SMILE program as input and ouputs a translated Java program. A more sophisticated framework is preferred since it makes the actual translated programs more light weight and easy to read which means higher degree of maintainability.</p><p>There are different ways to implement state machines in Java but the most flexible and versatile is to implement it as a black-box framework in an object oriented way where the framework has sophisticated mechanisms for message and event handling which is central to any state machine framework.</p><p>The translation for SMILE can easily be done by using a AST (abstract syntax tree) representation, which is a full representation of the SMILE program in tree-form. The AST is obtained from an intermediate state of the SMILE program compiler.</p><p> </p>