Formalios specifikacijos – tai matematinis programinės ar techninės įrangos aprašymas, kurį galima naudoti sistemos realizacijai. Formalių specifikacijų naudojimas dar negarantuoja specifikacijos teisingumo. Tam naudojami formalaus verifikavimo metodai. Šiame dokumente aptariami formalių specifikacijų validavimo metodai. Du populiaraiausi formalių specifikacijų validavimo metodai yra pasiekiamų būsenų grafo analizė bei invarianto tikrinimas. Pasiekiamų būsenų grafo analizę sudaro pasiekiamų būsenų grafo generavimas ir analizė. Grafo analizės metu ieškoma aklaviečių, uždarų ciklų, nepasiekiamų būsenų, atliekamas būsenų koordinačių apribojimų tikrinimas bei invarianto tikrinimas. Tradiciniai pasiekiamų būsenų grafo sudarymo algoritmai grafo sudarymui naudoja sistemos būsenų eilę. Kiekviena išanalizuota būsena įrašoma į pasiekiamų būsenų grafą. Dokumente aptariamas lygiagretaus programavimo naudojimas būsenų grafo generavimui, kuris analizuoja ir generuoja sistemos būsenas naudodamas lygiagrečias gijas. Eksperimentų su vienkanale aptarnavimo sistema metu nustatyta, kad lygiagretaus algoritmo naudojimas šio uždavinio metu leidžia pagerinti sistemos veikimą iki 35%, priklausomai nuo būsenų skaičiaus. / Arguably the most important task in creation of software is user requirement specification. Accurate requirement specification allows avoidance of errors in late stages of software development. This is extremely important in critical systems, where even vague error can cause great financial losses or even human victims. One of the methods used for precise user requirement specification is use of formal specifications. Formal specification is a mathematical method for describing of software or hardware, which might be suitable for system realization. Nevertheless, the construction of formal specifications does not guarantee the correctness of specification. For this reason formal specification validation is necessary. In this paper methods of formal specification validation are discussed. Two most popular methods of formal specification validation are reachable state graph analysis and invariant checking. Reachable state graph analysis consists of graph generation and graph analysis. Graphs can be analyzed for dead-ends, closed loops, state reach ability checking, coordinate restriction checking or invariant checking. Traditional reachable graph generation algorithm uses unanalyzed states queue to produce reachable state graph. Each step single state is analyzed and depending on results new vertex or edge is added to state graph. An improvement to the algorithm to consider is usage of parallel programming to process multiple states simultaneously. This allows increasing the... [to full text]

In this thesis, we study two fundamental problems that arise in the modeling of stochastic systems: (i) Validation of stochastic models against behavioral specifications such as temporal logics, and (ii) Discovery of kinetic parameters of stochastic biochemical models from behavioral specifications. We present a new Bayesian algorithm for Statistical Model Checking of stochastic systems based on a sequential version of Jeffreys’ Bayes Factor test. We argue that the Bayesian approach is more suited for application do- mains like systems biology modeling, where distributions on nuisance parameters and priors may be known. We prove that our Bayesian Statistical Model Checking algorithm terminates for a large subclass of prior probabilities. We also characterize the Type I/II errors associated with our algorithm. We experimentally demonstrate that this algorithm is suitable for the analysis of complex biochemical models like those written in the BioNetGen language. We then argue that i.i.d. sampling based Statistical Model Checking algorithms are not an effective way to study rare behaviors of stochastic models and present another Bayesian Statistical Model Checking algorithm that can incorporate non-i.i.d. sampling strategies. We also present algorithms for synthesis of chemical kinetic parameters of stochastic biochemical models from high level behavioral specifications. We consider the setting where a modeler knows facts that must hold on the stochastic model but is not confident about some of the kinetic parameters in her model. We suggest algorithms for discovering these kinetic parameters from facts stated in appropriate formal probabilistic specification languages. Our algorithms are based on our theoretical results characterizing the probability of a specification being true on a stochastic biochemical model. We have applied this algorithm to discover kinetic parameters for biochemical models with as many as six unknown parameters.

