Embedded systems are used in a wide spectrum of applications ranging from home appliances and mobile devices to medical equipment and vehicle controllers. They are typically characterized by their real-time behavior and many of them must fulfill strict requirements on reliability and correctness. In this thesis, we concentrate on aspects related to modeling and formal verification of realtime embedded systems. First, we define a formal model of computation for real-time embedded systems based on Petri nets. Our model can capture important features of such systems and allows their representations at different levels of granularity. Our modeling formalism has a welldefined semantics so that it supports a precise representation of the system, the use of formal methods to verify its correctness, and the automation of different tasks along the design process. Second, we propose an approach to the problem of formal verification of real-time embedded systems represented in our modeling formalism. We make use of model checking to prove whether certain properties, expressed as temporal logic formulas, hold with respect to the system model. We introduce a systematic procedure to translate our model into timed automata so that it is possible to use available model checking ools. Various examples, including a realistic industrial case, demonstrate the feasibility of our approach on practical applications.

Les algorithmes des systèmes temps réels incluent de plus en plus de nids de boucles, qui sont caractérisés par un temps d’exécution important. De ce fait, plusieurs démarches de parallélisme des boucles imbriquées ont été proposées dans l’objectif de réduire leurs temps d’exécution. Ces démarches peuvent être classifiées selon deux niveaux de granularité : le parallélisme au niveau des itérations et le parallélisme au niveau des instructions. Dans le cas du deuxième niveau de granularité, les techniques visent à atteindre un parallélisme total des instructions appartenant à une même itération. Cependant, le parallélisme est contraint par les dépendances des données inter-itérations ce qui implique le décalage des instructions à travers les boucles imbriquées, provocant ainsi une augmentation du code proportionnelle au niveau du parallélisme. Par conséquent, le parallélisme total au niveau des instructions des nids de boucles engendre des implémentations avec des temps d’exécution non-optimaux et des tailles du code importantes. Les travaux de cette thèse s’intéressent à l’amélioration des stratégies de parallélisme des nids de boucles. Une première contribution consiste à proposer une nouvelle technique de parallélisme au niveau des instructions baptisée « retiming multidimensionnel décalé ». Elle vise à ordonnancer les nids de boucles avec une période de cycle minimale, sans atteindre un parallélisme total. Une deuxième contribution consiste à mettre en pratique notre technique dans le contexte de l’implémentation temps réel embarquée des nids de boucles. L’objectif est de respecter la contrainte du temps d’exécution tout en utilisant un code de taille minimale. Dans ce contexte, nous avons proposé une première démarche d’optimisation qui consiste à utiliser notre technique pour déterminer le niveau parallélisme minimal. Par la suite, nous avons décrit une deuxième démarche permettant de combiner les parallélismes au niveau des instructions et au niveau des itérations, en utilisant notre technique et le « loop striping » / The real time implementation algorithms always include nested loops which require important execution times. Thus, several nested loop parallelism techniques have been proposed with the aim of decreasing their execution times. These techniques can be classified in terms of granularity, which are the iteration level parallelism and the instruction level parallelism. In the case of the instruction level parallelism, the techniques aim to achieve a full parallelism. However, the loop carried dependencies implies shifting instructions in both side of nested loops. Consequently, these techniques provide implementations with non-optimal execution times and important code sizes, which represent limiting factors when implemented on embedded real-time systems. In this work, we are interested on enhancing the parallelism strategies of nested loops. The first contribution consists of purposing a novel instruction level parallelism technique, called “delayed multidimensional retiming”. It aims to scheduling the nested loops with the minimal cycle period, without achieving a full parallelism. The second contribution consists of employing the “delayed multidimensional retiming” when providing nested loop implementations on real time embedded systems. The aim is to respect an execution time constraint while using minimal code size. In this context, we proposed a first approach that selects the minimal instruction parallelism level allowing the execution time constraint respect. The second approach employs both instruction level parallelism and iteration level parallelism, by using the “delayed multidimensional retiming” and the “loop striping”

