La méthodologie HILECOP a été élaborée pour la conception formelle de systèmes numériques complexes critiques ; elle couvre donc l'intégralité du processus, allant de la modélisation à la génération de code pour l’implantation sur la cible matérielle (composant électronique de type FPGA), en passant par la validation formelle. Or, si le modèle formel, les réseaux de Petri en l'occurrence, est par essence asynchrone, il est néanmoins exécuté de manière synchrone sur la cible. De fait, les approches d'analyse usuelles ne sont pas adaptées au sens où elles construisent des graphes d'états non conformes à l'évolution d'états réelle au sein de la cible. Dans l'objectif de gagner en confiance quant à la validité des résultats de l’analyse formelle, ces travaux visent à capturer les caractéristiques dites non-fonctionnelles, à les réifier sur le modèle et enfin à considérer leur impact à travers l’analyse. En d’autres termes, l’objectif est d’améliorer l’expressivité du modèle et la pertinence de l'analyse, en considérant des aspects comme la synchronisation d'horloge, le parallélisme effectif, le risque de blocage induit par l'expression conjointe d'un événement (condition) et d'une fenêtre temporelle d'occurrence, sans omettre la gestion des exceptions. Pour traiter tous ces aspects, nous avons proposé une nouvelle méthode d'analyse pour les réseaux de Petri temporels généralisés étendus interprétés exécutés en synchrone, en les transformant vers un formalisme équivalent analysable. Ce formalisme est associé avec une sémantique formelle intégrant toutes les aspects particuliers de l'exécution et un algorithme de construction d'un graphe d'états spécifique : le Graphe de Comportement Synchrone. Nos travaux ont été appliqués à un cas industriel, plus précisément à la validation du comportement de la partie numérique d'un neuro-stimulateur. / The HILECOP methodology has been developed for the formal design of critical complex digital systems; it therefore covers the entire design process, ranging from modeling to code generation for implementation on the hardware target (FPGA type electronic component), via formal validation. However, if the formal model, the Petri nets in this case, is inherently asynchronous, it is nevertheless executed synchronously on the target. In fact, the usual analysis approaches are not adapted in the sense that they construct state graphs that do not conform to the real state evolution within the target. In order to gain confidence in the validity of the results of the formal analysis, this work aims to capture the so-called non-functional characteristics, to reify them on the model and finally to consider their impact through the analysis.In other words, the aim is to improve the expressiveness of the model and the relevance of the analysis, considering aspects such as clock synchronization, effective parallelism, the risk of blocking induced by the expression of an event (condition) and a time window of occurrence, without omitting the management of exceptions.To deal with all these aspects, we have proposed a new method of analysis for extended generalized synchronous executed time Petri nets, transforming them into an analysable equivalent formalism. This formalism is associated with a formal semantics integrating all the particular aspects of the execution and dédicated state space construction algorithm: the Synchronous Behavior Graph.Our work has been applied to an industrial case, more precisely to the validation of the behavior of the digital part of a neuro-stimulator.

O crítico Roberto Schwarz, pensador da cultura, assume o ângulo estético como primazia para a interpretação da sociedade brasileira. Sua obra perpassa diversos âmbitos da produção cultural, mobilizando a relação entre análise formal e crítica social. Assumindo a importância da sua trajetória intelectual, esta dissertação dá ênfase à sua contribuição em relação ao debate sobre Arquitetura. À luz desta questão apresenta-se um percurso sobre seus ensaios, buscando-se elucidar suas análises, referências e pressupostos, assim como suas implicações para o significado da crítica de arquitetura diante dos impasses históricos por esta enfrentados no presente. / The critic Roberto Schwarz, thinker of culture, assumes the aesthetic perspective as a primacy for an interpretation of the Brazilian society. His essayistic production overviews a diversity of cultural productions, putting in motion the connection between formal analysis and social critics. Taking on the importance of his intellectual trajectory, this dissertation emphasizes his contributions about Architecture discussion. Considering this question, this work shows a way among his essays, seeking to elucidate his analysis, references, premisses and also their implications for the meaning of the Architecture criticism, forward the historical dilemmas that it presently faces.

