Foi definido que elementos regulatórios da expressão atrial-específica do promotor da SMyHC3 estão contidos em um elemento complexo de resposta a receptores nucleares (ECRRN). Ensaios de transativação celular indicam que alguns receptores nucleares se ligam nesta região. A partir destes ensaios verificamos a ativação do promotor por um receptor nuclear, o COUP-TFII. Ele regula muitos processos biológicos, como angiogênese e o próprio desenvolvimento atrial. Através da deleção do ECRRN observamos que o promotor não era ativado por COUP-TFII, indicando a sua ligação nessa região. Verificamos ainda que somente o domínio de ligação ao ligante do COUP-TFII é capaz de ativar o promotor, sugerindo a necessidade de uma interação com outros RNs para ativar o promotor. Uma análise proteômica indica que a maioria dos interactores de COUP-TFII está relacionada com complexos reguladores da transcrição e com a via de sinalização do receptor de andrógenos (AR). Ensaios de transativação celular mostram que juntos, COUP-TFII e AR, são capazes de aumentar a ativação do promotor. / It was determined that regulatory elements of the atrial-specific expression of the promoter SMyHC3 are contained in a complex nuclear receptor response element (CNRRE). Cellular transactivation assays indicated certain nuclear receptors (NR) can bind in this region. From these trials, was observed the promoter activation by a nuclear receptor, COUP-TFII. It regulates many biological processes such as angiogenesis and atrial development. Deletion of CNRRE resulted in no activation of the promoter by COUP-TFII, indicating their connection in this region. We also verified that only the ligand binding domain of COUP-TFII is able to activate the promoter, suggesting interaction with other NRs to activate it. A proteomic analysis revealed that most of COUP-TFII partners relates to complexes of transcription regulators and the androgen receptor (AR) signaling pathway. Cell transactivation assays showed that together, COUP - TFII and AR, are able to increase promoter activation.

Com a presença cada vez maior de sistemas computacionais e novas tecnologias no cotidiano das pessoas, garantir que eles não falhem e funcionem corretamente tornou-se algo de extrema importância. Além de indicar a qualidade do sistema, assegurar seu bom funcionamento é essencial para se evitar perdas, desde financeiras até de vidas. Uma das técnicas utilizadas para esta finalidade é a chamada verificação formal de programas. A partir da especificação do sistema, descrita numa linguagem formal, são definidas propriedades a serem satisfeitas e que certificariam a qualidade do software. Estas propriedades devem então ser implementadas para uso num verificador, que é a ferramenta responsável por executar a verificação e informar quais propriedades foram satisfeitas e quais não foram; no caso das propriedades terem sido violadas, o verificador deve indicar aos desenvolvedores os possíveis locais com código incorreto no sistema. A desvantagem do uso da verificação formal é, além do seu alto custo, a necessidade de haver pessoas com experiência em métodos formais para definir propriedades a partir da especificação formal do sistema, e convertê-las numa representação que possa ser entendida pelo verificador. Este processo de definição de propriedades é particularmente complexo, demorado e suscetível a erros, por ser feito em sua maior parte de forma manual. Para auxiliar os desenvolvedores na utilização da verificação formal em programas escritos em Java, propomos neste trabalho a geração de representação de propriedades para uso direto num verificador. As propriedades a serem geradas são objetivos de teste derivados da especificação formal do sistema. Estes objetivos de teste descrevem o comportamento esperado do sistema que deve ser observado durante sua execução. Ao estabelecer que o universo de propriedades corresponde ao universo de objetivos de teste do programa, garantimos que as propriedades geradas em nosso trabalho descrevem o comportamento esperado do programa por meio de caminhos de execução que levam a um estado de aceitação da propriedade, ou a um estado de violação. Assim, quando o verificador checa o objetivo de teste, ele consegue dar como resultado o veredicto de sucesso ou falha para a propriedade verificada, além de dados da cobertura dos caminhos de execução do programa que podem ser usados para análise do comportamento do programa que levou ao sucesso ou falha da propriedade verificada. / The task of guaranteeing that computational systems do not fail and work correctly has become extremely important with the growing presence of new technologies in people\'s lives. Therefore, it is essential to ensure that such systems work properly to confirm their high-quality and to avoid financial and even life losses. One of the techniques used to this purpose is called formal verification of programs. From the system specification, which should be described in a formal language, we define properties that must be satisfied during system execution to guarantee the software quality. Then, these properties are checked using a verifier, which is the tool responsible for running the verification and for notifying whether the property was satisfied by the program; if the property was violated, it indicates to software developers the possible location of faults in the system. The disadvantages of using formal verification are the high cost to apply this technique in practice, and the necessity of having people with experience in formal methods to derive the properties from system specification and define them in a formal representation that can be read by a program verifier. This particular task of deriving a property from system specification and defining it to be checked by a verifier is complex, time-consuming and error-prone, since it is usually done by hand. To help software developers in the application of formal verification in Java programs, we propose in this work the generation of properties formal representation for direct use in a verifier. The generated properties are test purposes, which are derived from system formal specification and present the desirable system behavior that must be observed during the system execution. Establishing that the universe of properties correspond to the universe of test purposes of a program, we guarantee that the generated properties describe the expected program behavior through execution traces that lead to either an accept state or a refuse state. Thus, when the verifier checks the test purpose, it can give a success/fail verdict for the property, and provide traces coverage data that can be used to analyze the program behavior that led to that verdict.