The use of objective tests in Technology Enhanced Learning (TEL) is based on the application of computers to support automatic assessment. Current research in this domain is mainly focused on the design of new question-items, being IMS Question and Test Interoperability (QTI) the recognized de-facto standard. This thesis claims that the domain can be extended with the design of advanced test-scenarios that integrate new interactive contexts for the visualization of question-items and tests, and that consider different types of devices and technologies that enable diverse activity settings. In this context, the dissertation proposes to term the domain as Computing-Based Testing (CBT) instead of Computer- Based Testing because it captures better the new technological support possibilities for testing. Advanced CBT scenarios can increase teachers’ choices in the design of more appropriate tests for their subject areas, enabling the assessment of higher-order skills. With the aim of modelling an advanced CBT domain that extends the current possibilities of QTI and related work, this thesis provides a set of contributions around three objectives. The first objective deals with proposing a Conceptual Model for the CBT domain considering three main dimensions: the Question-item, the Test and the Activity. To tackle this objective, the thesis presents, on the one hand, a framework to assist in the categorization and design of advanced CBT scenarios and, on the other hand, two models that suggest elements for technologically representing the Test and Question-item dimensions. The models are platform-independent models (PIM) that extend QTI in order to support advanced CBT. Besides, the use of patterns is proposed to complement the modelling of the domain. The second objective seeks to show the relevance, value and applicability of the CBT Conceptual Model through exemplary challenging scenarios and case studies in authentic settings. To this end, the dissertation evaluates the design and implementation of a set of CBT systems and experiments. All the experiments use the proposed CBT Conceptual Model for designing an advanced CBT scenario. For each case the CBT-PIMs serve as the basis for developing a particular CBT-PSM and system. The evaluation results show that the implementations foster educational benefits, enable the assessment of higher-order skills and enhance the students’ motivation. Finally, the third objective is devoted to propose extension paths for QTI. The collection of models proposed in the thesis suggests different extension directions for QTI so as to enable the implementation of advanced questions, tests and activities. The proposed systems and scenarios also represent reference implementation and good practices of the proposed extension paths. / El uso de test de corrección automática, en el Aprendizaje Apoyado por Tecnologías de la Información y las Comunicaciones, se basa en el uso de ordenadores. Las propuestas actuales se centran en el diseño de nuevas preguntas, siendo IMS Question and Test Interoperability (QTI) el estándar de-facto. La tesis propone que este dominio puede ser extendido con el diseño de escenarios de test avanzados que integren nuevos contextos de interacción para la visualización de preguntas y tests, y que consideren la aplicación de diversos dispositivos tecnológicos para permitir diversos tipos de actividades. En este contexto se propone usar el término inglés Computing-Based Testing (CBT) para referirse al dominio, en vez de usar el término Computer-Based Testing, enfatizando el papel de la tecnología para la evaluación basada en test. Los escenarios CBT avanzados pueden aumentar la posibilidad de que los profesores puedan diseñar test más adecuados para sus asignaturas, permitiendo la evaluación de habilidades de alto nivel. Con el reto principal de modelar el dominio del CBT extendiendo las posibilidades actuales de QTI y las aproximaciones actuales, esta tesis proporciona un conjunto de contribuciones relacionadas con tres objetivos. El primer objetivo de la tesis es proponer un Modelo Conceptual definiendo y relacionando tres dimensiones: Pregunta, Test y Actividad. Por una parte, se propone un marco como guía en la categorización y diseño de escenarios CBT. Además, se proponen dos modelos que indican los elementos para la representación tecnológica de preguntas y test. Estos modelos son independientes de plataforma (PIM) que extienden QTI formulando los elementos que permiten implementar escenarios CBT avanzados. Además, se propone el uso de patrones como complemento en el modelado del dominio. El segundo objetivo trata de mostrar la relevancia y aplicabilidad de las contribuciones a través de escenarios y casos de estudio representativos en contextos reales. Para ello, se evalúa el diseño e implementación de un conjunto de experimentos y sistemas. En todos los experimentos se utiliza el Modelo Conceptual para diseñar escenarios CBT avanzados. Para cada caso los CBT-PIMs sirven como base para desarrollar modelos específicos de plataforma (CBT-PSMs) y sistemas asociados. La evaluación muestra que las implementaciones resultantes tienen beneficios educativos positivos, permitiendo la evaluación de habilidades de alto nivel y mejorando la motivación de los estudiantes. Finalmente, el tercer objetivo se centra en proponer vías de extensión para QTI. La colección de modelos propuestos sugiere diferentes direcciones de extensión de QTI para la implementación de preguntas, tests y actividades avanzados. Los escenarios y sistemas llevados a cabo representan implementaciones de referencia y buenas prácticas para las vías de extensión propuestas.