A dissertação investiga possibilidades formais de articulação entre universos pessoais e processos históricos no campo da realização documentária em primeira pessoa. O ponto de partida são materiais e procedimentos advindos de um documentário de longa-metragem que atualmente desenvolvo, intitulado Bem vindos de novo. O filme aborda as experiências da minha família na imigração de nipo-brasileiros para o Japão, conhecida como \"fenômeno decasségui\". Nele, busco articular as experiências pessoais e familiares com aspectos mais amplos desse acontecimento histórico e social, de proporções internacionais, que atingiu, e continua afetando diretamente, cerca de 600 mil pessoas. Abordo três procedimentos formais empregados no filme: (1) a utilização de fotografias domésticas; (2) a elaboração da narração em voz over; (3) o emprego de filmagens históricas realizadas por Hikoma Udihara, colonizador e cinegrafista pioneiro da imigração japonesa no Brasil. Através do mapeamento de possibilidades formais relacionadas aos procedimentos em questão, busco identificar e analisar um conjunto de conceitos, de instrumentos críticos e teóricos, úteis para se pensar a articulação entre o íntimo e o histórico, o pessoal e o social, em documentários na primeira pessoa; em diálogo constante com aspectos concretos da realização cinematográfica. / This master\'s thesis investigates formal possibilities of articulation between personal universes and historical processes inside the first person filmmaking practice. The bases are materials and procedures related to a feature documentary film that I am now developing, called Welcome Back, Farewell (Bem vindos de novo). The film addresses my family experiences in immigration of Japanese-Brazilians to Japan, known as \"dekassegui phenomenon\". In the film, I try to articulate personal and familiar experiences with wider features of this historical and social event of international proportion, which reached, and still concerns directly to six hundreds thousand people. Three formal procedures of the film are covered: (1) the use of domestic photography; (2) the elaboration of the voice over narration; (3) the usage of historical footage produced by Hikoma Udihara, colonizer and pioneer amateur filmmaker of the Japanese immigration in Brazil. Through the organization of formal possibilities related with the previous procedures, the aim is to identify and analyze a group of concepts, of critical and theoretical devices, useful to think the articulation between the intimate and the historical, the personal and the social, within the first person documentary; in frequent contact with concrete features of the filmmaking practice.

Made available in DSpace on 2014-06-11T19:22:20Z (GMT). No. of bitstreams: 0 Previous issue date: 2006-08-07Bitstream added on 2014-06-13T19:48:36Z : No. of bitstreams: 1 mannis_gdb_me_ia.pdf: 3194427 bytes, checksum: 2374fc542cb39f88a904a9fe24e7d7ef (MD5) / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES) / O presente trabalho de mestrado tem como seu principal objetivo demonstrar que a aplicação de diferentes métodos analíticos a uma mesma obra e sua posterior comparação é uma metodologia eficaz para o estudo da linguagem musical, em particular de uma obra específica e que, através deste procedimento, informações de interesse teórico e interpretativo, que vão além da aplicação isolada de cada método, podem ser alcançadas. Para tanto, foi feita a análise de um movimento de grande duração inserido em uma obra extensa, composta pelo austríaco Gustav Mahler (1860-1911): a Sinfonia nº3. Sobre esta obra foram realizadas três análises: formal segundo Schoenberg e Rosen; motívica, segundo Réti; e schenkeriana, segundo Salzer.Os métodos foram comparados entre si, de modo a identificarem-se as convergências e divergências entre eles; com base nas divergências e convergências, foramindicadas possibilidades de leitura da obra. Ao final, estes resultados foram confrontados com gravações realizadas por grandes orquestras, tendo à frente regentes reconhecidos como grandes intérpretes da obra de Mahler, verifinco como foram solucionados os problemas de divergência analítica e observando, ainda, se as convergências podem ser confirmadas em suas interpretações. / The present Master's Degree dissertation seeks to demonstrate that the utilization of different analytical methods to a single opus, and their posterior comparation, in an efficient method for the study of musical language, particularly of an specific opus, and that, through this procedure, information on theoretical and interpretative interest that go beyond the isolated utilization of each method can be reached. Therefore, three analysis of the first movement of Gustav Mahler's 3rd Symphony were made. The three analysis were; formal, according to Schoenberg and Rosen; motivic according to Réti; and schenkerian, according to Salzer. The methods were compared to each other so it would be possible to identify similarities and differences amont them. Then, based on these similarities and differences, possibilities of reading of the work were indicated. In the end, these results were confronted with recording made by great orchestras, conducted by great maestros well-known as great interpreters of Mahler's opus, verifying how the problems of analytical diffrences were resolved and observing as well if the similarities coud be confirmed in their interpretations.

