Neste trabalho é apresentado um método de refinamento para especificações de sistemas embarcados, baseado na linguagem de especificação gráfica UML-RT e na linguagem de especificação formal CSP-OZ. A linguagem UML-RT é utilizada para descrever a arquitetura de sistemas de tempo real distribuídos e esses mapeados para uma especificação formal através de CSP-OZ. A linguagem de especificação formal CSP-OZ é a combinação da linguagem orientada a objetos Object-Z e a algebra de processos CSP, que descreve o comportamento de processos concorrentes. O método de refinamento proposto é baseado na integração de dois métodos: o de bi-simulação, para refinar a parte comportamental da especificação descrita por CSP; e o de equivalência de especificações, para refinar as estruturas de dados descritas por Object-Z, permitindo assim que características de orientação a objetos possam ser utilizadas. Com o método proposto é possível refinar especificações e, conseqüentemente, verificá-las com sua implementação. O desenvolvimento desse método é rigoroso, incluindo a definição formal para um metamodelo da UML-RT. Um exemplo detalhado é apresentado no final deste trabalho. / In this work, a method of refinement of embedded systems specifications based on the graphical specification language UML-RT and the formal specification CSP-OZ is introduced. The UML-RT is used to model real time distributed architecture systems and these are mapped onto formal specifications using CSP-OZ. The CSP-OZ formal specification language is a combination of the state-based object oriented language Object-Z and the CSP process algebra that describes behavioral models of concurrent processes. The rationale of the proposed refinement method is twofold, the use of bisimulation to refine the behavioral part and the specification matching algorithm to refine the state-based part, supporting object-oriented characteristics. Using this result, an equivalence between the specification-matching algorithm and simulation rules is showed. Using the proposed method it is possible to refine CSP-OZ specifications and verify them against their implementations. The development of the proposed refinement method is rigorous, including a formal definition for a UML-RT metamodel. A detailed study case is given at the end of this work.

Dans cette thèse nous proposons un modèle temporel dans le cadre des machines à états abstraits (ASM). Une extension du langage de spécification ASM est développé qui correspond à ce modéle temporel pour le temps continu. L'extension du langage avec des constructions de temps permet de diminuer la taille de la spécification et donc de réduire la probabilité d'erreurs. La sémantique de l'extension du langage ASM est fournie et prend en compte les définitions des fonctions externes, les valeurs des délais et les choix de résolution des non-déterminismes. Un sous-système de vérification des propriétés exprimées en logique FOTL (FirstOrder Timed Logic) est développé. Un simulateur d'ASMs temporisées est développé et implémenté, il comprend un analyseur syntaxique, un interprète du langage, un sous-système de vérification des propriétés ainsi qu'une interface graphique / In this thesis a temporal model for abstract state machines (ASM) method is pro- posed. An extension of ASM specification language on the base of the proposed temporal model with continuous time is developed. The language extension helps to reduce the size of the specification hence to diminish the probability of an error. The semantics of the extended ASM language is developed which takes into account the definitions of external functions, the values of time delays and the method of non-determinism resolving. A subsystem for verification of user properties in the FOTL language is developed. A simulator prototype for ASMs with time is developed and implemented. It includes the parser of the timed ASM language, the interpreter, the verification subsystem and the graphical user interface

Les tâches critiques en systèmes temps-réel sont soumises à des contraintes temporelles et de correction. La validation d'un tel système repose sur l'estimation du comportement temporel au pire cas de ses tâches. Le partage de ressources, inhérent aux architectures multi-cœurs, entrave le calcul de ces estimations. Le comportement temporel d'une tâche dépend de ses rivales du fait de l'arbitrage de l'accès aux ressources ou de modifications concurrentes de leur état. Cette étude vise à l'estimation de la contribution temporelle de la hiérarchie mémoire au pire temps d'exécution de tâches critiques. Les méthodes existantes, pour caches d'instructions, sont étendues afin de supporter caches de données privés et partagés, et permettre l'analyse de hiérarchies mémoires riches. Le court-circuitage de cache est ensuite utilisé pour réduire la pression sur les caches partagés. Nous proposons à cette fin différentes heuristiques basées sur la capture de la réutilisation de blocs de cache entre différents accès mémoire. Notre seconde proposition est la politique de partitionnement Preti qui permet l'allocation d'un espace sans conflits à une tâche. Preti favorise aussi les performances de tâches non critiques concurrentes aux temps-réel dans les systèmes de criticité hybride. / Critical tasks in the context of real-time systems submit to both timing and correctness constraints. Whence, the validation of a real-time system rely on the estimation of its tasks’ Worst case execution times. Resource sharing, as it occurs on multicore architectures, hinders the computation of such estimates. The timing behaviour of a task is impacted by its concurrents, whether because of resource access arbitration or concurrent modifications of a resource state. This study focuses on estimating the contribution of the memory hierarchy to tasks’ worst case execution time. Existing analysis methods, defined for instruction caches, are extended to support private and shared data caches, hence allowing for the analysis of rich memory hierarchies. Cache bypass is then used to reduce the pressure laid by concurrent tasks on shared caches levels. We propose different bypass heuristics, based on the capture of cache blocks’ reuse between memory accesses. Our second proposal is the Preti partitioning scheme which allows for the allocation to tasks of a cache space, free from inter-task conflicts. Preti offers the added benefit of providing for average-case performance to non-critical tasks concurrent to real-time ones on hybrid criticality systems.