Ces travaux avaient pour objectif la preuve de concept et le développement d’un dispositif embarqué sur un T-shirt visant à terme à se substituer au corset afin de pouvoir améliorer la prise en charge des patients scoliotiques. Il s’agissait d’orienter les soins de la scoliose vers un traitement permettant au patient de conserver l’ensemble de sa mobilité et de rééquilibrer l’activité des muscles de son tronc. Tout d’abord, une étude clinique comparative entre sujets sains, patients scoliotiques lombaires et patients scoliotiques thoraciques a été menée afin de mettre en évidence des différences cinématiques et posturales potentiellement corrigeables, à travers l’étude de mouvements simples standardisés. Ensuite, le dispositif baptisé « kinésithérapeute embarqué » a été développé. Son but est de détecter des anomalies cinématiques ou de mauvaises postures chez le patient afin de les lui signaler pour lui permettre une autocorrection de ses défauts. Le T-shirt permet alors une mesure précise des mouvements de l’utilisateur en temps-réel et sans dispositif externe, à l’aide de centrales inertielles. Deux feedbacks ont été conçus répondant à deux utilisations différentes, l’un vibro-tactile pour une correction posturale en ambulatoire au cours de la journée, et l’autre visuel permettant d’apprendre et d’entraîner des mouvements spécifiques lors de séances de kinésithérapie à domicile. / The purpose of this thesis was the proof of concept and the development of an embedded device on a T-shirt aiming in the future to replace the brace for improving the medical care of scoliotic patients. The aim was to orient scoliosis care toward a treatment allowing a patient to keep his/her full mobility and rebalancing his trunk muscles. First, a comparative clinical study between healthy subjects, lumbar scoliotic patients and thoracic scoliotic patients was conducted in order to highlight kinematic and postural differences potentially correctable through the study of simple and standardized movements. Then, the so-called “embedded physiotherapist” device has been developed. Its aim is to detect patient’s kinematic singularities or bad postures and to alert him/her for an auto-correction of the defect. Thus, the T-shirt is able to accurately measure user’s motion in real-time and without any external device, using inertial measurement units. Two feedback have been designed for satisfying two different purposes, first a vibro-tactile one for postural corrections during the day, and a visual one allowing the user to learn and train specific motions during physiotherapy sessions at home.

A crescente demanda da indústria exige a produção de dispositivos embarcados em menos tempo e com mais funcionalidades diferentes. Isso implica diretamente no processo de desenvolvimento destes produtos requerendo novas técnicas para absorver a complexidade crescente dos projetos e para acelerar suas etapas de desenvolvimento. A linguagem UML vem sendo utilizada para absorver a complexidade do projeto de sistemas embarcados através de sua representação gráfica que torna o processo mais simples e intuitivo. Para acelerar o desenvolvimento surgiram processos que permitem, diretamente a partir modelos UML, a geração de código para linguagens de descrição de software embarcado (C, C++, Java) e para linguagens tradicionais de descrição de hardware (VHDL, Verilog). Diversos trabalhos e ferramentas comerciais foram desenvolvidos para automatizar o processo de geração de código convencional a partir de modelos UML (software). No entanto, pela complexidade da transformação existem apenas poucos trabalhos e nenhuma ferramenta comercial direcionado à geração de HDL a partir de UML, tornando este processo ainda pouco difundido. Nossa proposta é focada na geração de descrições de hardware na linguagem VHDL a partir de modelos UML de sistemas tempo-real embarcados (STRE), surgindo como alternativa ao processo de desenvolvimento de hardware. Apresenta uma metodologia completa para geração automática de código VHDL, permitindo que o comportamento descrito para o sistema modelado seja testado e validado antes de ser desenvolvido, acelerando o processo de produção de hardware e diminuindo as chances de erros de projeto. É proposto como um processo de engenharia dirigido por modelos (MDE) que cobre desde as fases de análise de requisitos e modelagem UML, até a geração de código fonte na linguagem VHDL, onde o foco é gerar na forma de descrições de hardware, todas aquelas funções lógicas de um sistema embarcado que normalmente são desenvolvidas em software. Para atingir este objetivo, foi desenvolvido neste trabalho um conjunto de regras de mapeamento que estende a funcionalidade da ferramenta GenERTiCA, utilizada como suporte ao processo. Adicionalmente, foram pesquisados e desenvolvidos conceitos que serviram como base para o desenvolvimento de regras utilizadas pela ferramenta suporte para guiar o processo de mapeamento entre as linguagens. Os conceitos e as regras propostas foram validados por meio de um estudo de caso, cujos resultados obtidos estão demonstrados nesta dissertação. / The growing market demand requires the production of embedded devices in less time and with more different features. This directly implies on the development process of these products requiring new techniques to absorb the growing complexity of projects and to accelerate their development stages. UML has been used to handle the embedded systems design complexity through its graphical representation that makes the process simpler and more intuitive. To speed up the development cycle, it has emerged some processes that permit code generating directly from UML models to embedded software description languages (C, C++, Java), and traditional hardware description languages (VHDL, Verilog). Several researches and commercial tools have been developed to automate the code generation process from UML models to conventional languages (software). However, due to the transformation complexity there are only few studies and no commercial tool addressed to HDL generation from UML models, making this process almost unknown. Our proposal is focused on generating hardware descriptions as VHDL code from UML models of real-time embedded systems (RTES), emerging as an alternative to the hardware development. It presents a complete methodology to the VHDL code generation, allowing the behavior described to the modeled system to be tested and validated before being implemented, accelerating the hardware production and decreasing the chances of design errors. It is proposed as a model-driven engineering (MDE) process that covers the phases of requirements analysis, UML modeling, models transformations, and the source code generating process to the VHDL language, where the focus is to generate as hardware descriptions all the logic functions of an embedded system which are usually developed as software. To achieve this goal, this work was developed a set of mapping rules which extends the functionality of the tool GenERTiCA, used to support the process. Additionally, it was researched and developed concepts that were the basis for the development of rules used by the tool support to guide the mapping process between languages. The concepts and proposed rules have been validated through a case study, whose results are shown in this dissertation.