O desenvolvimento de arquiteturas de controle para veículos submarinos é uma tarefa complexa. Estas podem ser caracterizadas pelos seguintes atributos: tempo real, multitarefa, concorrência e comunicações distribuídas em rede. Neste cenário, existem múltiplos processos sendo executados em paralelo, possivelmente distribuídos, e se comunicando uns com os outros. Neste contexto, o modelo comportamental pode levar a fenômenos como deadlocks, livelocks, disputa por recursos, entre outros. A fim de se tentar minimizar os efeitos de tais dificuldades, neste trabalho será apresentado um método para checagem de modelos de arquiteturas de controle de veículos submarinos baseado em Especificações Formais. A linguagem de especificação formal escolhida foi CSP-OZ, uma combinação de CSP e Object-Z. Object-Z é uma extensão orientada a objetos da linguagem Z para a especificação de predicados, tipicamente pré e pós condições, além de invariantes de dados. CSP (Communicating Sequential Process) é uma álgebra de processos desenvolvida para descrever modelos comportamentais de processos paralelos. A checagem de modelos especificados formalmente consiste na análise das especificações para verificar se um sistema possui certas propriedades através de uma busca exaustiva em todos os estados em que este pode entrar durante sua execução. Neste contexto, é possível checar corretude, livelocks, deadlocks, etc. Além disso, pode-se relacionar duas especificações diferentes a fim de se checar relações de refinamento. Para as especificações, o verificador de modelos FDR da Formal Systems Ltd. será utilizado. A implementação é desenvolvida utilizando um perfil da linguagem Ada denominado RavenSPARK, uma junção do perfil Ravenscar (desenvolvido na Universidade de York) com a linguagem SPARK (um subconjunto da linguagem Ada desenvolvido pela Praxis, Inc.). O Ravenscar é um perfil para desenvolvimento de processos, e portanto os processos de CSP, incluindo seus canais de comunicação, podem ser facilmente criados. Por outro lado, SPARK é uma linguagem onde podem ser inseridos predicados para os dados (originalmente especificados em Object-Z) utilizando anotações da própria linguagem. A linguagem SPARK possui uma ferramenta, o Examinador, que pode checar códigos de modelos baseado nestas anotações. Em resumo, o método proposto permite tanto a checagem de modelos em CSP quanto a checagem no nível de código. Para isso, as especificações em Object-Z devem inicialmente ser convertidas em um código na linguagem SPARK juntamente com suas respectivas anotações, para que então a checagem do modelo possa ser realizada no código. O desenvolvimento de uma arquitetura de controle reativa para um ROV denominado VSOR (Veículo Submarino Operado Remotamente) é utilizado como exemplo de uso do método proposto. Toda a arquitetura de controle é codificada utilizando a linguagem Ada com o perfil RavenSPARK e embarcada em um computador do tipo PC104 com o sistema operacional de tempo real VxWorks, da Windriver, Inc. / The development of control architectures for Underwater Vehicles is a complex task. These control architectures might be chracterised by the following attributes: real-time, multitasking, concurrency, and distributed over communication networks. In this scenario, we have multiple processes running in parallel, possibly distributed, and engaging in communication between each other. In this context, the behavioural model might lead to phenomena like deadlocks, livelocks, race conditions, among others. In order to try to minimize the effects of such difficulties, in this work a method for model checking control architectures of underwater vehicles based on formal specifications is presented. The chosen formal specification language is CSP-OZ, a combination of CSP and Object-Z. Object-Z is an object-oriented extension of Z for the specification of predicates, typically, data pre, post and invariant conditions. CSP (Communicating Sequential Process) is a process algebra developed to describe behavioural models of parallel process. The model checking of formal specifications is a task of reasoning on specifications in which a system verifies certain properties by means of an exhaustive search of all possible states that a system could enter during its execution. In this context, it is possible to check about correctness, liveness, deadlock, etc. Also, one can relate two different specifications in order to check a refinement ordering. For the specifications, the model checker FDR of Formal Systems Ltd. is utilised. The implementation is developed using an ADA language profile called RavenSPARK, a union of the Ravenscar profile (developed at the University of York) and the SPARK language (a subset of the ADA language developed by Praxis, Inc.). The Ravenscar is a profile for developing processes, so CSP processes including their message channels can be easily deployed. On the other hand, SPARK is a language where one can insert data predicates (originally specified in Object-Z) using language annotations. The SPARK language has a tool, the Examiner, that can model check code based on these annotations. In summary, the proposed method allows model checking of CSP processes but does not allow any checking in the code level. On the contrary, Object-Z specifications must first be converted into a SPARK language code, together with proper annotations, and then model checking can be realised in code. The development of a real-time reactive control architecture of an ROV named VSOR (Veiculo Submarino Operado Remotamente) is used as an example of the use of the proposed method. The whole control architecture is coded using the ADA Language with the RavenSPARK profile and deployed into a PC104 cpu system running the Vxworks real-time operating system of Windriver, Inc.