Neste trabalho é apresentado um método de refinamento para especificações de sistemas embarcados, baseado na linguagem de especificação gráfica UML-RT e na linguagem de especificação formal CSP-OZ. A linguagem UML-RT é utilizada para descrever a arquitetura de sistemas de tempo real distribuídos e esses mapeados para uma especificação formal através de CSP-OZ. A linguagem de especificação formal CSP-OZ é a combinação da linguagem orientada a objetos Object-Z e a algebra de processos CSP, que descreve o comportamento de processos concorrentes. O método de refinamento proposto é baseado na integração de dois métodos: o de bi-simulação, para refinar a parte comportamental da especificação descrita por CSP; e o de equivalência de especificações, para refinar as estruturas de dados descritas por Object-Z, permitindo assim que características de orientação a objetos possam ser utilizadas. Com o método proposto é possível refinar especificações e, conseqüentemente, verificá-las com sua implementação. O desenvolvimento desse método é rigoroso, incluindo a definição formal para um metamodelo da UML-RT. Um exemplo detalhado é apresentado no final deste trabalho. / In this work, a method of refinement of embedded systems specifications based on the graphical specification language UML-RT and the formal specification CSP-OZ is introduced. The UML-RT is used to model real time distributed architecture systems and these are mapped onto formal specifications using CSP-OZ. The CSP-OZ formal specification language is a combination of the state-based object oriented language Object-Z and the CSP process algebra that describes behavioral models of concurrent processes. The rationale of the proposed refinement method is twofold, the use of bisimulation to refine the behavioral part and the specification matching algorithm to refine the state-based part, supporting object-oriented characteristics. Using this result, an equivalence between the specification-matching algorithm and simulation rules is showed. Using the proposed method it is possible to refine CSP-OZ specifications and verify them against their implementations. The development of the proposed refinement method is rigorous, including a formal definition for a UML-RT metamodel. A detailed study case is given at the end of this work.

Cette thèse présente une méthodologie de conception et d’évaluation de lois de commande pour projectiles guidés, au moyen d’un prototype placé dans une soufflerie via un support autorisant plusieurs degrés de liberté en rotation. Ce dispositif procure un environnement permettant à la fois de caractériser expérimentalement le comportement de la munition et d’évaluer les performances des lois de commande dans des conditions réalistes, et est mis en œuvre pour l’étude d’autopilotes de tangage et de lacet, à vitesse fixe et à vitesse variable, pour un prototype de projectile empenné piloté par canards. La modélisation d’un tel système aboutit à un modèle non-linéaire dépendant de nombreuses conditions de vol telles que la vitesse et des angles d’incidence. Les méthodes de séquencement de gain basées sur des linéarisations d’un modèle non-linéaire sont couramment employées dans l’industrie pour la commande de ce type de systèmes. A cette fin, le système est représenté au moyen d’une famille de modèles linéaires dont les paramètres sont directement estimés à partir de données recueillies sur le dispositif expérimental. L’observation du comportement à différents points de vol permet de considérer la vitesse de l’air comme unique variable de séquencement. La synthèse des différents contrôleurs est réalisée au moyen d’une méthode H∞ multi-objectifs à ordre et structure fixes, afin de garantir la stabilité et la robustesse du système vis-à-vis d’incertitudes liées à la variation du point de fonctionnement. Ces lois de commande sont alors validées au moyen d’analyses de robustesse, puis par leur implémentation sur le dispositif expérimental. Les résultats obtenus lors d’essais en soufflerie correspondent aux simulations numériques et sont conformes aux spécifications attendues. / This work presents a novel methodology for flight control law design and evaluation, using a functional prototype installed in a wind tunnel by the means of a support structure allowing multiple rotational degrees of freedom. This setup provides an environment allowing experimental characterization of the munition’s behavior, as well as for flight control law evaluation in realistic conditions. The design and validation of pitch and yaw autopilots for a fin-stabilized, canard-guided projectile is investigated, at fixed and variable airspeeds. Modeling such a system leads to a nonlinear model depending on numerous flight conditions such as the airspeed and incidence angles. Linearization-based gain scheduling techniques are widely employed in the industry for controlling this class of systems. To this end, the system is represented with a family of linear models whose parameters are directly estimated from experimentally collected data. Observation of the projectile’s behavior for different operating points indicates the airspeed can be considered as the only scheduling variable. Controller synthesis is performed using a multi-objective, fixed-order, fixed-structure H∞ technique in order to guarantee the stability and robustness of the closed-loop against operating point uncertainty. The obtained control laws are validated with robustness analysis techniques and are then implemented on the experimental setup, where wind-tunnel tests results correlate with numerical simulations and conform to the design specifications.