A crescente demanda da indústria exige a produção de dispositivos embarcados em menos tempo e com mais funcionalidades diferentes. Isso implica diretamente no processo de desenvolvimento destes produtos requerendo novas técnicas para absorver a complexidade crescente dos projetos e para acelerar suas etapas de desenvolvimento. A linguagem UML vem sendo utilizada para absorver a complexidade do projeto de sistemas embarcados através de sua representação gráfica que torna o processo mais simples e intuitivo. Para acelerar o desenvolvimento surgiram processos que permitem, diretamente a partir modelos UML, a geração de código para linguagens de descrição de software embarcado (C, C++, Java) e para linguagens tradicionais de descrição de hardware (VHDL, Verilog). Diversos trabalhos e ferramentas comerciais foram desenvolvidos para automatizar o processo de geração de código convencional a partir de modelos UML (software). No entanto, pela complexidade da transformação existem apenas poucos trabalhos e nenhuma ferramenta comercial direcionado à geração de HDL a partir de UML, tornando este processo ainda pouco difundido. Nossa proposta é focada na geração de descrições de hardware na linguagem VHDL a partir de modelos UML de sistemas tempo-real embarcados (STRE), surgindo como alternativa ao processo de desenvolvimento de hardware. Apresenta uma metodologia completa para geração automática de código VHDL, permitindo que o comportamento descrito para o sistema modelado seja testado e validado antes de ser desenvolvido, acelerando o processo de produção de hardware e diminuindo as chances de erros de projeto. É proposto como um processo de engenharia dirigido por modelos (MDE) que cobre desde as fases de análise de requisitos e modelagem UML, até a geração de código fonte na linguagem VHDL, onde o foco é gerar na forma de descrições de hardware, todas aquelas funções lógicas de um sistema embarcado que normalmente são desenvolvidas em software. Para atingir este objetivo, foi desenvolvido neste trabalho um conjunto de regras de mapeamento que estende a funcionalidade da ferramenta GenERTiCA, utilizada como suporte ao processo. Adicionalmente, foram pesquisados e desenvolvidos conceitos que serviram como base para o desenvolvimento de regras utilizadas pela ferramenta suporte para guiar o processo de mapeamento entre as linguagens. Os conceitos e as regras propostas foram validados por meio de um estudo de caso, cujos resultados obtidos estão demonstrados nesta dissertação. / The growing market demand requires the production of embedded devices in less time and with more different features. This directly implies on the development process of these products requiring new techniques to absorb the growing complexity of projects and to accelerate their development stages. UML has been used to handle the embedded systems design complexity through its graphical representation that makes the process simpler and more intuitive. To speed up the development cycle, it has emerged some processes that permit code generating directly from UML models to embedded software description languages (C, C++, Java), and traditional hardware description languages (VHDL, Verilog). Several researches and commercial tools have been developed to automate the code generation process from UML models to conventional languages (software). However, due to the transformation complexity there are only few studies and no commercial tool addressed to HDL generation from UML models, making this process almost unknown. Our proposal is focused on generating hardware descriptions as VHDL code from UML models of real-time embedded systems (RTES), emerging as an alternative to the hardware development. It presents a complete methodology to the VHDL code generation, allowing the behavior described to the modeled system to be tested and validated before being implemented, accelerating the hardware production and decreasing the chances of design errors. It is proposed as a model-driven engineering (MDE) process that covers the phases of requirements analysis, UML modeling, models transformations, and the source code generating process to the VHDL language, where the focus is to generate as hardware descriptions all the logic functions of an embedded system which are usually developed as software. To achieve this goal, this work was developed a set of mapping rules which extends the functionality of the tool GenERTiCA, used to support the process. Additionally, it was researched and developed concepts that were the basis for the development of rules used by the tool support to guide the mapping process between languages. The concepts and proposed rules have been validated through a case study, whose results are shown in this dissertation.

