| 1. |
- Broman, David, 1977-
(författare)
-
Meta-Languages and Semantics for Equation-Based Modeling and Simulation
- 2010
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Performing computational experiments on mathematical models instead of building and testing physical prototypes can drastically reduce the develop cost for complex systems such as automobiles, aircraft, and powerplants. In the past three decades, a new category of equation-based modeling languages has appeared that is based on acausal and object-oriented modeling principles, enabling good reuse of models. 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. This thesis concerns the problem of designing the semantics of such equation-based modeling languages in a way that allows formal reasoning and increased correctness. The work is presented in two parts.In the first part we study the state-of-the-art modeling language Modelica. We analyze the concepts of types in Modelica and conclude that there are two kinds of type concepts: class types and object types. Moreover, a concept called structural constraint delta is proposed, which is used for isolating the faults of an over- or under-determined model.In the second part, we introduce a new research language called the Modeling Kernel Language (MKL). 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.
|
|
| 2. |
- Natarajan, Saranya
(författare)
-
Programming Language Primitives and Tools for Integrated Real-Time Systems Development
- 2021
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- The correctness of real-time systems depends on both its logical and temporal correctness. Typically, real-time systems are developed in several steps. First, the application is divided into a number of recurrent tasks and implemented using a programming language. Second, the worst-case execution time (WCET) of each task is estimated for a specific hardware platform. Finally, schedulability analysis is performed to determine if the timing requirements are met on the specified hardware. There are several challenges in each of these complex steps, as well as how to integrate them in a systematic way. Moreover, many small-scale embedded systems are implemented using the C programming language. However, the C programming language has no direct primitives for programming the system’s temporal requirements. Similarly, the uncertainties in the measured WCET values and the release jitter can render the result of the schedulability analysis unreliable. Further, the practical differences in the tools used in each of these steps make the integrated development of real-time systems challenging. In this dissertation, we propose a set of programming primitives and tools for the integrated development of real-time systems. More specifically, we propose a small number of language primitives for programming timing, concurrency, and scheduling requirements of real-time systems. We introduce Timed C, a programming language for real-time systems that extends the C programming language with the proposed language primitives. We propose a seamless and pragmatic end-to-end toolchain that integrates the Timed C programming language, a source-to-source compiler, timing analysis, schedulability analysis, and a novel sensitivity analysis. The new approach to sensitivity analysis determines the worst-case execution time margins for weakly-hard real-time systems. We formalize a subset of the Timed C semantics and use this to design a new temporal property-based testing tool and methodology. Finally, we evaluate the proposed programming language and tools using experiments and case studies.
|
|
| 3. |
- Gustavsson, Andreas, 1982-
(författare)
-
Static Execution Time Analysis of Parallel Systems
- 2016
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- The past trend of increasing processor throughput by increasing the clock frequency and the instruction level parallelism is no longer feasible due to extensive power consumption and heat dissipation. Therefore, the current trend in computer hardware design is to expose explicit parallelism to the software level. This is most often done using multiple, relatively slow and simple, processing cores situated on a single processor chip. The cores usually share some resources on the chip, such as some level of cache memory (which means that they also share the interconnect, e.g., a bus, to that memory and also all higher levels of memory). To fully exploit this type of parallel processor chip, programs running on it will have to be concurrent. Since multi-core processors are the new standard, even embedded real-time systems will (and some already do) incorporate this kind of processor and concurrent code.A real-time system is any system whose correctness is dependent both on its functional and temporal behavior. For some real-time systems, a failure to meet the temporal requirements can have catastrophic consequences. Therefore, it is crucial that methods to derive safe estimations on the timing properties of parallel computer systems are developed, if at all possible.This thesis presents a method to derive safe (lower and upper) bounds on the execution time of a given parallel system, thus showing that such methods must exist. The interface to the method is a small concurrent programming language, based on communicating and synchronizing threads, that is formally (syntactically and semantically) defined in the thesis. The method is based on abstract execution, which is itself based on abstract interpretation techniques that have been commonly used within the field of timing analysis of single-core computer systems, to derive safe timing bounds in an efficient (although, over-approximative) way. The thesis also proves the soundness of the presented method (i.e., that the estimated timing bounds are indeed safe) and evaluates a prototype implementation of it.
|
|
| 4. |
- Jonsson, Leif, 1973-
(författare)
-
Machine Learning-Based Bug Handling in Large-Scale Software Development
- 2018
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- This thesis investigates the possibilities of automating parts of the bug handling process in large-scale software development organizations. The bug handling process is a large part of the mostly manual, and very costly, maintenance of software systems. Automating parts of this time consuming and very laborious process could save large amounts of time and effort wasted on dealing with bug reports. In this thesis we focus on two aspects of the bug handling process, bug assignment and fault localization. Bug assignment is the process of assigning a newly registered bug report to a design team or developer. Fault localization is the process of finding where in a software architecture the fault causing the bug report should be solved. The main reason these tasks are not automated is that they are considered hard to automate, requiring human expertise and creativity. This thesis examines the possi- bility of using machine learning techniques for automating at least parts of these processes. We call these automated techniques Automated Bug Assignment (ABA) and Automatic Fault Localization (AFL), respectively. We treat both of these problems as classification problems. In ABA, the classes are the design teams in the development organization. In AFL, the classes consist of the software components in the software architecture. We focus on a high level fault localization that it is suitable to integrate into the initial support flow of large software development organizations.The thesis consists of six papers that investigate different aspects of the AFL and ABA problems. The first two papers are empirical and exploratory in nature, examining the ABA problem using existing machine learning techniques but introducing ensembles into the ABA context. In the first paper we show that, like in many other contexts, ensembles such as the stacked generalizer (or stacking) improves classification accuracy compared to individual classifiers when evaluated using cross fold validation. The second paper thor- oughly explore many aspects such as training set size, age of bug reports and different types of evaluation of the ABA problem in the context of stacking. The second paper also expands upon the first paper in that the number of industry bug reports, roughly 50,000, from two large-scale industry software development contexts. It is still as far as we are aware, the largest study on real industry data on this topic to this date. The third and sixth papers, are theoretical, improving inference in a now classic machine learning tech- nique for topic modeling called Latent Dirichlet Allocation (LDA). We show that, unlike the currently dominating approximate approaches, we can do parallel inference in the LDA model with a mathematically correct algorithm, without sacrificing efficiency or speed. The approaches are evaluated on standard research datasets, measuring various aspects such as sampling efficiency and execution time. Paper four, also theoretical, then builds upon the LDA model and introduces a novel supervised Bayesian classification model that we call DOLDA. The DOLDA model deals with both textual content and, structured numeric, and nominal inputs in the same model. The approach is evaluated on a new data set extracted from IMDb which have the structure of containing both nominal and textual data. The model is evaluated using two approaches. First, by accuracy, using cross fold validation. Second, by comparing the simplicity of the final model with that of other approaches. In paper five we empirically study the performance, in terms of prediction accuracy, of the DOLDA model applied to the AFL problem. The DOLDA model was designed with the AFL problem in mind, since it has the exact structure of a mix of nominal and numeric inputs in combination with unstructured text. We show that our DOLDA model exhibits many nice properties, among others, interpretability, that the research community has iden- tified as missing in current models for AFL.
|
|