[pt] Atualmente, podemos observar uma clara tendência na direção de sistemas cada vez maiores e mais complexos quanto às suas partes e formas de interconexão. Num cenário como este, torna-se imperativa a preocupação com a modelagem da estrutura, organização geral e formas de interação presentes nesses sistemas, assim como com as garantias de que certos requisitos críticos sejam atendidos. O contexto de nosso trabalho engloba disciplinas de Engenharia de Software, como Arquitetura de Software e Técnicas de Modelagem, e disciplinas mais formais como Verificação de Modelos, Lógicas Modais e Álgebras de Processos. Nosso trabalho tem inspirações nestas disciplinas mas apresenta, de fato, um cunho metodológico, localizando-se nas fronteiras da ES com Métodos Formais, onde buscamos investigar e estabelecer uma forma sistemática para utilização efetiva de métodos formais logo nas etapas iniciais do desenvo lvimento. Mais especificamente, mostramos como é possível, a partir de modelos baseados em abstrações arquiteturais, obter-se sistematicamente um modelo formal sobre o qual possamos realizar certos tipos de análise comportamental. Nossa proposta inclui um sistema notacional básico para expressar modelos arquiteturais, junto com sua semântica formal, e um protótipo construído para dar suporte a tarefas de especificação e análise formal orientadas por abstrações arquiteturais. Com isto, pretendemos abordar alguns dos aspectos essenciais de uma metodologia de desenvolvimento que integre ferramentas e técnicas formais na etapa de modelagem arquitetural. / [en] There is a trend nowadays towards bigger and more complex systems concerning their parts and interconnectivity. In such scenario, modeling structure, overall organization and interaction have become a main concern, as well as fulfillment of mission critical requirements. The scope of our work encompasses Software Engineering related subjects such as Software Architecture, Modeling Techniques and more formal disciplines like Model Checking, Modal Logics and Process Algebra. Although inspired by such techniques, there is, indeed a methodological orientation in our work, traversing the boundaries of Software Engineering with Formal Methods, through which we seek to investigate and establish a systematic way for the effective utilization of formal methods in the first steps of software development. Still, more specifically, we show how it is possible, starting from models based on architectural abstractions, to systematically produce a formal model upon which we can execute certain forms of behavior analysis. Our proposal includes a basic notational system to express architectural models along with their formal semantics and a prototype built to support specification and formal analysis tasks oriented by architectural abstractions. With this, we intend to stress some essential aspects of a development methodology which aims to integrate tools and formal techniques to software modeling.

This thesis makes a survey on conception of &ldquo / surface&rdquo / in the works of Peter Eisenman. In doing so, the concept of &ldquo / surface&rdquo / is discussed under three titles: &ldquo / Surface&rdquo / as an element of architectural vocabulary (as a formal element), as an analytical tool (as a grammar), and as a diagrammatic tool. Correspondingly, the thesis is intended to examine how &ldquo / surface&rdquo / is conceptualized and handled through the critical readings of Eisenman&rsquo / s writings, and projects are referred in order to support and visualize the discussions. In this context, Eisenman&rsquo / s dissertation, The Formal Basis of Modern Architecture (1963), reveals the definition of architectural surface in relation to the architectural language that is proposed by him. Through the formal analysis of Giuseppe Terragni&rsquo / s building, Casa Guiliani Frigerio, he utilizes surface as an analytical tool. Considering design processes of his projects, as discussed in the book Diagram Diaries (1999), surface becomes a dominant tool for generating architectural form. As a result, in this thesis, surface is evaluated in various aspects (as a formal, analytical and diagrammatic tool) that are essential for understanding of architectural form. In the case of Eisenman, its significance dominates the way of developing his architecture.

O crítico Roberto Schwarz, pensador da cultura, assume o ângulo estético como primazia para a interpretação da sociedade brasileira. Sua obra perpassa diversos âmbitos da produção cultural, mobilizando a relação entre análise formal e crítica social. Assumindo a importância da sua trajetória intelectual, esta dissertação dá ênfase à sua contribuição em relação ao debate sobre Arquitetura. À luz desta questão apresenta-se um percurso sobre seus ensaios, buscando-se elucidar suas análises, referências e pressupostos, assim como suas implicações para o significado da crítica de arquitetura diante dos impasses históricos por esta enfrentados no presente. / The critic Roberto Schwarz, thinker of culture, assumes the aesthetic perspective as a primacy for an interpretation of the Brazilian society. His essayistic production overviews a diversity of cultural productions, putting in motion the connection between formal analysis and social critics. Taking on the importance of his intellectual trajectory, this dissertation emphasizes his contributions about Architecture discussion. Considering this question, this work shows a way among his essays, seeking to elucidate his analysis, references, premisses and also their implications for the meaning of the Architecture criticism, forward the historical dilemmas that it presently faces.