Os sistemas de tratamento de esgotos por zona de raízes constituem-se de um leito filtrante plantado com macrófitas emergentes. Tecnologia de baixo custo e, com eficiência comprovada em inúmeros trabalhos, as Estações de Tratamento de Efluentes (ETEs) por zona de raízes apresentam grande potencial para solucionar o problema da inexistência de coleta e tratamento de esgoto em pequenas comunidades. Este trabalho teve por objetivo caracterizar uma ETE por zona de raízes de fluxo vertical com base em variáveis abióticas e microbiológicas. Através da técnica de contagem em placas e da técnica de tubos múltiplos, foi possível estimar a densidade de fungos totais, bactérias heterotróficas, coliformes totais, Escherichia coli, bactérias redutoras de nitrato, bactérias desnitrificantes e bactérias redutoras de sulfato presentes nos diferentes estratos do sistema. Além das análises microbiológicas, foram avaliadas as variáveis abióticas temperatura, pH, oxigênio dissolvido (OD), nitrogênio amoniacal, nitrito, nitrato, nitrogênio total, ortofosfato e Demanda Química de Oxigênio (DQO). As análises foram realizadas em 8 locais, sendo uma referente ao efluente bruto, uma ao efluente tratado, três correspondendo à interface zona de raízes-brita e três ao filtro de areia, num total de 7 amostragens durante um ciclo sazonal. Em 5 amostragens não foi possível observar a redução do NMP de E. coli, apenas na Amostragem 1(C1) e na Amostragem 7 (C7) foi possível observar aproximadamente 66% e 97% de redução, respectivamente. As bactérias desnitrificantes, na maioria dos pontos e as redutoras de sulfato, com exceção da Amostragem 3 (C3), foram determinadas no valor de 1600 NMP.100mL-1. A densidade de bactérias redutoras de nitrato variou, na maioria das amostragens, de 1,8 NMP. 100mL-1 a 19 NMP. 100mL-1. A ETE foi eficiente para a remoção de DQO e fósforo, este último com porcentagem de remoção variando de, aproximadamente, 37% a 69%. A concentração de N-amoniacal foi reduzida em todas as amostragens, com exceção da C3. O pH permaneceu próximo da neutralidade e a concentração de oxigênio dissolvido aumentou na região do filtro de areia. Ao longo do período deste estudo foi observado um baixo desenvolvimento das plantas utilizadas. Com os resultados de quantificação foi possível verificar que a biodegradação é mais intensa nos primeiros 50 cm da ETE. Observou-se redução significativa da densidade de microrganismos no filtro de areia em relação à zona de raízes. Fatores como a idade da estação, que permitiu a formação de um biofilme no filtro de brita, a presença do filtro de areia e a disponibilidade de matéria orgânica podem estar envolvidas com a redução de microrganismos. Em resumo, pode se concluir que a ETE foi eficiente para remoção de microrganismos, porém apenas nos períodos de menor precipitação pluviométrica. / Wastewater root zone treatment systems are constituted of a filter bed planted with emergent macrophytes. A low cost technology with treatment potential proven in numerous studies, the root zone Wastewater Treatment Station (WTS) have great potential to solve the problem of lack of wastewater collection and treatment in small communities. This study aimed to characterize a root zone WTS with vertical flow on the basis of abiotic and microbiological variables. Through the technique of plate count and the multiple tube method was possible to estimate the density of total fungi, heterotrophic bacteria, total coliforms, Escherichia coli, nitrate-reducing bacteria, denitrifying bacteria and sulfate-reducing bacteria in the different strata of the system. In addition to the microbiological analysis the abiotic variables temperature, pH, dissolved oxygen, ammonia nitrogen, nitrite, nitrate, total nitrogen, orthophosphate, Chemical Oxygen Demand (COD) were evaluated. Analyses were performed in eight locations, one related to raw wastewater, one of treated effluent, three corresponding to the root zone interface and three to the sand filter, in a total of seven samples during a seasonal cycle. In 5 samples did not exhibit a reduction in the MPN of E. coli, only in Sample 1 (C1) and Sample 7 (C7) was observed approximately 66% and 97% reduction, respectively. Denitrifying bacteria in most spots and sulfate reducers, with the exception of the Sample 3 (C3) were determined in the amount of 1600 MPN.100mL-1. The density of nitrate-reducing bacteria ranged in most samples, from 1.8 MPN.100mL-1 to 19 MPN.100mL-1. The WTS was efficient for the removal of COD and phosphorus, the latter with removal percentage ranged from approximately 37% to 69 %. The concentration of ammonia-N was reduced in all samples, except for C3. The pH remained near neutrality and the concentration of dissolved oxygen increased in the region of the sand filter. Throughout the study period was observed a less growing of the plants. With the results of quantification it was possible verify that biodegradation is more intense in the first 50 cm of the WTS. It was observed significant reduction in the density of microorganisms in the sand filter compared with the root zone. Factors such as age of the station, which allowed the formation of a biofilm in the filter of gravel, the presence of sand filter and the availability of organic matter may be involved in the reduction of microorganisms. In summary it can be concluded that the WTS was efficient for removal of microorganisms, but only during periods of low rainfall.