Dans cette thèse, nous abordons le problème de la modélisation et de la vérification de systèmes complexes présentant des comportements à la fois probabilistes et temporisés. La conception de tels systèmes est devenue de plus en plus complexe en raison de l’hétérogénéité des composants impliqués, l’incertitude découlant d’un environnement ouvert et les contraintes temps réelinhérentes à leurs domaines d’application. La gestion à la fois du logiciel et du matériel dans une vue unifiée tout en incluant des informations sur les performances (par exemple, temps de calcul et de communication, consommation d’énergie, etc.) devient indispensable. Construire et analyser des modèles de performance est d’une importance primordiale pour donner des garanties sur les exigences fonctionnelles et extra-fonctionnelles des systèmes, et permettre uneprise de décision fondée sur des mesures quantitatives dès les premières étapes de la conception.Cette thèse apporte plusieurs nouvelles contributions. Tout d’abord, nous introduisons un nouveau formalisme de modélisation appelé BIP stochastique et temps réel (SRT-BIP) pour la modélisation, la simulation et la génération de code de systèmes à base de composants. Ce formalisme hérite du framework BIP ses capacités de modélisation basées sur les composants et le temps réel et, en outre, il fournit des primitives pour exprimer des comportements stochastiquescomplexes.Deuxièmement, nous étudions des techniques d’apprentissage automatique pour faciliter la construction de modèles de performance. Nous proposons d’améliorer et d’adapter une procédure d’apprentissage présentée dans la littérature pour déduire des modèles stochastiques et temporisés à partir d’exécutions concrètes du système, et de les exprimer dans le formalisme SRT-BIP.Troisièmement, étant donné les modèles de performance dans SRT-BIP, nous explorons l’utilisation du model checking statistique (SMC) pour l’analyse d’exigences concernant la fonctionnalité et les performances du système. Pour ce faire, nous fournissons un framework complet, appelé SBIP, en tant qu’outil de support pour la modélisation, la simulation et l’analyse des systèmes SRT-BIP. SBIP est un environnement de développement intégré (IDE) qui implémente des algorithmes SMC pour des analyses quantitatives, qualitatives et d’événementsrares, en plus d’une procédure d’automatisation pour l’exploration des paramètres d’une propriété. Nous validons nos propositions sur des études de cas réels touchant à des domaines variés tels que les protocoles de communication, les systèmes concurrents et les systèmesembarqués.Enfin, nous étudions plus en détail l’intérêt du SMC lorsqu’il est inclus dans des méthodes d’analyse de système élaborées. Nous illustrons cela en proposant deux approches d’évaluation des risques. Dans la première approche, nous introduisons une méthodologie en spirale pour modéliser des systèmes résilients avec des composants FDIR que nous validons à travers l’évaluation de la sécurité du système de locomotion d’un rover d’exploration planétaire. La deuxième approche concerne l’évaluation des politiques de sécurité des organisations selon une approche de sécurité offensive. L’objectif est de synthétiser des configurations de défense efficaces contre des stratégies d’attaque optimisées (qui minimisent le coût d’attaque et maximisent la probabilité de succès). Ces stratégies d’attaque sont obtenues en combinant l’apprentissage de modèles et les méthodes méta-heuristiques, dans lesquels le SMC a le rôle principal d’évaluer et de prioriser les potentielles stratégies candidates. / In this thesis, we address the problem of modeling and verification of complex systems exhibiting both probabilistic and timed behaviors. Designing such systems has become increasingly complex due to the heterogeneity of the involved components, the uncertainty resulting from open environment and the real-time constraints inherent to their application domains. Handling both software and (abstraction of) hardware in a unified view while also including performanceinformation (e.g. computation and communication times, energy consumption, etc.) becomes a must. Building and analyzing performance models is of paramount importance in order to give guarantees on the functional and extra-functional system requirements and to make well-founded design decisions based on quantitative measures at early design stages.This thesis brings several new contributions. First, we introduce a new modeling formalism called Stochastic Real-Time BIP (SRT-BIP) for the modeling, the simulation and the code generation of component-based systems. This formalism inherits from the BIP framework its component-based and real-time modeling capabilities and, extends it by providing comprehensive primitives to express complex stochastic behaviors.Second, we investigate machine learning techniques to ease the construction of performance models. We propose to enhance and adapt a state-of-the-art learning procedure to infer stochastic real-time models from concrete system execution and to represent them in the SRT-BIP formalism.Third, given performance models in SRT-BIP, we explore the use of statistical Model Checking (SMC) for the anaysis of system’s functional and performance requirements. To do so, we provide a full framework, called SBIP, as a support tool for the modeling, simulation and analysis of SRT-BIP systems. SBIP is an Integrated Development Environment (IDE) that implements SMC algorithms for quantitative, qualitative and rare events analyses together with an automated exploring procedure for parameterized requirements. We validate our proposalson real-life case studies ranging from communication protocols and concurrent systems to embedded systems.Finally, we further investigate the interest of SMC when included in elaborated system analysis workflows. We illustrate this by proposing two risk assessment approaches. In the first approach, we introduce a spiral methodology to build resilient systems with FDIR components that we validate on the safety assessment of a planetary rover locomotion system. The second approach is concerned with the security assessment of organization’s defenses following an offensive security approach. The goal is to synthesize impactful defense configurations against optimized attack strategies (that minimize attack cost and maximize success probability). These attack strategies are obtained by combining model learning with meta heuristics, and where SMC is used to score and prioritize potential candidate strategies.

