Made available in DSpace on 2014-06-12T15:52:55Z (GMT). No. of bitstreams: 1 license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2009 / Nos últimos anos, a redução do consumo de energia das aplicações dos sistemas embarcados tem recebido uma grande atenção da comunidade científica, visto que, como o tempo de resposta e o baixo consumo de energia são requisitos conflitantes, esses estudos tornam-se altamente necessários. Nesse contexto, é proposta uma metodologia aplicada nas fases iniciais de projeto para dar suporte às decisões relativas ao consumo de energia e ao desempenho das aplicações desses dispositivos embarcados. Al´em disso, esse trabalho propõe modelos temporizados de eventos discretos que são avaliados através de uma metodologia de simulção estocástica com o objetivo de representar diferentes cenários dos sistemas com facilidade. Dessa forma, para cada cenário ´e preciso decidir o n´umero máximo de simulações e o tamanho de cada rodada da simulação, onde ambos os fatores podem impactar no desempenho para se obter tais estimativas. Essa metodologia considera também, um modelo intermediário que representa a descrição do comportamento do sistema e, é através desse modelo que cenários são analisados. Esse modelo intermediário ´e baseado em redes de Petri coloridas temporizadas que permitem não somente a anáise do software, mas também fornece suporte a um conjunto de métodos bem estabelecidos para verificações de propriedades. É nesse contexto que o software, ALUPAS, responsável por estimar o consumo de energia e o tempo de execução dos sistemas embarcados é apresentado. Por fim, um caso de estudo real, assim como tamb´em, exemplos customizados são apresentados com a finalidade de mostrar a aplicabilidade desse trabalho, onde usuários não especializados não precisam interagir diretamente com o formalismo de redes de Petri.

Modern software systems have increasingly higher expectations on their reliability, in particular if the systems are critical and real-time. The development of these complex software systems requires strong modelling and analysis methods including quantitative modelling and formal verification. Unified Modelling Language (UML) is a widely used and intuitive graphical modelling language to design complex systems, while formal models provide a theoretical support to verify system design models. However, UML models are not sufficient to guarantee correct system designs and formal models, on the other hand, are often restrictive and complex to use. It is believed that a combined approach comprising the advantages of both models can offer better designs for modern complex software development needs. This thesis focuses on the design and development of a rigorous framework based on Model Driven Development (MDD) that facilitates transformations of non-formal models into formal models for design verification. This thesis defines and describes the transformation from UML2 sequence diagrams to coloured Petri nets and proves syntactic and semantic correctness of the transformation. Additionally, we explore ways of adding information (time, probability, and hierarchy) to a design and how it can be added onto extensions of a target model. Correctness results are extended in this context. The approach in this thesis is novel and significant both in how to establish semantic and syntactic correctness of transformations, and how to explore semantic variability in the target model for formal analysis. Hence, the motivation of this thesis establishes: the UML behavioural models can be validated by correct transformation of them into formal models that can be formally analysed and verified.