Submitted by Aelson Maciera (aelsoncm@terra.com.br) on 2017-08-25T18:53:26Z No. of bitstreams: 1 DissGP.pdf: 3104844 bytes, checksum: 2e20a531a8e46327359fb4eacc9adf50 (MD5) / Approved for entry into archive by Ronildo Prado (bco.producao.intelectual@gmail.com) on 2018-01-24T12:17:05Z (GMT) No. of bitstreams: 1 DissGP.pdf: 3104844 bytes, checksum: 2e20a531a8e46327359fb4eacc9adf50 (MD5) / Approved for entry into archive by Ronildo Prado (bco.producao.intelectual@gmail.com) on 2018-01-24T12:18:07Z (GMT) No. of bitstreams: 1 DissGP.pdf: 3104844 bytes, checksum: 2e20a531a8e46327359fb4eacc9adf50 (MD5) / Made available in DSpace on 2018-01-24T12:21:46Z (GMT). No. of bitstreams: 1 DissGP.pdf: 3104844 bytes, checksum: 2e20a531a8e46327359fb4eacc9adf50 (MD5) Previous issue date: 2017-05-05 / Não recebi financiamento / The purpose of this work is to propose a method that allow to bring the fundamentals of mathematical logic to high school through the use of set theory, however making the whole approach of the subject through diagrams, making it possible to avoid, for the demonstrations and understanding necessary to the development of the subject, the rigors of writing used in mathematical logic, which, in a first contact, tend to discourage the interest of beginning students. / O objetivo deste trabalho é propor um método que permita levar os fundamentos da lógica matemática para o ensino médio por meio da utilização da teoria dos conjuntos, porém fazendo todo a aproximação do assunto utilizando diagramas, tornando possível evitar assim, para as demonstrações e o entendimento necessários ao desenvolvimento do assunto, os rigores da escrita utilizada na lógica matemática, que, em um primeiro contato, podem desestimular o interesse dos alunos iniciantes

Esta pesquisa apresenta uma proposta de bula para software, a qual possibilita capturar informações relacionadas aos requisitos funcionais e não funcionais de um determinado software, seguindo uma estrutura pré-definida. O referencial bibliográfico que embasa o trabalho é composto das teorias inerentes à transparência, transparência de software e mapas mentais. Discute a transparência dada às informações e processos das iniciativas públicas e privadas. Fornece subsídios para a concepção básica dos mapas mentais, proposto por Tony Buzan, com o intuito de justificar sua aderência em meio à proposta do trabalho. A proposta une a ideia de bulas de medicamentos, normatizada pela Agência Nacional de Vigilância Sanitária – ANVISA, aos conceitos de mapas mentais. Complementado por uma pesquisa experimental, este trabalho verificou a eficiência da bula de software na transmissão de conhecimentos por meio de um experimento que envolveu 326 participantes. Traz como resultado um modelo de bula para software que poderá ser utilizado pela indústria com o objetivo de elevar uma das características de transparência: a entendibilidade. / This research proposes a package insert for software that makes it possible to gather information related to the functional and non-functional requirements of a particular software, following a pre-defined structure. The bibliographic references that supports the work consists of theories relating to transparency, software transparency and mind maps. Discusses the transparency given to the information and processes of public and private initiatives. Provides subsidies for basic conception of mental maps, proposed by Tony Buzan, in order to justify its use in the work. The proposal combines the idea of pharmaceutical inserts, regulated by the National Health Surveillance Agency – ANVISA, to the concepts of mind maps. Complemented by experimental research, this study found the software package insert for efficiency in the transmission of knowledge through an experiment involving 326 participants. It brings up as result a model of package insert for software that may be used by the industry in order to increase one of the transparency’s characteristics: the understandability.

