The specification of enterprise information systems using formal specification languages enables the formal verification of these systems. Reasoning about the properties of a formal specification is a tedious task that can be facilitated much through the use of an automated reasoner. However, set theory is a corner stone of many formal specification languages and poses demanding challenges to automated reasoners. To this end a number of heuristics has been developed to aid the Otter theorem prover in finding short proofs for set-theoretic problems. This dissertation investigates the applicability of these heuristics to next generation theorem provers. / Computing / M.Sc. (Computer Science)

Les techniques formelles de la famille « vérification de modèles » (« model checking ») se heurtent au problème de l’explosion combinatoire. Ceci limite les perspectives d’exploitation dans des projets industriels. Ce problème est provoqué par la combinatoire dans la construction de l’espace des états possibles durant l’exécution des systèmes modélisés. Le nombre d’états pour des modèles de systèmes industriels réalistes dépasse régulièrement les capacités des ressources disponibles en calcul et stockage. Cette thèse défend l’idée qu’il est possible de réduire cette combinatoire en spécialisant les outils pour des familles de propriétés. Elle propose puis valide expérimentalement un ensemble de méthodes pour le développement de ce type d’outils en suivant une approche guidée par les propriétés appliquée au contexte temps réel. Il s’agit donc de construire des outils d’analyse performants pour des propriétés temps réel qui soient exploitables pour des modèles industriels de taille réaliste. Les langages considérés sont, d’une part UML étendu par le profil MARTE pour la modélisation par les utilisateurs, et d’autre part les réseaux de Petri temporisés comme support pour la vérification. Les propositions sont validées sur un cas d’étude industriel réaliste issu du monde avionique : l’étude de la latence et la fraicheur des données dans un système de gestion des alarmes exploitant les technologies d’Avionique Modulaire Intégrée. Ces propositions ont été mise en oeuvre comme une boite à outils qui intègre les cinq contributions suivantes: la définition de la sémantique d’exécution spécifiques aux propriétés temps réel pour les modèles d’architecture et de comportement spécifiés en UML/MARTE; la spécification des exigences temps réel en s’appuyant sur un ensemble de patrons de vérification atomiques dédiés aux propriété temps réel; une méthode itérative d’analyse à base d’observateurs pour des réseaux de Petri temporisés; des techniques de réduction de l’espace d’états spécifiques aux propriétés temps réel pour des Réseaux de Petri temporisés; une approche pour l’analyse des erreurs détectées par « vérification des modèles » en s’appuyant sur des idées inspirées de la « fouille de données » (« data mining »). / Automatic formal verification such as model checking faces the combinatorial explosion issue. This limits its application in indus- trial projects. This issue is caused by the explosion of the number of states during system’s execution , as it may easily exceed the amount of available computing or storage resources. This thesis designs and experiments a set of methods for the development of scalable verification based on the property-driven approach. We propose efficient approaches based on model checking to verify real-time requirements expressed in large scale UML-MARTE real-time system designs. We rely on the UML and its profile MARTE as the end-user modeling language, and on the Time Petri Net (TPN) as the verification language. The main contribution of this thesis is the design and implementation of a property-driven verification prototype toolset dedicated to real-time properties verification for UML-MARTE real-time software designs. We validate this toolset using an avionic use case and its user requirements. The whole prototype toolset includes five contributions: definition of real-time property specific execution semantics for UML-MARTE architecture and behavior models; specification of real- time requirements relying on a set of verification dedicated atomic real- time property patterns; real-time property specific observer-based model checking approach in TPN; real-time property specific state space reduction approach for TPN; and fault localization approach in model checking.

