The development of high integrity embedded systems remains an arduous and error-prone task, despite the efforts by researchers in inventing tools and techniques for design automation. Much of the problem arises from the fact that the semantics of the modeling languages for the various tools, are often distinct, and the semantics gaps are often filled manually through the engineer's understanding of one model or an abstraction. This provides an opportunity for bugs to creep in, other than standardizing software engineering errors germane to such complex system engineering. Since embedded systems applications such as avionics, automotive, or industrial automation are safety critical, it is very important to invent tools, and methodologies for safe and reliable system design. Much of the tools, and techniques deal with either the design of embedded platforms (hardware, networking, firmware etc), and software stack separately. The problem of the semantic gap between these two, as well as between models of computation used to capture semantics must be solved in order to design safer embedded systems. In this dissertation we propose a methodology for the end-to-end modeling and analysis of safety-critical embedded systems. Our approach consists of formal platform modeling, and analysis; formal application modeling; and 'correct-by-construction' code synthesis with the aim of bridging semantic gaps between the various abstractions and models required for the end-to-end system design. While the platform modeling language AADL has formal semantics, and analysis tools for real-time, and performance verification, the application behavior modeling in AADL is weak and part of an annex. In our work, we create the APECS (AADL and Polychrony based Embedded Computing Synthesis) methodology to allow an embedded system design specification all the way from platform architecture and platform components, the real-time behavior, non-functional properties, as well as the application software modeling. Our main contribution is to integrate a polychronous application software modeling language, and synthesis algorithms in order for synthesis of the embedded software running on the target platform, with the required constraints being met. We believe that a polychronous approach is particularly well suited for a multiprocessor/multi-controller distributed platform where different components often operate at independent rates and concurrently. Further, the use of a formal polychronous language will allow for formal validation of the software prior to code generation. We present a prototype framework that implements this approach, which we refer to as the AADL and Polychrony based Embedded Computing System (APECS). Our prototype utilizes an extended version of Ocarina to provide code generation for the AADL model. Our polychronous modeling language is MRICDF. Our prototype extends Ocarina to support software specification in MRICDF and generate multi-threaded software. Additionally, we implement an automated translation from Simulink to MRICDF, allowing designers to benefit from its formal semantics and exploit engineers' familiarity with Simulink tools, and legacy models. We present case studies utilizing APECS to implement safety critical systems both natively in MRICDF and in Simulink through automated translation. / Ph. D.

For maximal market penetration, popular mobile applications are typically supported on all major platforms, including Android and iOS. Despite the vast differences in the look-and-feel of major mobile platforms, applications running on these platforms in essence provide the same core functionality. As an application is maintained and evolved, programmers need to replicate the resulting changes on all the supported platforms, a tedious and error-prone programming process. Commercial automated source-to-source translation tools prove inadequate due to the structural and idiomatic differences in how functionalities are expressed across major platforms. In this thesis, we present a new approach---Native-2-Native---that automatically synthesizes code for a mobile application to make use of native resources on one platform, based on the equivalent program transformations performed on another platform. First, the programmer modifies a mobile application's Android version to make use of some native resource, with a plugin capturing code changes. Based on the changes, the system then parameterizes a web search query over popular programming resources (e.g., Google Code, StackOverflow, etc.), to discover equivalent iOS code blocks with the closest similarity to the programmer-written Android code. The discovered iOS code block is then presented to the programmer as an automatically synthesized Swift source file to further fine-tune and subsequently integrate in the mobile application's iOS version. Our evaluation, enhancing mobile applications to make use of common native resources, shows that the presented approach can correctly synthesize more than 86% of Swift code for the subject applications' iOS versions. / Master of Science

To increase market penetration, mobile software makers support their popular applications on all major software platforms, which currently include Android, iOS, and Windows Phone. Although these platforms often offer a drastically different look and feel, cross-platform applications deliver the same core functionality to the end user. Maintaining and evolving such applications currently requires replicating all the changes across all supported variants, a laborious and intellectually taxing enterprise. The state-of-the-practice automated source translation tools fall short, as they are incapable of handling the structural and idiomatic differences of the software frameworks driving major mobile platforms. In addition, popular mobile applications increasingly make use of distributed resources. Certain domains, including social networking, productivity enhancement, and gaming, require different application instances to continuously exchange information with each other. The current state of the art in supporting communication across heterogeneous mobile devices requires the programmer to write platform-specific, low-level API calls that are hard not only to develop but also to evolve and maintain. This thesis reports on the findings of two complementary research activities, conducted with the goal of facilitating the development and communication across heterogeneous mobile devices: (1) a programming model and runtime support for heterogeneous device-to-device communication across mobile applications; (2) a source code recommendation system that synthesizes code snippets from web-based programming resources, based on the functionality written for Android or iOS and vice versa. The conceptual and practical advancements of this research have potential to benefit fellow researchers as well as mobile software developers and users. / Master of Science