Les travaux présentés dans ce mémoire s'inscrivent dans le contexte de l'Ingénierie d'un Système Interactif d'Aide à la Conduite (SIAC) d'un procédé industriel. Nous défendons l'intérêt d'améliorer l'interactivité numérique entre un procédé et un agent (opérateur de conduite, rondier) qui applique des procédures de conduite. L'originalité du SIAC consiste à encapsuler le système physique par un canal d'objets logiques afin de mieux équilibrer la distribution des rôles entre l'humain et le système technique qu'il conduit. Ce SIAC fournit aux opérateurs et aux rondiers des services d'aide à la conduite tels que la localisation des équipements, l'autorisation des actions à exécuter et la validation des actions exécutées, de même que la gestion des contraintes d'exclusion et de dépendances entre actions, imposées par la physique du procédé. La spécification de ce système sociotechnique interprète les travaux des « Problem Frames » en génie informatique pour proposer un procédé de modélisation itératif dans le cadre d'une Ingénierie Système Basée sur des Modèles (ISBM). Cette ISBM s'appuie sur le langage SysML, dont la syntaxe et la sémantique sont spécialisées pour supporter le procédé de modélisation proposé. Cette spécialisation met en correspondance les artéfacts clés extraits à la fois des bonnes pratiques de l'Ingénierie Système et des bonnes pratiques de SysML. / Within the context of the Engineering of an Interactive Aiding System for industrial process Control (SIAC), these works aims to improve the digital interaction between a process and a human operator (control room operator, field operator) which applies control procedures. The proposed SIAC enhances the digital capabilities of the field operator in order to better balance the role distribution between the technical system and the human system. It provides active control services to field operators such as equipment localisation, action authorization and action validation, as well as man-agement services for the verification of exclusions between procedures constraints and verification of de-pendencies between actions constraints.The specification of such socio-technical system interprets the ?Problem Frames? from software engineer-ing in order to propose an iterative Model Based System Engineering (MBSE) process. This MBSE is based on SysML modelling language, whose syntax and semantics are specialized to support the proposed meth-odology. This specialization maps the key artefacts that are extracted from the System Engineering and SysML good practices.