[pt] As operações de EeP na Bacia de Santos sempre ficaram em segundo plano quando comparadas com a Bacia de Campos, berço das gigantescas descobertas petrolíferas dos últimos 40 anos. Porém, com a descoberta do pré-sal, mais presente na Bacia de Santos, essa hegemonia da Bacia de Campos está aos poucos diminuindo, tendo a produção do pré-sal ultrapassado pela primeira vez a do póssal em junho de 2017. Com isso, torna-se imprescindível o aprimoramento da operação para atender a essa nova demanda. Junto com essa nova descoberta, a grave crise que a indústria do petróleo tem vivido desde 2014 com a alta queda no preço do barril, mais intensificada ainda no Brasil devido ao aumento do dólar, trouxe um novo foco para a diminuição do custo de extração, incluindo aí a diminuição de custos logísticos. Na Petrobras, a grande parte da produção de petróleo vem de água profundas e as unidades marítimas necessitam de suprimentos em volume considerável e tempo hábil para realizar suas operações. O elo final da cadeia logística para atendimento às unidades marítimas são as embarcações e elas representam cerca de 70 por cento dos custos logísticos. Nesse estudo, as diferentes metodologias de atendimento marítimo para transporte de cargas utilizadas nos últimos anos, tanto na Bacia de Campos quanto na de Santos, foram analisadas empiricamente e foram encontrados alguns pontos passíveis de melhoria. Uma possibilidade de redução de frota foi identificada e uma metodologia para realizar essa redução foi proposta. A metodologia se baseia em uma nova forma de formação de clusters, reduzindo o tempo total de navegação das embarcações, e um novo ordenamento portuário, de tal forma que uma mesma embarcação possa realizar mais serviços durante a semana, gerando assim menor necessidade de frota. A nova metodologia completa foi implantada em janeiro de 2018, gerando inicialmente uma diminuição de 20 por cento da frota de transporte de carga na Bacia de Santos. / [en] EeP operations in the Santos Basin have always been left in second plan when compared to the Campos Basin, the cradle of the gigantic oil discoveries of the last 40 years. However, with the discovery of the pre-salt, more present in the Santos Basin, this hegemony of the Campos Basin is gradually diminishing, with the production of the pre-salt having surpassed for the first time the one of the postsalt in June of 2017. With this, it is essential to improve the operation to meet this new demand. Along with this new discovery, the severe crisis that the oil industry has experienced since 2014 with the sharp fall in the price of the barrel, more intensified in Brazil due to the increase of the dollar, brought a new focus in reducing the cost of extraction, including the reduction of logistics costs. At Petrobras, most of the oil production comes from deep water and the maritime units need supplies in considerable volume and on time to carry out their operations. The final link of the logistics chain to serve this maritime units are vessels and they represent about 70 percent of logistics costs. In this study, the different maritime service policies for deck cargo transport used in recent years, both in the Campos Basin and Santos Basin, were analyzed empirically and some improvement points were found. The feasibility of reducing the fleet was identified and a methodology to accomplish this reduction was proposed. The methodology is based on a new form of clusters formation, reducing the total vessels navigation time, and a new berth scheduling, in such a way that the same vessel can perform more services during the week, thus generating less need of fleet. The complete new methodology was implemented in January 2018, initially generating a 20 percent decrease in the cargo transport fleet in the Santos Basin.

Esta tese de doutorado apresenta um modelo de especificação, textual e grafico, para sistemas transacionais em banco de dados (ER/T+) e, também, um modelo de implementação desta especificação. Sugere uma técnica de proceduralização de especificações declarativas, usando um grafo de dependencia de fluxos de dados para estabelecer a relação de precedecia entre os fluxos do diagrama da linguagem gráfica de especificação. Apresenta, também, os mecanismos de execução da linguagem de especificação proposta e as regras de mapeamento da linguagem de especificação, em seus aspectos estruturais (dados) e comportamentais (transações), para correspondentes construções na linguagem de implementação (C e SQL). Adicionalmente, são discutidos aspectos de otimização de consultas no âmbito da linguagem de especificação de transações e, também, aspectos de aninhamento de consultas para combinar diversos fluxos do diagrama ER/T+ em expressões complexas de consultas SQL. / This Ph.D thesis presents a graphic and textual specification model for database transactions systems (ER/T+) and, also, an implementation model for this specification. Suggest a proceduralization technique for declarative specifications using a data flow dependency graph to establish a precedence relation between the diagram flows of the graphics specification language. Furthermore it presents the execution mechanism of the proposal specification language and the behavioral and structural rules for mapping the specification language into corresponding implementation language (C and SQL) constructions. Additionaly, are discussed query optimization aspects for transaction specification language and aspects of nested queries to combine various ER/T+ diagram flows into complex SQL query expressions

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.

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.