A dissertação investiga possibilidades formais de articulação entre universos pessoais e processos históricos no campo da realização documentária em primeira pessoa. O ponto de partida são materiais e procedimentos advindos de um documentário de longa-metragem que atualmente desenvolvo, intitulado Bem vindos de novo. O filme aborda as experiências da minha família na imigração de nipo-brasileiros para o Japão, conhecida como \"fenômeno decasségui\". Nele, busco articular as experiências pessoais e familiares com aspectos mais amplos desse acontecimento histórico e social, de proporções internacionais, que atingiu, e continua afetando diretamente, cerca de 600 mil pessoas. Abordo três procedimentos formais empregados no filme: (1) a utilização de fotografias domésticas; (2) a elaboração da narração em voz over; (3) o emprego de filmagens históricas realizadas por Hikoma Udihara, colonizador e cinegrafista pioneiro da imigração japonesa no Brasil. Através do mapeamento de possibilidades formais relacionadas aos procedimentos em questão, busco identificar e analisar um conjunto de conceitos, de instrumentos críticos e teóricos, úteis para se pensar a articulação entre o íntimo e o histórico, o pessoal e o social, em documentários na primeira pessoa; em diálogo constante com aspectos concretos da realização cinematográfica. / This master\'s thesis investigates formal possibilities of articulation between personal universes and historical processes inside the first person filmmaking practice. The bases are materials and procedures related to a feature documentary film that I am now developing, called Welcome Back, Farewell (Bem vindos de novo). The film addresses my family experiences in immigration of Japanese-Brazilians to Japan, known as \"dekassegui phenomenon\". In the film, I try to articulate personal and familiar experiences with wider features of this historical and social event of international proportion, which reached, and still concerns directly to six hundreds thousand people. Three formal procedures of the film are covered: (1) the use of domestic photography; (2) the elaboration of the voice over narration; (3) the usage of historical footage produced by Hikoma Udihara, colonizer and pioneer amateur filmmaker of the Japanese immigration in Brazil. Through the organization of formal possibilities related with the previous procedures, the aim is to identify and analyze a group of concepts, of critical and theoretical devices, useful to think the articulation between the intimate and the historical, the personal and the social, within the first person documentary; in frequent contact with concrete features of the filmmaking practice.

Since the first lines of code were introduced in the automotive domain, vehicles have transitioned from being predominantly mechanical systems to software intensive systems. With the ever-increasing computational power and memory of vehicular embedded systems, a set of new, more powerful and more complex software functions are installed into vehicles to realize core functionalities. This trend impacts all phases of the system development including requirements specification, design and architecture of the system, as well as the integration and testing phases. In such settings, creating and managing different artifacts during the system development process by using traditional, human-intensive techniques becomes increasingly difficult. One problem stems from the high number and intricacy of system requirements that combine functional and possibly timing or other types of constraints. Another problem is related to the fact that industrial development relies on models, e.g. developed in Simulink, from which code may be generated, so the correctness of such models needs to be ensured. A potential way to address of the mentioned problems is by applying computer-aided specification, analysis and verification techniques already at the requirements stage, but also further at later development stages. Despite the high degree of automation, exhaustiveness and rigor of formal specification and analysis techniques, their integration with industrial practice remains a challenge. To address this challenge, in this thesis, we develop the foundation of a framework, tailored for industrial adoption, for formal specification and analysis of system requirements specifications and behavioral system models. First, we study the expressiveness of existing pattern-based techniques for creating formal requirements specifications, on a relevant industrial case study. Next, in order to enable practitioners to create formal system specification by using pattern-based techniques, we propose a tool called SeSAMM Specifier. Further, we provide an automated Satisfiability Modulo Theories (SMT)-based consistency analysis approach for the formally encoded system requirements specifications. The proposed SMT-based approach is suitable for early phases of the development for debugging the specifications. For the formal analysis of behavioral models, we provide an approach for statistical model checking of Simulink models by using the UPPAAL SMC tool. To facilitate the adoption of the approach, we provide the SIMPPAAL tool that automates procedure of generating network of stochastic timed automata for a given Simulink model. For validation, we apply our approach on a complex industrial model, namely the Brake-by-Wire function from Volvo GTT. / VeriSpec

Formal analysis of security protocols is becoming increasingly relevant. In formal analysis, a model is created of a protocol or system, and propositions about the security of the model are written. A program is then used to verify that the propositions hold, or find examples of where they do not. This report uses formal methods to analyse the authentication aspect of a protocol that allows private individuals, enterprises, and systems to securely and asynchronously share sensitive data. Unpublished, early drafts of the protocol were studied and algorithms described in it were verified with the help of the formal verification tool Tamarin Prover. The analysis revealed two replay attacks. Improvements to the protocol were suggested based on this analysis. In later versions of the protocol, the improvements have been implemented by the protocol developers. / Det blir alltmer relevant med formell analys av säkerhetsprotokoll. I formell analys så skapas en modell av ett protokoll eller ett system, och påståenden om modellens säkerhet skrivs. Ett program används sedan för att verifiera att påståendena gäller, eller för att hitta exempel där de inte gäller. Den här rapporten avänder formella metoder för att analysera autentiseringsaspekten av ett protokoll som tillåter privatpersoner, företag och system att asynkront dela känslig information på ett säkert sätt. Opublicerade och tidiga utkast av protokollet studerades och de algoritmer som beskrivs i protokollet verifierades med hjälp av Tamarin Prover. Analysen avslöjade två återspelningsattacker. Förbättringar till protokollet föreslogs baserat på denna analys. I senare versioner har protokollutvecklarna implementerat förslagen.