Le développement de spécifications formelles correctes pour des systèmes et logiciels commence par l’analyse et la compréhension des besoins du client. Entre ces besoins décrits en langage naturel et leur spécification définie dans un langage formel précis, un écart existe et rend la tâche de développement de plus en plus difficile à accomplir. Nous sommes face à deux mondes distincts. Ce travail de thèse a pour objectif d’expliciter et d’établir des interactions entre ces deux mondes et de les faire évoluer en même temps. Par interaction, nous désignons les liens, les échanges et les activités se déroulant entre les différents documents. Parmi ces activités, nous présentons la validation comme un processus rigoureux qui démarre dès l’analyse des besoins et continue tout au long de l’élaboration de leur spécification formelle. Au fur et à mesure du développement, des choix sont effectués et les retours des outils de vérification et de validation permettent de détecter des lacunes aussi bien dans les besoins que dans la spécification. L’évolution des deux mondes est décrite via l’introduction d’un nouveau besoin dans un système existant et à travers l’application de patrons de développement. Ces patrons gèrent à la fois les besoins et la spécification formelle associée ; ils sont élaborés à partir de la description de la forme des besoins. Ils facilitent la tâche de développement et aident à éviter les risques d’oublis. Quel que soit le choix, des questions se posent tout au long du développement et permettent de déceler des lacunes, oublis ou ambiguïtés dans l’existant. / The development of correct formal specifications for systems and software begins with the analysis and understanding of client requirements. Between these requirements described in natural language and their specification defined in a specific formal language, a gap exists and makes the task of development more and more difficult to accomplish. We are facing two different worlds. This thesis aims to clarify and establish interactions between these two worlds and to evolve them together. By interaction, we mean all the links, exchanges and activities taking place between the different documents. Among these activities, we present the validation as a rigorous process that starts from the requirements analysis and continues throughout the development of their formal specification. As development progresses, choices are made and feedbacks from verification and validation tools can detect shortcomings in requirements as well as in the specification. The evolution of the two worlds is described via the introduction of a new requirement into an existing system and through the application of development patterns. These patterns manage both the requirements and their associated formal specifications ; they are elaborated from the description of the form of the requirements in the client document. They facilitate the task of development and help to avoid the risk of oversights. Whatever the choice, the proposed approach is guided by questions accompanying the evolution of the whole system and makes it possible to detect imperfections, omissions or ambiguities in the existing.

Estuda-se o problema de sintonia de controladores, objetivando-se a formulação do problema de sintonia ótima de controladores. Busca-se uma formulação que seja geral, ou seja, válida para qualquer estrutura de controlador e qualquer conjunto de especificações. São abordados dois temas principais: especificação de controladores e sintonia ótima de controladores. São compiladas as principais formas de especificação e avaliação de controladores e é feita a formulação do problema de sintonia de controladores como um problema padrão de otimização. A abordagem proposta e os conceitos apresentados são então aplicados em um conjunto de exemplos. / The problem of control tuning is studied, aiming the formulation of the optimal control tuning problem. A general formulation, valid for any controller structure and any set of specifications, is sought. Two main themes are addressed: controller specification and optimal controller tuning. The main ways of controller specification and assessment are compiled and the optimal controller tuning problem is formulated as a standard optimization problem. The proposed approach and the presented concepts are then applied in a set of examples.

Several recent empirical studies, particularly in the regional economic growth literature, emphasize the importance of explicitly accounting for uncertainty surrounding model specification. Standard approaches to deal with the problem of model uncertainty involve the use of Bayesian model-averaging techniques. However, Bayesian model-averaging for spatial autoregressive models suffers from severe drawbacks both in terms of computational time and possible extensions to more flexible econometric frameworks. To alleviate these problems, this paper presents two global-local shrinkage priors in the context of high-dimensional matrix exponential spatial specifications. A simulation study is conducted to evaluate the performance of the shrinkage priors. Results suggest that they perform particularly well in high-dimensional environments, especially when the number of parameters to estimate exceeds the number of observations. Moreover, we use pan-European regional economic growth data to illustrate the performance of the proposed shrinkage priors.

Hardware engineers frequently create formal specification documents as part of the verification process. Doing so is a time-consuming and error-prone process, as the primary documents for communications and standards use a mixture of prose, diagrams and tables. We would like this process to be partially automated, in which the engineer's role would be to refine a machine-generated skeleton of a specification's formal model. We have created a preliminary intermediate language which allows specifications to be captured using formal semantics, and allows an engineer to easily find, understand, and modify critical portions of the specification. We have converted most of ARM's AMBA AHB specification to our language; our representation is able to follow the structure of the original document.