nÃo hà / Esse trabalho propÃe um novo mÃtodo para sÃntese de supervisores em sistemas a eventos discretos, utilizando redes de Petri coloridas, baseado no contexto da teoria de controle supervisÃrio. Como aspecto principal, tem-se a formalizaÃÃo teÃrica e a prova matemÃtica do mÃtodo para sÃntese desses supervisores, denominado RestriÃÃes de Controle sobre Cores Decompostas (RCCD). AlÃmdisso, como consequÃncia, à apresentado ummÃtodo para reduÃÃo do nÃmero de lugares de controle denominado FusÃo de Controladores (FC). Os mÃtodos RCCD e FC sÃo uma extensÃo do trabalho de Moody e Antsaklis, que propÃem, originalmente, um Teorema comprovando a sÃntese de supervisores usando redes de Petri ordinÃrias e, dessa forma, sÃo propostas aqui as extensÃes desse Teorema, para o contexto das redes de Petri coloridas. Nesse caso, explora-se a decomposiÃÃo da matriz de incidÃncia de uma rede de Petri colorida para de…nir lugares de controle que nÃo sÃo con‡itantes em suas aÃÃes, usando o soft CPNTools como ferramenta. A seguir, à realizada a fusÃo desses lugares de controle, obtidos com o RCCD, com a aplicaÃÃo do mÃtodo FC, em que o lugar de controle encontrado, denominado supervisor resultante da fusÃo, atende as mesmas restriÃÃes e contribui com a mesma performance de controle do sistema. / This work proposes a newmethod for synthesis of supervisors in discrete event systems using coloured Petri nets, based in the theory of supervisory control. As a main aspect, there is the theoretical and formal mathematical proof of the method for synthesis of supervisors, called Control Constraints on Decomposed Colors (CCDC). In addition, as a consequence, it is presented a method for reducing the number of control places called Fusion of Controllers (FC). The CCDC and FC methods are an extension of the work of Moody and Antsaklis, they propose, originally a theorem proving the synthesis of supervisors using Petri nets thus are proposed here extensions of this theorem to the context of coloured Petri nets. In this case, it is explored the decomposition of the incidence matrix of a coloured Petri net to de…ne control places that are not con‡icting in their actions, using the soft CPNTools. The following is realized the fusion of these control places obtained with CCDC, with the aplication of the FC method. The obtained place is called the resulting fusion supervisor, where it is found the same constraints and contributes with the same control system performance.

Le développement et l’application des langages formels sont un défi à long terme pour la science informatique. Un enjeu particulier est l’acceptation par l’industrie. Cette thèse présente une approche pour la modélisation et la vérification des postes d’aiguillage français. La première question est la modélisation du système d’enclenchement par les réseaux de Petri colorés (RdPC). Un cadre de modélisation générique et compact est introduit, dans lequel les règles d’enclenchement sont modélisées dans une structure hiérarchique, tandis que les installations sont modélisées dans une perspective géographique. Ensuite, un patron de modèle est présenté. C’est un modèle paramétré qui intègre les règles nationales françaises qui peut être appliquée pour différentes gares. Puis, un concept basé sur l’événement est présenté dans le processus de modélisation des parties basses des postes d’aiguillage. La deuxième question est la transformation des RdPCs en machines B, qui va aider les concepteurs sur la route de l’analyse à application. Tout d’abord, une méthodologie détaillée, s’appuyant sur une table de correspondance, du RdPCs non-hiérarchiques vers les notations B est présentée. Ensuite, la hiérarchie et la priorité des transitions du RdPC sont successivement intégrées dans le processus de mapping, afin d’enrichir les possibilités de types de modèles en entrées de la transformation. Les machines B produites par la transformation permettent la preuve automatique intégrale par l’Atelier B. L’ensemble de ces travaux, chacun à leur niveau, contribuent à renforcer l’efficacité d’un cadre global d’analyse sécuritaire / Development and application of formal languages are a long-standing challenge within the computer science domain. One particular challenge is the acceptance of industry. This thesis presents some model-based methodologies for modelling and verification of the French railway interlocking systems (RIS). The first issue is the modellization of interlocking system by coloured Petri nets (CPNs). A generic and compact modelling framework is introduced, in which the interlocking rules are modelled in a hierarchical structure while the railway layout is modelled in a geographical perspective. Then, a modelling pattern is presented, which is a parameterized model respecting the French national rules. It is a reusable solution that can be applied in different stations. Then, an event-based concept is brought into the modelling process of low-level part of RIS to better describe internal interactions of relay-based logic. The second issue is the transformation of coloured Petri nets into B machines, which can help designers on the way from analysis to implementation. Firstly, a detailed mapping methodology from non-hierarchical CPNs to abstract B machine notations is presented. Then the hierarchy and the transition priority of CPNs are successively integrated into the mapping process, in order to enrich the adaptability of the transformation. This transformation is compatible with various types of colour sets and the transformed B machines can be automatically proved by Atelier B. All these works at different levels contribute towards a global safe analysis framework