Les programmes informatiques prennent une place de plus en plus importante dans nos vies. Certains de ces programmes, comme par exemple les systèmes de contrôle de centrales électriques, d'avions ou de systèmes médicaux sont critiques : une panne ou un dysfonctionnement pourraient causer la perte de vies humaines ou des dommages matériels ou environnementaux importants. Les méthodes formelles visent à offrir des moyens de concevoir et vérifier de tels systèmes afin de garantir qu'ils fonctionneront comme prévu. Au fil du temps, ces systèmes deviennent de plus en plus évolués et complexes, ce qui est source de nouveaux défis pour leur vérification. Il devient nécessaire de développer ces systèmes de manière modulaire afin de pouvoir distribuer la tâche d'implémentation à différentes équipes d'ingénieurs. De plus, il est important de pouvoir réutiliser des éléments certifiés et les adapter pour répondre à de nouveaux besoins. Aussi les méthodes formelles doivent évoluer afin de s'adapter à la conception et à la vérification de ces systèmes modulaires de taille toujours croissante. Nous travaillons sur une approche algébrique pour la conception de systèmes corrects par construction. Elle définit un formalisme pour exprimer des spécifications de haut niveau et permet de les raffiner de manière incrémentale en des spécifications plus concrètes tout en préservant leurs propriétés, jusqu'à ce qu'une implémentation soit atteinte. Elle définit également plusieurs opérations permettant de construire des systèmes complexes à partir de composants plus simples en fusionnant différents points de vue d'un même système ou en composant plusieurs sous-systèmes ensemble, ainsi que de décomposer une spécification complexe afin de réutiliser des composants existants et de simplifier la tâche d'implémentation. Le formalisme de spécification que nous utilisons est basé sur des spécifications modales. Intuitivement, une spécification modale est un automate doté de deux types de transitions permettant d'exprimer des comportements optionnels ou obligatoires. Raffiner une spécification modale revient à décider si les parties optionnelles devraient être supprimées ou rendues obligatoires. Cette thèse contient deux principales contributions théoriques basées sur une extension des spécifications modales appelée " spécifications à ensembles d'acceptation ". La première contribution est l'identification d'une sous-classe des spécifications à ensembles d'acceptation, appelée " spécifications à ensembles d'acceptation convexes ", qui permet de définir des opérations bien plus efficaces tout en gardant un haut niveau d'expressivité. La seconde contribution est la définition d'un nouveau formalisme, appelé " spécifications à ensembles d'acceptation marquées ", qui permet d'exprimer des propriétés d'atteignabilité. Ceci peut, par exemple, être utilisé pour s'assurer qu'un système termine ou exprimer une propriété de vivacité dans un système réactif. Les opérations usuelles sont définies sur ce nouveau formalisme et elles garantissent la préservation des propriétés d'atteignabilité. Cette thèse présente également des résultats d'ordre plus pratique. Tous les résultats théoriques sur les spécifications à ensembles d'acceptation convexes ont été prouvés en utilisant l'assistant de preuves Coq. L'outil MAccS a été développé pour implémenter les formalismes et opérations présentés dans cette thèse. Il permet de les tester aisément sur des exemples, ainsi que d'étudier leur efficacité sur des cas concrets. / Software programs are taking a more and more important place in our lives. Some of these programs, like the control systems of power plants, aircraft, or medical devices for instance, are critical: a failure or malfunction could cause loss of human lives, damages to equipments, or environmental harm. Formal methods aim at offering means to design and verify such systems in order to guarantee that they will work as expected. As time passes, these systems grow in scope and size, yielding new challenges. It becomes necessary to develop these systems in a modular fashion to be able to distribute the implementation task to engineering teams. Moreover, being able to reuse some trustworthy parts of the systems and extend them to answer new needs in functionalities is increasingly required. As a consequence, formal methods also have to evolve in order to accommodate both the design and the verification of these larger, modular systems and thus address their scalability challenge. We promote an algebraic approach for the design of correct-by-construction systems. It defines a formalism to express high-level specifications of systems and allows to incrementally refine these specifications into more concrete ones while preserving their properties, until an implementation is reached. It also defines several operations allowing to assemble complex systems from simpler components, by merging several viewpoints of a specific system or composing several subsystems together, as well as decomposing a complex specification in order to reuse existing components and ease the implementation task. The specification formalism we use is based on modal specifications. In essence, a modal specification is an automaton with two kinds of transitions allowing to express mandatory and optional behaviors. Refining a modal specification amounts to deciding whether some optional parts should be removed or made mandatory. This thesis contains two main theoretical contributions, based on an extension of modal specifications called acceptance specifications. The first contribution is the identification of a subclass of acceptance specifications, called convex acceptance specifications, which allows to define much more efficient operations while maintaining a high level of expressiveness. The second contribution is the definition of a new formalism, called marked acceptance specifications, that allows to express some reachability properties. This could be used for example to ensure that a system is terminating or to express a liveness property for a reactive system. Usual operations are defined on this new formalism and guarantee the preservation of the reachability properties as well as independent implementability. This thesis also describes some more practical results. All the theoretical results on convex acceptance specifications have been proved using the Coq proof assistant. The tool MAccS has been developed to implement the formalisms and operations presented in this thesis. It allows to test them easily on some examples, as well as run some experimentations and benchmarks.