A crescente demanda da indústria exige a produção de dispositivos embarcados em menos tempo e com mais funcionalidades diferentes. Isso implica diretamente no processo de desenvolvimento destes produtos requerendo novas técnicas para absorver a complexidade crescente dos projetos e para acelerar suas etapas de desenvolvimento. A linguagem UML vem sendo utilizada para absorver a complexidade do projeto de sistemas embarcados através de sua representação gráfica que torna o processo mais simples e intuitivo. Para acelerar o desenvolvimento surgiram processos que permitem, diretamente a partir modelos UML, a geração de código para linguagens de descrição de software embarcado (C, C++, Java) e para linguagens tradicionais de descrição de hardware (VHDL, Verilog). Diversos trabalhos e ferramentas comerciais foram desenvolvidos para automatizar o processo de geração de código convencional a partir de modelos UML (software). No entanto, pela complexidade da transformação existem apenas poucos trabalhos e nenhuma ferramenta comercial direcionado à geração de HDL a partir de UML, tornando este processo ainda pouco difundido. Nossa proposta é focada na geração de descrições de hardware na linguagem VHDL a partir de modelos UML de sistemas tempo-real embarcados (STRE), surgindo como alternativa ao processo de desenvolvimento de hardware. Apresenta uma metodologia completa para geração automática de código VHDL, permitindo que o comportamento descrito para o sistema modelado seja testado e validado antes de ser desenvolvido, acelerando o processo de produção de hardware e diminuindo as chances de erros de projeto. É proposto como um processo de engenharia dirigido por modelos (MDE) que cobre desde as fases de análise de requisitos e modelagem UML, até a geração de código fonte na linguagem VHDL, onde o foco é gerar na forma de descrições de hardware, todas aquelas funções lógicas de um sistema embarcado que normalmente são desenvolvidas em software. Para atingir este objetivo, foi desenvolvido neste trabalho um conjunto de regras de mapeamento que estende a funcionalidade da ferramenta GenERTiCA, utilizada como suporte ao processo. Adicionalmente, foram pesquisados e desenvolvidos conceitos que serviram como base para o desenvolvimento de regras utilizadas pela ferramenta suporte para guiar o processo de mapeamento entre as linguagens. Os conceitos e as regras propostas foram validados por meio de um estudo de caso, cujos resultados obtidos estão demonstrados nesta dissertação. / The growing market demand requires the production of embedded devices in less time and with more different features. This directly implies on the development process of these products requiring new techniques to absorb the growing complexity of projects and to accelerate their development stages. UML has been used to handle the embedded systems design complexity through its graphical representation that makes the process simpler and more intuitive. To speed up the development cycle, it has emerged some processes that permit code generating directly from UML models to embedded software description languages (C, C++, Java), and traditional hardware description languages (VHDL, Verilog). Several researches and commercial tools have been developed to automate the code generation process from UML models to conventional languages (software). However, due to the transformation complexity there are only few studies and no commercial tool addressed to HDL generation from UML models, making this process almost unknown. Our proposal is focused on generating hardware descriptions as VHDL code from UML models of real-time embedded systems (RTES), emerging as an alternative to the hardware development. It presents a complete methodology to the VHDL code generation, allowing the behavior described to the modeled system to be tested and validated before being implemented, accelerating the hardware production and decreasing the chances of design errors. It is proposed as a model-driven engineering (MDE) process that covers the phases of requirements analysis, UML modeling, models transformations, and the source code generating process to the VHDL language, where the focus is to generate as hardware descriptions all the logic functions of an embedded system which are usually developed as software. To achieve this goal, this work was developed a set of mapping rules which extends the functionality of the tool GenERTiCA, used to support the process. Additionally, it was researched and developed concepts that were the basis for the development of rules used by the tool support to guide the mapping process between languages. The concepts and proposed rules have been validated through a case study, whose results are shown in this dissertation.