Pour réduire les coûts des systèmes embarqués, ces derniers sont livrés avec des micro-processeurs peu puissants. Ces processeurs sont dédiés à l'exécution de tâches calculatoires dont certaines, comme la transformée de Fourier rapide, peuvent s'avérer exigeantes en termes de ressources de calcul. Afin que les implémentations de ces algorithmes soient efficaces, les programmeurs utilisent l'arithmétique à virgule fixe qui est plus adaptée aux processeurs dépourvus d'unité flottante. Cependant, ils se retrouvent confrontés à deux difficultés: D'abord, coder en virgule fixe est fastidieux et exige que le programmeur gère tous les détails arithmétiques. Ensuite, et en raison de la faible dynamique des nombres à virgule fixe par rapport aux nombres flottants, les calculs en fixe sont souvent perçus comme intrinsèquement peu précis. La première partie de cette thèse propose une méthodologie pour dépasser ces deux limitations. Elle montre comment concevoir et mettre en œuvre des outils pour générer automatiquement des programmes en virgule fixe. Ensuite, afin de rassurer l'utilisateur quant à la qualité numérique des codes synthétisés, des certificats sont générés qui fournissent des bornes sur les erreurs d'arrondi. La deuxième partie de cette thèse est dédiée à l'étude des compromis lors de la génération de programmes en virgule fixe pour les briques d'algèbre linéaire. Des données expérimentales y sont fournies sur la synthèse de code pour la multiplication et l'inversion matricielles. / To be cost effective, embedded systems are shipped with low-end micro-processors. These processors are dedicated to one or few tasks that are highly demanding on computational resources. Examples of widely deployed tasks include the fast Fourier transform, convolutions, and digital filters. For these tasks to run efficiently, embedded systems programmers favor fixed-point arithmetic over the standardized and costly floating-point arithmetic. However, they are faced with two difficulties: First, writing fixed-point codes is tedious and requires that the programmer must be in charge of every arithmetical detail. Second, because of the low dynamic range of fixed-point numbers compared to floating-point numbers, there is a persistent belief that fixed-point computations are inherently inaccurate. The first part of this thesis addresses these two limitations as follows: It shows how to design and implement tools to automatically synthesize fixed-point programs. Next, to strengthen the user's confidence in the synthesized codes, analytic methods are suggested to generate certificates. These certificates can be checked using a formal verification tool, and assert that the rounding errors of the generated codes are indeed below a given threshold. The second part of the thesis is a study of the trade-offs involved when generating fixed-point code for linear algebra basic blocks. It gives experimental data on fixed-point synthesis for matrix multiplication and matrix inversion through Cholesky decomposition.

Researchers use datasets of Question-Solution pairs to train machine learning models, such as source code generation models. A Question-Solution pair contains two parts: a programming question and its corresponding Solution Snippet. A Solution Snippet is a source code that solves a programming question. These datasets of Question-Solution pairs can be extracted from a number of different platforms. In this research, I study how Question-Solution pairs are extracted from Stack Overflow (SO). There are two limitations of datasets of Question-Solution pairs extracted from SO: (1) according to the authors of these datasets, some Question-Solution pairs contain Solution Snippets that do not solve the question correctly, and (2) these datasets do not contain the information on how Solution Snippets need to be reused, and such information would enhance the reusability of Solution Snippets. These limitations of datasets of pairs could adversely affect the quality of the code being generated by machine learning models. In this research, I conducted a qualitative study to categorize various presentations of Solution Snippets in SO’s answers as well as how Solution Snippets can be adapted for reuse. By doing so, I identified eight categories of how Solution Snippets are presented in SO’s answers and five categories of how Solution Snippets could be adapted. Based on these results, I concluded several potential reasons why it is not easy to create datasets of Question-Solution pairs. The first categorization informs that finding the correct location of the Solution Snippet is challenging when there are several code blocks within the answer to the question. Subsequently, the researcher must identify which code within that code block is the Solution Snippet. The second categorization informs that most Solution Snippets appear challenging to be adapted for reuse, and how Solution Snippets are potentially adapted is not explicitly stated in them. These insights shed light on creating better quality datasets from questions and answers posted on Stack Overflow. / Graduate

