At safety-critical, mission-critical and business-critical systems the high cost of failure makes required the use of methods and techniques to ensure application reliability. In this context, formal languages, as Circus or specific languages versions like Safety-Critical Java, were created to facilitate the verification and validation of applications so consequently assisting to increase the overall reliability. Despite of the reliability increase, the modeled systems in formal languages can not be executed subsequently has to be implemented in a traditional programming language. It is in this process of free translation where occur most mistakes that end up not ensuring that the generated code conforms to the specification. Based on that premise, this paper propose to expound a strategy of translation from models written in Circus language to executable programs in SCJ language. Among the main objectives and contributions include the creation of EBNFs of the two languages and the detailed description of the translation of all elements between the two languages. / Em sistemas críticos de segurança, missão ou negócios o alto custo das falhas faz com que sejam necessários o uso de métodos e técnicas para garantir a confiabilidade da aplicação. É neste contexto que foram criadas linguagens formais como o Circus ou versões específicas de linguagens como o Safety-Critical Java para facilitar a verificação e validação das aplicações criadas e aumentar consequentemente a confiabilidade geral da aplicação. Apesar de aumentar a confiabilidade, os sistemas modelados em linguagens formais não podem ser executados e então precisam ser implementados em uma linguagem de programação tradicional. É nesse processo de livre tradução do sistema especificado onde ocorrem a maioria dos erros que acabam por não garantir que o código gerado esteja de acordo com a especificação. Baseando-se nessa premissa o presente trabalho propõem-se a apresentar uma estratégia de tradução de modelos escritos na linguagem Circus para programas executáveis na linguagem SCJ. Entre os principais objetivos e contribuições do trabalho estão a criação das EBNFs das duas linguagens e a descrição detalhada da tradução de todos os elementos entre as duas linguagens.

The Java platform is becoming a vital tool for developing real-time and safety-critical systems. Design patterns and the availability of Java libraries, both provide solutions to many known problems. Furthermore, the object-oriented nature of Java simplifies modular development of real-time systems. However, limitations of Java as a programming language for real-time systems are a notable obstacle to producing safe real-time systems. These limitations are found in the unpredictable execution model of the language, due to Java’s garbage collector, and the lack of support for non-functional specification and verification tools. In this dissertation I introduce SafeJML, a specification language for support of functional and non-functional specifications, based on an implementation of a safety-critical Java platform and the Java Modeling Language (JML). This dissertation concentrates on techniques that enable specification and dynamic checking of timing constraints for some important Java features, including methods and subtyping. SafeJML and these dynamic checking techniques allow modular specification and checking of safety-critical systems, including those that use object-orientation and design patterns. Such coding techniques could have maintenance benefits for real-time and safety-critical software

The ever-increasing functional and nonfunctional requirements in real-time safety-critical embedded systems call for new design flows that solve the specification, validation, and synthesis problems. Ensuring key properties, such as functional determinism and temporal predictability, has been the main objective of many embedded system design models. Dataflow models of computation (such as KPN, SDF, CSDF, etc.) are widely used to model stream-based embedded systems due to their inherent functional determinism. Since the introduction of the (C)SDF model, a considerable effort has been made to solve the static-periodic scheduling problem. Ensuring boundedness and liveness is the essence of the proposed algorithms in addition to optimizing some nonfunctional performance metrics (e.g. buffer minimization, throughput maximization, etc.). However, nowadays real-time embedded systems are so complex that real-time operating systems are used to manage hardware resources and host real-time tasks. Most of real-time operating systems rely on priority-driven scheduling algorithms (e.g. RM, EDF, etc.) instead of static schedules which are inflexible and difficult to maintain. This thesis addresses the real-time scheduling problem of dataflow graph specifications; i.e. transformation of the dataflow specification to a set of independent real-time tasks w.r.t. a given priority-driven scheduling policy such that the following properties are satisfied: (1) channels are bounded and overflow/underflow-free; (2) the task set is schedulable on a given uniprocessor (or multiprocessor) architecture. This problem requires the synthesis of scheduling parameters (e.g. periods, priorities, processor allocation, etc.) and channel capacities. Furthermore, the thesis considers two performance optimization problems: buffer minimization and throughput maximization.

Les systèmes temps-réel critiques sont de plus en plus complexes, et les exigences fonctionnelles et non-fonctionnelles ne cessent plus de croître. Le flot de conception de tels systèmes doit assurer, parmi d’autres propriétés, le déterminisme fonctionnel et la prévisibilité temporelle. Le déterminisme fonctionnel est inhérent aux modèles de calcul flot de données (ex. KPN, SDF, etc.) ; c’est pour cela qu’ils sont largement utilisés pour modéliser les systèmes embarqués de traitement de flux. Un effort considérable a été accompli pour résoudre le problème d’ordonnancement statique périodique et à mémoire de communication bornée des graphes flot de données. Cependant, les systèmes embarqués temps-réel optent de plus en plus pour l’utilisation de systèmes d’exploitation temps-réel et de stratégies d’ordonnancement dynamique pour gérer les tâches et les ressources critiques. Cette thèse aborde le problème d’ordonnancement temps-réel dynamique des graphes flot de données ; ce problème consiste à assigner chaque acteur dans un graphe à une tâche temps-réel périodique (i.e. calcul des périodes, des phases, etc.) de façon à : (1) assurer l’ordonnançabilité des tâches sur une architecture et pour une stratégie d’ordonnancement (ex. RM, EDF) données ; (2) exclure statiquement les exceptions d’overflow et d’underflow sur les buffers de communication ; et (3) optimiser les performances du système (ex. maximisation du débit, minimisation des tailles des buffers). / The ever-increasing functional and nonfunctional requirements in real-time safety-critical embedded systems call for new design flows that solve the specification, validation, and synthesis problems. Ensuring key properties, such as functional determinism and temporal predictability, has been the main objective of many embedded system design models. Dataflow models of computation (such as KPN, SDF, CSDF, etc.) are widely used to model stream-based embedded systems due to their inherent functional determinism. Since the introduction of the (C)SDF model, a considerable effort has been made to solve the static-periodic scheduling problem. Ensuring boundedness and liveness is the essence of the proposed algorithms in addition to optimizing some nonfunctional performance metrics (e.g. buffer minimization, throughput maximization, etc.). However, nowadays real-time embedded systems are so complex that real-time operating systems are used to manage hardware resources and host real-time tasks. Most of real-time operating systems rely on priority-driven scheduling algorithms (e.g. RM, EDF, etc.) instead of static schedules which are inflexible and difficult to maintain. This thesis addresses the real-time scheduling problem of dataflow graph specifications; i.e. transformation of the dataflow specification to a set of independent real-time tasks w.r.t. a given priority-driven scheduling policy such that the following properties are satisfied: (1) channels are bounded and overflow/underflow-free; (2) the task set is schedulable on a given uniprocessor (or multiprocessor) architecture. This problem requires the synthesis of scheduling parameters (e.g. periods, priorities, processor allocation, etc.) and channel capacities. Furthermore, the thesis considers two performance optimization problems: buffer minimization and throughput maximization.