This research work develops real-time incremental learning decision tree solutions suitable for real-time embedded systems by virtue of having both a defined memory requirement and an upper bound on the computation time per training vector. In addition, the work provides embedded systems with the capabilities of rapid processing and training of streamed data problems, and adopts electronic hardware solutions to improve the performance of the developed algorithm. Two novel decision tree approaches, namely the Multi-Dimensional Frequency Table (MDFT) and the Hashed Frequency Table Decision Tree (HFTDT) represent the core of this research work. Both methods successfully incorporate a frequency table technique to produce a complete decision tree. The MDFT and HFTDT learning methods were designed with the ability to generate application specific code for both training and classification purposes according to the requirements of the targeted application. The MDFT allows the memory architecture to be specified statically before learning takes place within a deterministic execution time. The HFTDT method is a development of the MDFT where a reduction in the memory requirements is achieved within a deterministic execution time. The HFTDT achieved low memory usage when compared to existing decision tree methods and hardware acceleration improved the performance by up to 10 times in terms of the execution time.

<p>Ova disertacija se bavi istraživanjem u oblasti integracije servisa digitalne televizije u moderne uređaje potrošačke elektronike. Cilj teze je da razvije pristup za sistemsko proširenje Android operativnog sistema servisima digitalne televizije, i da predloži rešenje koje omogućuje rad u realnom vremenu. Kvalitet rešenja se ocenjuje odgovarajućim metrikama preko ocene kvaliteta implementirane Java objektno orijentisane sprege za TV servise. Osnovni doprinos teze se ogleda u definisanju jedinstvene programske sprege servisa digitalne televizije na platformama koje prate paradigmu virtuelne mašine. Predloženo rešenje omogućuje razvoj aplikacija optimizovanih za izvršavanje na TV uređajima i dalje sprezanje podataka TV servisa sa ostatkom Android ekosistema.</p> / <p>This PhD dissertation addresses the problem of integration of the digital TV services inside modern consumer electronic devices. The main focus of the dissertation is a development of systematic approach for extension of Android operating system with support for digital television. Combined with this, the dissertation describes solution in form of hardware platform with accompanying software that closely follows this approach and achieves real-time performance. Quality of proposed solution is benchmarked using metrics for measuring quality of object-oriented program code. The main contribution of the dissertation is unification of system software API for digital television on Android-based platforms. Proposed solution allows development of TV-centric software capable of real-time performance, and further native integration of data coming from DVB broadcast into Android ecosystem.</p>