Heterogeneous platforms, systems with both general-purpose processors and task-specific hardware, are largely used in industry to increase efficiency, but the heterogeneity also increases the difficulty of design and verification. We often need to wait for the completion of all the modules to know whether the functionality of the design is correct or not, which can cause costly and tedious design iteration cycles. Correctness by construction is a methodology that proposes tackling this problem by separating specification and implementation and bridging them through formal methods. Code synthesis is one of these methods which refers to the process of generating low-level codes implementing the desired system from high-level modelling languages. Formulating a generic synthesis method can, in principle, decrease error rates and shorten development cycles since target-specific usage and mechanisms can be systematically taken care of in an automatic manner, whereas the designer needs only to ensure the functional correctness of the high-level specification model. In this respect, this thesis aims to use the open-source Zero Overhead Topology Infrastructure (ZOTI) methodology to formulate a synthesis process from a denotational graph-based representation of an application, tailored towards heterogeneous hardware/software implementations. The case study presents the partially automated synthesis of an open-source streaming processing subsystem on a Xilinx Zynq-based system-on-chip architecture consisting of a software part and a custom hardware accelerator part, where both C software and VHDL hardware are generated from the input model. While the initial results demonstrate a promising path for systemizing the code generation process, certain aspects of the synthesis, such as generating glue code for complex data types (e.g., multi-arrays), are left out of the scope of this thesis and will be explored in future work. / Heterogena plattformar, system med både generella processorer och uppgiftsspecifik hårdvara, används till stor del inom industrin för att öka effektiviteten, men heterogeniteten ökar också svårigheten att designa och verifiera. Vi behöver ofta vänta på att alla moduler är färdiga för att veta om designens funktionalitet är korrekt eller inte, vilket kan orsaka kostsamma och tråkiga designiterationscykler. Korrekthet genom konstruktion är en metod som föreslår att man åtgärdar detta problem genom att separera specifikation och implementering och överbrygga dem genom formella metoder. Kodsyntes är en av dessa metoder som hänvisar till processen att generera lågnivåkoder som implementerar det önskade systemet från högnivåmodelleringsspråk. Att formulera en generisk syntesmetod kan i princip minska felfrekvensen och förkorta utvecklingscyklerna eftersom målspecifik användning och mekanismer systematiskt kan tas om hand på ett automatiskt sätt, medan designern bara behöver säkerställa den funktionella korrektheten hos högnivån. specifikationsmodell. I detta avseende syftar denna avhandling till att använda öppen källkod Zero Overhead Topology Infrastructure (ZOTI) metodiken för att formulera en syntesprocess från en denotationsgrafbaserad representation av en applikation, skräddarsydd för heterogena hårdvaru-/mjukvaruimplementationer. Fallstudien presenterar den delvis automatiserade syntesen av ett undersystem för bearbetning av strömning med öppen källkod på en Xilinx Zynq-baserad system-på-chip-arkitektur bestående av en mjukvarudel och en anpassad hårdvaruacceleratordel, där både C-programvara och VHDL-hårdvara genereras från ingångsmodellen. Även om de initiala resultaten visar en lovande väg för att systemisera kodgenereringsprocessen, lämnas vissa aspekter av syntesen, såsom generering av limkod för komplexa datatyper (t.ex. multi-arrayer), utanför ramen för denna avhandling och kommer att vara utforskas i framtida arbete.

Communicating Sequential Processes (CSP) is a formal language whose primary purpose is to model and verify concurrent systems. The CSP++ toolset was created to embody the concept of selective formalism by making machine-readable CSPm specifications both executable (through the automatic synthesis of C++ source) and extensible (by allowing the integration of C++ user-coded functions). However, these user-coded functions were limited by their inability to share data with each other, which meant that their application was constrained to solving simple problems in isolation. We extend CSP++ by providing user-coded functions in the same CSP process with safe access to a shared storage area, similar in concept and API to Pthreads' thread-local storage, enabling cooperation between them and granting them the ability to undertake more complex tasks without breaking the formalism of the underlying specification. This feature's utility is demonstrated in our line-following robot case study.