Dans le domaine de l'Interaction Homme-Machine, nos travaux concernent l'interaction multiutilisateur et multimodale. Exploitant les avancées importantes en terme de modalités d'interaction, de nombreux collecticiels reposent sur une combinaison de modalités, comme les systèmes multiutilisateurs autour d'une table augmentée. Néanmoins ces systèmes constituent des réalisations ad-hoc en l'absence d'outils de conception. Face à constat, nos contributions conceptuelles et logicielles concernent la phase de spécification de l'interaction multiutilisateur et multimodale. Nous présentons une notation de spécification notée COMM (COllaborative et MultiModale) qui est une extension de CTT par l'introduction de deux concepts, le rôle interactif et la tâche modale, et par la spécialisation des opérateurs temporels, en s'appuyant sur les relations de Allen. La notation COMM est instrumentée par un éditeur logiciel de spécifications COMM, nommé e-COMM ((http://iihm.imag.fr/demo/editeur/). COMM et e-COMM ont été utilisés dans un projet DGA de taille conséquente pour spécifier l'interaction au sein d'un poste de commande de drones militaires. / Multi-user multimodal interactive systems involve multiple users that can use multiple interaction modalities. Although multi-user multimodal systems are becoming more prevalent (especially multi-user multimodal systems involving multi-touch surfaces), their design is still ad-hoc without properly keeping track of the design process. Addressing this issue of lack of design tools, our doctoral research is dedicated to the specification of multi-user multimodal interaction. The doctoral research contributions include the COMM (Collaborative and MultiModal) notation and its on-line editor for specifying multi-user multimodal interactive systems. Extending the CTT notation, the salient features of the COMM notation include the concepts of interactive role and modal task as well as a refinement of the temporal operators applied to tasks using the Allen relationships. The COMM notation and its on-line editor e-COMM (http://iihm.imag.fr/demo/editeur/) have been successfully applied to a large scale project dedicated to a multimodal military command post for the control of unmanned aerial vehicles (UAV) by two operators.

Les applications Web sont très populaires et l'utilisation de certaines d'entre elles (p. ex. Facebook, Google) fait de plus en plus partie de nos vies. Les développeurs sont impatients de créer diverses applications Web pour répondre à la demande croissante des gens. Pour construire une application Web, les développeurs doivent connaître quelques technologies de programmation de base. De plus, ils préfèrent utiliser certains composants tiers (tels que les bibliothèques côté serveur, côté client, services REST) dans les applications web. En incluant ces composants, ils pourraient bénéficier de la maintenabilité, de la réutilisabilité, de la lisibilité et de l'efficacité. Dans cette thèse, nous proposons d'aider les développeurs à utiliser des composants tiers lorsqu'ils créent des applications web. Nous présentons trois obstacles lorsque les développeurs utilisent les composants tiers: Quelles sont les meilleures bibliothèques JavaScript à utiliser? Comment obtenir les spécifications standard des services REST? Comment s'adapter aux changements de données des services REST? C'est pourquoi nous présentons trois approches pour résoudre ces problèmes. Ces approches ont été validées par plusieurs études de cas et données industrielles. Nous décrivons certains travaux futurs visant à améliorer nos solutions et certains problèmes de recherche que nos approches peuvent cibler. / Web applications are highly popular and using some of them (e.g., Facebook, Google) is becoming part of our lives. Developers are eager to create various web applications to meet people's increasing demands. To build a web application, developers need to know some basic programming technologies. Moreover, they prefer to use some third-party components (such as server-side libraries, client-side libraries, REST services) in the web applications. By including those components, they could benefit from maintainability, reusability, readability, and efficiency. In this thesis, we propose to help developers to use third-party components when they create web applications. We present three impediments when developers using the third-party components: What are the best JavaScript libraries to use? How to get the standard specifications of REST services? How to adapt to the data changes of REST services? As such, we present three approaches to solve these problems. Those approaches have been validated through several case studies and industrial data. We describe some future work to improve our solutions, and some research problems that our approaches can target.