O reúso de software enfrenta inúmeras barreiras gerenciais, técnicas e culturais na sua adoção, e a definição da estrutura de ativos reutilizáveis de software é uma dessas barreiras técnicas. Para solucionar isso, o Reusable Asset Specification (RAS) é um padrão de facto proposto pela OMG. Uma especificação como o RAS define e padroniza um modelo de ativos (assets) reutilizáveis, e é a base para a construção e para o uso de um repositório de ativos que apoia a reutilização de software. No entanto, para ser adotado na prática, o RAS necessita resolver suas lacunas através da sua extensão e da definição de informações complementares. Essas lacunas estão detalhadas neste trabalho. Solucionando estas lacunas, o RAS torna-se útil para auxiliar efetivamente na padronização do empacotamento dos ativos reutilizáveis e para guiar a estrutura do repositório de reutilização de software. Alguns trabalhos anteriores já responderam parcialmente essa questão, porém eles atendiam propósitos muito específicos, não possuíam uma ferramenta de apoio ou não haviam sido avaliados em contexto real de (re)uso. Esse trabalho propõe o Software Profile RAS (SW-RAS), uma extensão do Profile de componentes do RAS, que propõe soluções para diversas de suas lacunas, incluindo informações úteis e artefatos relevantes apontados na literatura, baseados em outros modelos de ativos reutilizáveis, em outras extensões do RAS e na experiência do processo de reúso no desenvolvimento de software. Particularmente, o SW-RAS estende as categorias de classificação, solução, uso e ativos relacionados, cujos detalhes estão descritos no texto. Visando à experimentação da proposta através de um estudo de caso, desenvolveu-se o Lavoi, um repositório de ativos reutilizáveis baseado no SW-RAS, que foi avaliado num ambiente real de reutilização e desenvolvimento de software de uma grande companhia pública de TI. Uma descrição deste processo de avaliação em um contexto real é também apresentada neste trabalho. A principal contribuição desta dissertação é a proposta, a avaliação e a consolidação de uma extensão do RAS que atende várias de suas lacunas e é suportada por uma ferramenta de software livre. / The software reuse faces numerous managerial, technical and cultural barriers in its adoption, and the definition of the structure of reusable software assets is one of these technical barriers. To solve this, the Reusable Asset Specification (RAS) is a de facto standard proposed by OMG. A specification such as the RAS defines and standardizes a reusable asset model, and it is the foundation for the construction and for the use of an asset repository that supports the software reuse. However, for being adopted in the practice, the RAS needs to solve its lacks through its extension and the definition of complementary information. These lacks are detailed in this work. Solving these lacks, the RAS becomes useful to help effectively in the standardization of packaging reusable assets and to guide the structure of the software reuse repository. Some previous works have already partially answered this question, but they attended very specific purposes, did not have a support tool or have not been evaluated in a real context of (re)use. This work proposes the Software Profile RAS (SW-RAS), an extension of the component Profile of RAS, which proposes solutions for its various lacks, including useful information and relevant artifacts pointed out in the literature, based on other reusable asset models, on other RAS extensions and on the experience in the reuse process at software development. Particularly, the SW-RAS extends the categories of classification, solution, usage and related assets, whose details are described in the text. Aiming at the experimentation of the proposal through a case study, the Lavoi was developed, a reusable asset repository based on the SW-RAS, which is was evaluated in a real environment of reuse and software development of a large public IT company. A description of this evaluation process in real context is also presented in this work. The main contribution of this dissertation is the proposal, the evaluation and the consolidation of an extension of RAS that addresses several of its lacks and is supported by a free software tool.

O presente trabalho tem por objetivo apresentar uma linguagem comum entre Usuários e Analistas para definição de requisitos, a ser utilizada durante as fases de Análise de Requisitos e Especificação, realizadas durante o desenvolvimento de Sistemas de Informação. A motivação para o trabalho surgiu da busca de uma solução para o problema de compatibilizar as diferenças entre as linguagens usadas por aqueles. Normalmente, são utilizados dois tipos de linguagens. O primeiro tipo tem, por principal característica, a informalidade, sendo as linguagens deste tipo, portanto, naturais mas pouco precisas. Já as linguagens do segundo tipo apresentam grande precisão, mas pouca legibilidade. Considerando que as linguagens informais são melhores para a participação dos Usuários no desenvolvimento de Sistemas de Informação e que as linguagens formais são úteis e necessárias para que Analistas elaborem a especificação do sistema e projetistas a interpretem, fez-se necessário o estudo de uma linguagem intermediária que busque um meio termo entre legibilidade (ou naturalidade) e precisão e que, ao mesmo tempo, seja próxima das linguagens informais e formais já em uso. São também apresentadas, neste trabalho, heurísticas (regras informais) para as transformações entre as linguagens, para justificar a referida proximidade, e um estudo de caso para avaliação dos graus de precisão e legibilidade da linguagem comum proposta. / The objecive of this work is to present a common language for users and analists, for requirements definition during Information Systems development. The motivation for this work arose from the study of the communication problem that users and analists have, working with diferent languages of at least two kinds (natural and formal). Natural languages have informality as their main characteristic, hence are not precise. On the other side, formal languages are precise, but sometimes not readable. Informal or natural languages are better for user participation in information system development, and formal languages are useful and necessary to analists when they create a system specification for implementors. It is necessary to search for an intermediate language, that could play a middle role between readableness and precision, and that, at the same time, is relatively close to informal and formal languages. In this work, heuristics (informal and common sense rules) for requirements ellicitation and for transformations between languages are defined too. A case study is detailed, for illustrate the degree of precision and readableness of the common language proposed here.