Cache memory is used, in most single-core and multi-core processors, to improve performance by bridging the speed gap between the main memory and CPU. Even though cache increases performance, it poses some serious challenges for embedded systems running real-time applications. Cache introduces execution time unpredictability due to its adaptive and dynamic nature and cache consumes vast amount of power to be operated. Energy requirement and execution time predictability are crucial for the success of real-time embedded systems. Various cache optimization schemes have been proposed to address the performance, power consumption, and predictability issues. However, currently available solutions are not adequate for real-time embedded systems as they do not address the performance, power consumption, and execution time predictability issues at the same time. Moreover, existing solutions are not suitable for dealing with multi-core architecture issues. In this dissertation, we develop a methodology through cache optimization for real-time embedded systems that can be used to analyze and improve execution time predictability and performance/power ratio at the same time. This methodology is effective for both single-core and multi-core systems. First, we develop a cache modeling and optimization technique for single-core systems to improve performance. Then, we develop a cache modeling and optimization technique for multi-core systems to improve performance/power ratio. We develop a cache locking scheme to improve execution time predictability for real-time systems. We introduce Miss Table (MT) based cache locking scheme with victim cache (VC) to improve predictability and performance/power ratio. MT holds information about memory blocks, which may cause more misses if not locked, to improve cache locking performance. / VC temporarily stores the victim blocks from level-1 cache to improve cache hits. In addition, MT is used to improve cache replacement performance and VC is used to improve cache hits by supporting stream buffering. We also develop strategies to generate realistic workload by characterizing applications to simulate cache optimization and cache locking schemes. Popular MPEG4, H.264/AVC, FFT, MI, and DFT applications are used to run the simulation programs. Simulation results show that newly introduced Miss Table based cache locking scheme with victim cache significantly improves the predictability and performance/power ratio. In this work, a reduction of 33% in mean delay per task and a reduction of 41% in total power consumption are achieved by using MT and VCs while locking 25% of level-2 cache size in an 4-core system. It is also observed that execution time predictability can be improved by avoiding more than 50% cache misses while locking one-fourth of the cache size. / by Abu Asaduzzaman. / Vita. / Thesis (Ph.D.)--Florida Atlantic University, 2009. / Includes bibliography. / Electronic reproduction. Boca Raton, Fla., 2009. Mode of access: World Wide Web.

Future space missions, such as Mars Science Laboratory, suggest the engineering of some of the most complex man-rated autonomous software systems. The present process-oriented certification methodologies are becoming prohibitively expensive and do not reach the level of detail of providing guidelines for the development and validation of concurrent software. Time and concurrency are the most critical notions in an autonomous space system. In this work we present the design and implementation of the first concurrency and time centered framework for product-oriented software certification of autonomous space systems. To achieve fast and reliable concurrent interactions, we define and apply the notion of Semantically Enhanced Containers (SEC). SECs are data structures that are designed to provide the flexibility and usability of the popular ISO C++ STL containers, while at the same time they are hand-crafted to guarantee domain-specific policies, such as conformance to a given concurrency model. The application of nonblocking programming techniques is critical to the implementation of our SEC containers. Lock-free algorithms help avoid the hazards of deadlock, livelock, and priority inversion, and at the same time deliver fast and scalable performance. Practical lock-free algorithms are notoriously difficult to design and implement and pose a number of hard problems such as ABA avoidance, high complexity, portability, and meeting the linearizability correctness requirements. This dissertation presents the design of the first lock-free dynamically resizable array. Our approach o ers a set of practical, portable, lock-free, and linearizable STL vector operations and a fast and space effcient implementation when compared to the alternative lock- and STM-based techniques. Currently, the literature does not offer an explicit analysis of the ABA problem, its relation to the most commonly applied nonblocking programming techniques, and the possibilities for its detection and avoidance. Eliminating the hazards of ABA is left to the ingenuity of the software designer. We present a generic and practical solution to the fundamental ABA problem for lock-free descriptor-based designs. To enable our SEC container with the property of validating domain-specific invariants, we present Basic Query, our expression template-based library for statically extracting semantic information from C++ source code. The use of static analysis allows for a far more efficient implementation of our nonblocking containers than would have been otherwise possible when relying on the traditional run-time based techniques. Shared data in a real-time cyber-physical system can often be polymorphic (as is the case with a number of components part of the Mission Data System's Data Management Services). The use of dynamic cast is important in the design of autonomous real-time systems since the operation allows for a direct representation of the management and behavior of polymorphic data. To allow for the application of dynamic cast in mission critical code, we validate and improve a methodology for constant-time dynamic cast that shifts the complexity of the operation to the compiler's static checker. In a case study that demonstrates the applicability of the programming and validation techniques of our certification framework, we show the process of verification and semantic parallelization of the Mission Data System's (MDS) Goal Networks. MDS provides an experimental platform for testing and development of autonomous real-time flight applications.