La Tesis presenta el desarrollo de una metodología de análisis y diseño de sistemas distribuidos de tiempo real estricto, y su aplicación a una implementación práctica en lenguaje Ada.Se han optimizado los métodos existentes para la planificación y análisis de sistemas distribuidos de tiempo real mediante un algoritmo heurístico para la asignación de prioridades, y la aplicación del algoritmo de servidor esporádico a la planificación de redes de comunicación de tiempo real. También se ha ampliado el campo de aplicación del análisis a sistemas más complejos en los que existe sincronización por intercambio de eventos o paso de mensajes.Se ha demostrado que la metodología propuesta se puede implementar en sistemas de tiempo real prácticos, a través de su aplicación a sistemas distribuidos programados en lenguaje Ada. / The Thesis presents a methodology to analyze and design distributed real-time systems, and its application to a practical implementation.Existing methods for scheduling and analyzing distributed real-time systems have been optimized through a new heuristic algorithm for assigning priorities, and with the application of the sporadic server algorithm for scheduling real-time communication networks. The area of application of the analysis has been extended to more complex systems, like those with synchronization through event exchange or message passing.It has been demonstrated that the proposed methodology can be implemented in practical real-time systems, through the application to a distributed system programmed in the Ada language.

Se propone una metodología de desarrollo de aplicaciones de tiempo real estricto que van a ser ejecutadas en plataformas distribuidas abiertas. En esta metodología, el diseñador de la aplicación no conoce la carga de trabajo de la plataforma que será ejecutada concurrentemente junto con la aplicación que diseña. La metodología se basa en el paradigma de reserva de recursos, y utiliza como base el concepto de plataforma virtual, tanto para describir el uso de los recursos que una aplicación requiere, como para ejecutar la aplicación satisfaciendo sus requisitos temporales. La plataforma virtual es utilizada en el proceso de negociación con el servicio de reserva de recursos de la plataforma física, con objeto de obtener una configuración de la aplicación que haga compatible su ejecución con la carga de trabajo que ya se está ejecutando en dicha plataforma. La metodología aborda todas las fases del desarrollo de una aplicación: describe la información que debe asociarse al código de la aplicación para poder ser configurado, así como el proceso que permite analizar independientemente su planificabilidad en base a la plataforma virtual; especifica el proceso de despliegue de la aplicación y define la información que se utiliza para negociar su ejecución con el servicio de reserva de recursos de la plataforma física y para generar los datos de configuración que deben ser asignados al código cuando se ejecute. Todos estos procesos son dirigidos por modelos, por lo que la tesis aborda la definición de las transformaciones de modelos requeridas, así como la formulación de los metamodelos formales utilizados en ellas. Por otro lado, aunque la tecnología es independiente de la plataforma de ejecución, se especifica la funcionalidad que debe ofrecer el servicio de reserva de recursos presente en la misma para dar soporte a la metodología propuesta, y se analiza su compatibilidad con algunas implementaciones actualmente disponibles / This thesis proposes a methodology for the development of hard real-time applications that will be executed in open distributed platforms. When this methodology is applied, the application designer does not know the workload of the platform that will execute concurrently with the designed application. The methodology is based on the resource reservation paradigm, and relies on the concept of virtual platform, both to describe the resources usage required by an application to execute, and to run the application guaranteeing the fulfillment of the specified timing requirements. The virtual platform is also used on the negotiation process with the resource reservation service of the physical platform in order to obtain a configuration of the application that supports its execution together with the current workload running on that platform. The methodology deals with all the phases of the application design: it describes the information that must be associated to the application code in order to obtain a proper configuration, as well as the process that allows an independent schedulability analysis of the application based on its virtual platform; it specifies the application deployment process and defines the information that is used to negotiate the execution of the application with the resource reservation service of the physical platform, and to generate the configuration data that must be assigned to the code when it is executed. The methodology follows a model-driven perspective, so the thesis addresses the required models transformations, as well as the formulation of the metamodels used in them. Moreover, although the technology is independent from the execution platform, the functionality that must be provided by the resource reservation service to support the proposed technology is specified and its compatibility with other implementations is analyzed.