A exemplo de qualquer outra atividade que se destine a produzir um produto, a engenharia de software necessariamente passa por um fase inicial, onde necessário definir o que será produzido. A análise de requisitos é esta fase inicial, e o produto dela resultante é a especificação do sistema a ser construído. As duas atividades básicas durante a analise de requisitos são a eliciação (busca ou descoberta das características do sistema) e a modelagem. Uma especificação completa e consistente é condição indispensável para o adequado desenvolvimento de um sistema. Muitos tem sido, entretanto, os problemas enfrentados pelos analistas na execução desta tarefa. A variedade e complexidade dos requisitos, as limitações humanas e a dificuldade de comunicação entre usuários e analistas são as principais causas destas dificuldades. Ao considerarmos o ciclo de vida de um sistema de informação, verificamos que a atividade principal dos profissionais em computação é a transformação de uma determinada porção do ambiente do usuário, em um conjunto de modelos. Inicialmente, através de um modelo descritivo representamos a realidade. A partir dele derivamos um modelo das necessidades (especificação dos requisitos), transformando-o a seguir num modelo conceitual. Finalizando o ciclo de transformações, derivamos o modelo programado (software), que ira se constituir no sistema automatizado requerido. Apesar da reconhecida importância da analise dos requisitos e da conseqüente representação destes requisitos em modelos, muito pouco se havia inovado nesta área ate o final dos anos 80. Com a evolução do conceito de reutilização de software para reutilização de especificações ou reutilização de modelos de requisitos, finalmente surge não apenas um novo método, mas um novo paradigma: a reutilização sistemática (sempre que possível) de modelos integrantes de especificações de sistemas semelhantes ao que se pretende desenvolver. Muito se tem dito sobre esta nova forma de modelagem e um grande número de pesquisadores tem se dedicado a tornar mais simples e eficientes várias etapas do novo processo. Entretanto, para que a reutilização de modelos assuma seu papel como uma metodologia de use geral e de plena aceitação, resta comprovar se, de fato, ele produz software de melhor quantidade e confiabilidade, de forma mais produtiva. A pesquisa descrita neste trabalho tem por objetivo investigar um dos aspectos envolvido nesta comprovação. A experimentação viabilizou a comparação entre modelos de problemas construídos com reutilização, a partir dos modelos de problemas similares previamente construídos e postos a disposição dos analistas, e os modelos dos mesmos problemas elaborados sem nenhuma reutilização. A comparação entre os dois conjuntos de modelos permitiu concluir, nas condições propostas na pesquisa, serem os modelos construídos com reutilização mais completos e corretos do que os que foram construídos sem reutilização. A apropriação dos tempos gastos pelos analistas durante as diversas etapas da modelagem, permitiu considerações sobre o esforço necessário em cada um dos dois tipos de modelagem. 0 protocolo experimental e a estratégia definida para a pesquisa possibilitaram também que medidas pudessem ser realizadas com duas series de modelos, onde a principal diferença era o grau de similaridade entre os modelos do problema reutilizado e os modelos do problema alvo. A variação da qualidade e completude dos dois conjuntos de modelos, bem como do esforço necessário para produzi-los, evidenciou uma questão fundamental do processo: a reutilização só terá efeitos realmente produtivos se realizada apenas com aplicações integrantes de domínios específicos e bem definidos, compartilhando, em alto grau, dados e procedimentos. De acordo com as diretrizes da pesquisa, o processo de reutilização de modelos de requisitos foi investigado em duas metodologias de desenvolvimento: na metodologia estruturada a modelagem foi realizada com Diagramas de Fluxo de Dados (DFD's) e na metodologia orientada a objeto com Diagramas de Objetos. A pesquisa contou com a participação de 114 alunos/analistas, tendo sido construídos 175 conjuntos de modelos com diagramas de fluxo de dados e 23 modelos com diagramas de objeto. Sobre estas amostras foram realizadas as analises estatísticas pertinentes, buscando-se responder a um considerável número de questões existentes sobre o assunto. Os resultados finais mostram a existência de uma série de benefícios na análise de requisitos com modelagem baseada na reutilização de modelos análogos. Mas, a pesquisa em seu todo mostra, também, as restrições e cuidados necessários para que estes benefícios de fato ocorram. / System Engineering, as well as any other product oriented activity, starts by a clear definition of the product to be obtained. This initial activity is called Requirement Analysis and the resulting product consists of a system specification. The Requirement Analysis is divided in two separated phases: elicitation and modeling. An appropriate system development definition relies in a complete, and consistent system specification phase. However, many problems have been faced by system analysts in the performance of such task, as a result of requirements complexity, and diversity, human limitations, and communication gap between users and developers. If we think of a system life cycle, we'll find out that the main activity performed by software engineers consists in the generation of models corresponding to specific parts of the users environment. This modeling activity starts by a descriptive model of the portion of reality from which the requirement model is derived, resulting in the system conceptual model. The last phase of this evolving modeling activity is the software required for the system implementation. In spite of the importance of requirement analysis and modeling, very little research effort was put in these activities and none significant improvement in available methodologies were presented until the late 80s. Nevertheless, when the concepts applied in software reuse were also applied to system specification and requirements modeling, then a new paradigm was introduced, consisting in the specification of new systems based on systematic reuse of similar available system models. Research effort have been put in this new modeling technique in the aim of make it usable and reliable. However, only after this methodology is proved to produce better and reliable software in a more productive way, it would be world wide accepted by the scientific and technical community. The present work provides a critical analysis about the use of such requirement modeling technique. Experimental modeling techniques based on the reuse of similar existing models are analyzed. Systems models were developed by system analyst with similar skills, with and without reusing previously existing models. The resulting models were compared in terms of correction, consumed time in each modeling phase, effort, etc. An experimental protocol and a special strategy were defined in order to compare and to measure results obtained from the use of two different groups of models. The main difference between the two selected groups were the similarity level between the model available for reuse and the model to be developed. The diversity of resulting models in terms of quality and completeness, as well in the modeling effort, was a corroboration to the hypothesis that reuse effectiveness is related to similarity between domains, data and procedures of pre-existing models and applications being developed. In this work, the reuse of requirements models is investigated in two different methodologies: in the first one, the modeling process is based on the use of Data Flow Diagrams, as in the structured methodology; in the second methodology, based on Object Orientation, Object Diagrams are used for modeling purposes. The research was achieved with the cooperation of 114 students/analysts, resulting in 175 series of Data Flow Diagrams and 23 series of Object Diagrams. Proper statistical analysis were conducted with these samples, in order to clarify questions about requirements reuse. According to the final results, modeling techniques based on the reuse of analogous models provide an improvement in requirement analysis, without disregarding restrictions resulting from differences in domain, data and procedures.

Sistemas de Informação de Escritórios são tipos particulares de sistemas de informação. São sistemas sócio-técnicos, muito complexos, com grande influência humana. O tempo tem grande importância no tratamento das informações, tanto na representação de informações temporais explícitas como em restrições de ordem temporal e em características que são alteradas com a evolução da aplicação. Neste trabalho é apresentado um modelo de dados para ser utilizado como método de especificação de requisitos de sistemas de informação de escritórios. 0 desenvolvimento de especificações é uma tarefa bastante complexa, devendo possibilitar a representação de todas as características da aplicação, tanto as estáticas como as comportamentais. A especificação de uma aplicação geralmente é muito extensa, sendo dispendido um tempo considerável em sua elaboração. Um aspecto importante no desenvolvimento de especificações é a verificação da corretude destas, devido a complexidade que apresentam. Uma maneira de gerar especificações mais corretas e em menor espaço de tempo é através da reutilização de especificações anteriormente construídas e já validadas através de implementações. Neste trabalho optou-se por utilizar um modelo de dados orientado a objetos para especificar os sistemas de informação de escritórios. A utilização do paradigma de orientação a objetos na modelagem permite a definição de uma biblioteca de classes de objetos, classes estas identificadas em diversas especificações realizadas em um determinado domínio de aplicação. As classes constantes desta biblioteca podem ser reutilizadas de maneira bastante eficiente em especificações posteriores. A representação das características dinâmicas de uma aplicação, tais como a evolução dos objetos dentro do escritório, requer a possibilidade de representação de propriedades temporais. O modelo de dados utilizado na especificação deve permitir a representação de aspectos temporais tanto para definição de dados definidos em um domínio temporal como para representar a evolução dos valores assumidos pelos objetos durante sua existência. A possibilidade de representação dos aspectos temporais é um dos principais pontos desenvolvidos na elaboração do modelo de dados apresentado neste trabalho. O modelo apresentado denomina-se TF-ORM (Temporal Fuctionality in Objects with Roles Model), sendo uma extensão do modelo F-ORM (Functionality in Objects with Roles Model) [DEA 91a,b,c]. Foram incorporadas a este modelo os necessários aspectos temporais e foram ampliadas características básicas para captar melhor as particularidades do domínio de sistemas de informação de escritórios, principalmente no que à concerne representação de alguma parcela de trabalho humano. O modelo resultante, TF-ORM, um modelo de dados orientado a objetos, temporal, que utiliza o conceito de papéis para representar os diferentes comportamentos de um objeto. A possibilidade de recuperação de informações de um banco de dados que implemente o modelo de dados proposto foi também considerada. Neste trabalho é apresentada uma linguagem de recuperação de informações (linguagem de consulta) para o modelo de dados TF-ORM. Especial atenção é dada as consultas temporais. Como no modelo proposto são armazenados tanto o tempo de transação como o de validade, a linguagem de recuperação pode ser utilizada para recuperar informações referentes ao estado atual do banco de dados (informações atualmente válidas), a respeito de estados passados e futuros (informações válidas no passado e que serão válidas em estados futuros, de acordo com o atual conhecimento dos dados) e referentes a histórias passadas do banco de dados (informações que se acreditava como válidas em algum momento do passado). É apresentado em estudo de caso completo com o objetivo de validar o modelo de dados proposto e sua eficiência na especificação deste tipo de sistema de informação. O trabalho apresenta ainda a descrição de um ambiente de apoio a especificações que faz use de uma biblioteca de classes. Através deste ambiente, a especificação de uma aplicação é construída gradualmente, estando disponíveis opções de listagem das partes já definidas e de informações da biblioteca de classes para serem reutilizadas. As especificações geradas através deste ambiente apresentam pouca possibilidade de erro, uma vez que são efetuados vários procedimentos de verificação das informações fornecidas. / Office Information Systems constitute special kinds of information systems - very complex socio-technical systems, with large human influence. Time is very important in the information representation, not only for explicit temporal information but also for restrictions on temporal ordering of activities to be executed and to record the temporal evolution of property values. In this work a data model to be used as a requirement specification method for office infoimations systems is presented. Specification development is a complex task. All the possible characteristics of an application, static and behavioral, shall be represented. An applications' specification is usually not a trivial task, and a big amount of time is used to develop it. Specifications are usually very complex and the possibility of verifying the correctness is an important aspect to be considered. The reuse of specifications is a way to obtain a better rate of correctness spending less time, using parts of specifications that were already validated through previous implementations. An object-oriented data model is used in this work to specify office information systems. The use of the object-oriented paradigm allows the definition of a class library containing classes identified in several specifications constructed in a specific application domain. The reuse of classes of such a library in new specifications gives efficiency to the process. To represent the dynamic characteristics of an application, such as the documents evolution within the office, it is necessary to be able to represent temporal properties. The data model used in the specification shall allow the representation of these temporal aspects not only to model data defined in a temporal domain but also to represent the objects values evolution during an objects existence. The representaion of temporal aspects is one of the main issues developed in the data model defined in this work. The data model is called TF-ORM (Temporal Fuctionality in Objects with Roles Model), and is an extention to the F-ORM (Functionality in Objects with Roles Model) model [DEA 91 a,b,c]. To this model the necessary temporal aspects were added and the basic characteristics were enlarged to better capture the particular aspects of the office habilitation systems domain, specially concerning the representation of some parts of human work. The resulting model. TF-ORM, is an object-oriented temporal data model and uses the concept of roles to represent an objects different behaviors. The possibility of retrieving information from a database specified through this data model is also considered and a query language for the TF-ORM data model is presented. Special attention is given to the retrieval of temporal information. The TFORM data model stores both the transaction and the valid time associated to dynamic properties and allows the retrieving of information fettering the databases' actual state (actually valid information), information refering the databases' past and future states (valid information in the past and information that will be valid in the future according to the actual data knowledge) and information about the databases' past history (information that was believed to be true in some moment in the past). A complete case study is presented to validate the TF-ORM data model and its efficiency as a specification method for office information systems. An environment to support specifications using TF-ORM is described. This environment uses a class library. The use of this environment allows stepwise construction of a specification, with the access to listings of the already defined parts and to the information of the class library to be reused. The contructed specifications present a small rate of errors, due to several verification procedures embedded in the environment.

Prosoft é um grupo de pesquisa do Instituto de Informática da UFRGS, desenvolvido pelo grupo de pesquisa homônimo e coordenado pelo Professor Daltro José Nunes. O objetivo do projeto é desenvolver um ambiente de desenvolvimento de software completo, o Ambiente Prosoft, que é baseado nos conceitos de Modelos, Cálculo Lambda, Tipos Abstratos de Dados e Orientação a Objetos. Um dos componentes do Ambiente Prosoft é sua linguagem de especificação algébrica: o Prosoft Algébrico. Apesar de ser base e tema de diversos trabalhos no grupo de pesquisa Prosoft, o Prosoft Algébrico não tem sua semântica devidamente definida. Os trabalhos desenvolvidos até agora foram baseados em noções operacionais, e apresentam diferentes interpretações do Prosoft Algébrico. Esta dissertação apresenta uma especificação de semântica denotacional para o Prosoft Algébrico, compreendendo, entre outras características, sua primitiva de comunicação entre tipos de dados, chamada ICS, e sua notação gráfica para representação de instanciação de tipos abstratos de dados. Essa dissertação apresenta também um estudo sobre prototipação semântica usando a linguagem de programação Haskell. O conceito de Literate Programming e a proximidade entre Cálculo Lambda e Haskell foram cruciais no rápido desenvolvimento de uma implementação protótipo do Prosoft Algébrico, baseada na sua semântica especificada. As principais contribuições dessa dissertação incluem: uma interpretação precisa e sem ambiguidades do Prosoft Algébrico, através da especificação da sua semântica; a definição de semântica para a ICS, um conceito único (até o limite do nosso conhecimento) que fornece um mecanismo de passagem de mensagens entre tipos de dados algébricos; uma implementação protótipo do Prosoft Algébrico, que pode realmente ser utilizada para experimentar e testar a definição da linguagem e a especificação da semântica do Prosoft Algébrico; resultados sobre prototipação semântica de especificações tanto de semântica denotacional quanto de semântica operacional usando a linguagem de programação Haskell para desenvolvimento rápido de protótipos de linguagens baseados na sua semântica. Como grande parte do desenvolvimento do Ambiente Prosoft é realizado através de projetos de cooperação internacional e essa dissertação irá influenciar fortemente o seu desenvolvimento futuro, o texto foi escrito em inglês para facilitar a troca de informação entre o grupo Prosoft e seus parceiros estrangeiros. / Prosoft is a research project at Instituto de Informática da UFRGS, developed by the research group with the same name and coordinated by Professor Daltro José Nunes. The project’s goal is to develop a full software development environment, the Prosoft Environment, based on the concepts of Models, Lambda Calculus, Abstract Data Types and Object orientation. One of the components of the Prosoft Environment is its algebraic specification language: Algebraic Prosoft. Although being the basis and theme of several works in the Prosoft research group, Algebraic Prosoft doesn’t have its semantics properly defined. Works done up to now were based on operational notions and presented different interpretations of Algebraic Prosoft. This thesis presents a denotational semantics specification for Algebraic Prosoft, comprising, among other features, its “inter-data type” communication primitive, called ICS, and its graphical notation for representing instantiations of abstract data types. This thesis also presents a study of semantic prototyping using the Haskell programming language. The concept of Literate Programing and the proximity between lambda calculus and Haskell were crucial to the rapid development of a prototype implementation of Algebraic Prosoft, based on its specified semantics. This thesis’ main contributions include: a precise and unambiguous interpretation of Algebraic Prosoft, through a semantics specification; the definition of semantics to the ICS, a unique (to the best of our knowledge) concept that provides a messagepassing mechanism between algebraic data types; a prototype implementation of Algebraic Prosoft, which can actually be used to experiment and test the Algebraic Prosoft language definition and semantics specification; results regarding semantics prototyping of both denotational and operational semantics specifications using the Haskell programming language for rapid development of semantics-based prototypes of languages. Since a large portion of Prosoft Environment’s development is done through international cooperation projects and this thesis will strongly influence its future development, the text was written in English in order to facilitate the information exchange between the Prosoft research group and its foreign partners.

[pt] Um estudo sistemático da metodologia de determinação da probabilidade do DGD ultrapassar um determinado valor máximo foi apresentado. A metodologia foi discutida sob o ponto de vista teórico, obtendo-se o resultado a partir de uma base de dados recebidos de fabricantes de cabos de fibra óptica. Efetuou-se a comparação com os dados coletados destes mesmos cabos, porém já implantados em backbone. O resultado deste comparativo sistemático, foi apresentado sob a forma de estatística do valor de DGD ultrapassar o valor máximo estabelecido na norma ITU-T, para sistemas de 10 e 40Gbps. A partir dos resultados obtidos foi importante a identificação de erros que remontam a origem do processo de fabricação de cabos de fibras ópticas, a restrição na sensibilidade dos equipamentos de medição o que leva a uma superestimação da probabilidade do DGD ultrapassar um certo valor máximo e o próprio conceito do guia TIA/EIA TSB107, que define o método para a obtenção destes resultados. A criticidade destes resultados pode levar a um erro na escolha de um sistema óptico de transmissão podendo gerar prejuízos muito significativos, sejam financeiro ou temporal. Foram propostas três recomendações para direcionar a metodologia a uma previsão mais confiável dos resultados obtidos a partir do método 2 TIA/EIA TSB107, gerando mais conforto para o projeto de sistemas de alta capacidade. / [en] A systematic study of the methodology that determines the probability of the DGD overcomes a settled maximum value was presented. The methodology was discussed in a theoretical way; the values were based on a database received from optical fibers manufacturers/cablers. A comparison was conducted taking in consideration these same cables already installed in two backbones. The result of this systematic comparison was presented, as a statistic of the DGD value exceeds certain maximum value established by the standard ITU-T for systems from 10 to 40Gbps. Based on these results, the identification of mistakes that ascends the beginning of manufacture process of the optical fiber cables was important. The restriction of the sensibility of measurement devices leads to a overestimation of the probability of the DGD exceeds a given maximum value and the concept of the guideline TIA/EIA TSB107, that defines the methodology of acquisition of these results. These critical results could lead to a mistake choosing the optical system transmission and cause loss profit as well as time delay in a project. There were proposed three recommendations in order to guide the methodology for a trustful preview of the obtained results from TIA/EIA method 2, offering more comfort for optical high capacity system design.

Made available in DSpace on 2014-12-17T15:28:51Z (GMT). No. of bitstreams: 1 BrunaSL_DISSERT.pdf: 1891001 bytes, checksum: 1d482b920c53ec1f846060dbc2158ebb (MD5) Previous issue date: 2012-08-10 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / The cerebral cortex of mammals is histologically organized into different layers of excitatory neurons that have distinct patterns of connections with cortical or subcortical targets. During development, these cortical layers are established through an intricate combination of neuronal specification and migration in a radial pattern known as "insideout": deep-layer neurons are generated prior to upper-layer neurons. In the last few decades, several genes encoding transcription factors involved in the sequential specification of neurons destined to different cortical layers have been identified. However, the influence of early-generated neurons in the specification of subsequent neuronal cohorts remains unclear. To investigate this possible influence, we induced the selective death of cortical neurons from layer V and VI before the generation of layer II, III and IV neurons. Thus, we can evaluate the effects of ablation of early born neurons on the phenotype of late born neurons. Our data shows that one-day after ablation, layer VI neurons expressing the transcription factor TBR1 are newly generated while virtually no neuron expressing TBR1 was generated in the same age in control animals. This suggests that progenitors involved in the generation of neurons destined for superficial layers suffer interference from the selective death of neurons in deep layers, changing their specification. We also observed that while TBR1-positive neurons are located exclusively in deep cortical layers of control animals, many TBR1-positive neurons are misplaced in superficial layers of ablated animals, suggesting that the migration of cortical neurons could be controlled independently of neuronal phenotypes. Furthermore, we observed an increase in layer V neurons expressing CTIP2 and neurons expressing SATB2 and that these cells have changed their distributions. As a conclusion, our data indicate the existence of a mechanism of control exercised by the early-generated neurons in the cerebral cortex on the fate of the progenitors involved in the generation of the following cortical neurons. This mechanism could help to control the number of neurons in different layers and contribute to the establishment of different cortical areas / O c?rtex cerebral de mam?feros encontra-se histologicamente organizado em camadas de neur?nios excitat?rios que, por sua vez, apresentam distintos padr?es de conectividade com alvos corticais ou sub-corticais. Durante o desenvolvimento, estas camadas corticais s?o estabelecidas atrav?s de uma intrincada combina??o entre especifica??o neuronal e migra??o radial num padr?o conhecido como "inside-out" (de dentro para fora). Desta forma, por exemplo, neur?nios infragranulares nas camadas V e VI s?o gerados anteriormente aos neur?nios granulares da camada IV, que por sua vez s?o gerados antes dos supra-granulares das camadas II e III. Na ?ltima d?cada, foram identificados diversos genes codificando fatores de transcri??o envolvidos na especifica??o sequencial de neur?nios destinados ?s diferentes camadas corticais. No entanto, ainda pouco ? sabido sobre a influ?ncia dos neur?nios gerados previamente sobre a especifica??o das coortes neuronais subsequentes. Para investigar esta poss?vel influ?ncia, n?s utilizamos um m?todo de recombina??o g?nica (sistema Cre- Lox) para induzir a morte seletiva de neur?nios das camadas corticais V e VI antes da gera??o dos neur?nios das camadas II, III e IV. Dessa forma, pudemos avaliar os efeitos da abla??o de neur?nios infragranulares sobre o fen?tipo dos neur?nios gerados em seguida. Nossos dados mostraram que, um dia ap?s a abla??o, neur?nios da camada VI expressando o fator de transcri??o TBR1 voltaram a ser gerados enquanto praticamente nenhum neur?nio expressando TBR1 foi gerado na mesma idade em animais controle. Esse dado sugere que os progenitores envolvidos na gera??o de neur?nios destinados ?s camadas superficiais sofrem interfer?ncia da morte seletiva de neur?nios de camadas profundas, mudando sua especifica??o. Uma parte dos neur?nios TBR1 se estabeleceu na camada VI e outra migrou at? as camadas II e III, indicando que o controle dos padr?es migrat?rios pode ser independente dos fen?tipos neuronais. Al?m disso, observamos que na popula??o neuronal total tamb?m ocorreu um aumento na quantidade de neur?nios de camada V expressando CTIP2 e uma altera??o na distribui??o dessas c?lulas. O mesmo foi observado para neur?nios supragranulares expressando SATB2. Em conjunto, nossos dados indicam a exist?ncia de um mecanismo de controle exercido pelos neur?nios gerados inicialmente no c?rtex cerebral sobre o destino dos progenitores envolvidos na gera??o dos demais neur?nios corticais. Tal mecanismo poderia contribuir para o controle do n?mero de neur?nios em diferentes camadas e contribuir para o estabelecimento de diferentes ?reas corticais