The Dynamic Distributed Dependable Real-Time Industrial communication Protocol (D3RIP) provides service guarantees for Real-Time traffic and integrates the dynamically changing requirements of automation applications in their operation to efficiently utilize the resources. The protocol dynamically allocates the network resources according to the respective system state. To this end, the protocol architecture consists of an Interface Layer that provides time-slotted operation and a Coordination Layer that assigns each time slot to a unique transmitter device based on a distributed computation. In this thesis, a software simulator for D3RIP is developed. Using the D3RIP Simulator, modifications in D3RIP can be easily examined without facing complexities in real implementations and extensive effort in terms of time and cost. The simulator simulates the Interface Layer, the Coordination Layer and additionally, the Shared Medium. Hence, using the simulator, the system-protocol couple can be easily analyzed, tested and further improvements on D3RIP can be achieved with the least amount of effort. The simulator implements the Timed Input Output Automata (TIOA) models of the D3RIP stack components using C++. The resulting code is compiled on GCC (Gnu Compiler Collection). The logs of the simulation runs and the real system with 2 devices connected via cross 100MbE cables are compared. In a 3ms time slot, the simulator and the system incidents differ about 135&micro / s on the average, causing no asynchronousity in their instantaneous operational states. The D3RIP Simulator is useful in keeping track of any variable in the D3RIP system automaton at any instant up to 1&micro / s resolution.

<p>Real-time systems do not only require that the logical operations are correct. Equally important is that the specified time constraints always are complied. This has successfully been studied before for mono-processor systems. However, as the hardware in the systems gets more complex, the previous approaches become invalidated. For example, multi-processor systems-on-chip (MPSoC) get more and more common every day, and together with a shared memory, the bus access time is unpredictable in nature. This has recently been resolved, but a safe and not too pessimistic cache analysis approach for MPSoC has not been investigated before. This thesis has resulted in designed and implemented algorithms for cache analysis on real-time MPSoC with a shared communication infrastructure. An additional advantage is that the algorithms include improvements compared to previous approaches for mono-processor systems. The verification of these algorithms has been performed with the help of data flow analysis theory. Furthermore, it is not known how different types of cache miss characteristic of a task influence the worst case execution time on MPSoC. Therefore, a program that generates randomized tasks, according to different parameters, has been constructed. The parameters can, for example, influence the complexity of the control flow graph and average distance between the cache misses.</p>