No presente trabalho serão apresentadas questões usuais em jogos diferenciais, nos quais os jogadores envolvidos têm objetivos diferentes; ou seja, enquanto um dos jogadores tenta fugir, o outro tenta pegar. Além disso, será definido um modelo de especificação para o jogo diferencial lobos e cordeiro. As Redes de Petri foram escolhidas como forma de especificação para o jogo proposto. Assim, o objetivo será estabelecer estratégias eficientes para o jogo lobos e cordeiro para que se possa realizar um estudo da complexidade das questões apresentadas para este jogo, levando-se em consideração a especificação formal apresentada para tal jogo. / In this work usual questions in differential games will be presented, in which the involved players have different objectives; that is, while one of the players tries "to run away", the other tries "to catch". Moreover, a specification for the differential game "wolves and lamb" will be defined. The Petri Nets had been chosen as specification formalism for the considered game. Thus, the objective is to establish efficient strategies for the game wolves and lamb so that we can carry out a study of the complexity of the presented questions, taking into consideration the presented formal specification for the game.

A integração estruturada e consistente de diversas especificações (ou visões) de um sistema é hoje uma questão essencial na moderna abordagem para especificação e desenvolvimento de software. Neste contexto, precisamos de uma teoria que fale sobre formalismos de especificação e que ao mesmo tempo nos ofereça conceitos e construções para estabelecer-mos relações entre eles. Com este trabalho temos o objetivo de discutir noções rigorosas para idéia de lógica, técnicas fundamentais para relacioná-Ias e mostrar a utilização destes concei¬tos para abordar a questão da interoperabilidade formal, especialmente de provas. Como formalização para idéia de lógica utilizaremos as Instituições de Goguen & Burstall e a extensão de Meseguer para General Logics. Como técnica para rela¬cionar lógicas trabalharemos com os mapeamentos Plain e Simples de Meseguer. Atenção especial é dada à discussão das propriedades destes mapeamentos com vis¬ta à reutilização de componentes lógicos, especialmente da relação de consequência entre fórmulas. Contribuições desta dissertação incluem um tratamento acessível para os con¬ceitos fundamentais necessários para estudar lógicas e sua integração, uma expo¬sição uniforme e detalhada de uma família de sistemas lógicos e uma apresentação categórica desta integração via mapeamentos. / The integration in a sound and structured way of several specifications (or views) of a system is a key research area in (modern) software specification and development. In this context, we need a theory to speak not only about specification logics, but also one that can offer us concepts and constructions to establish relations between these formalisms. In this work we have the purpose of discussing rigorous notions for the idea of logic, presenting fundamental techniques to relate them, and introducing important constructions to approach the problem of formal interoperability, most notably of proofs. As a formalization of the informal idea of a logical system, we use Goguen & Burstall's concept of Institutions and Meseguer's further extension to General Logics. Meseguer's Plain and Simple Maps of Institutions are the tools we use to relate and map logics. Besides, special attention is given for the discussion of the essential properties of these maps concerning the borrowing of logical components, specially of consequence relations. Contributions of this thesis include a smooth presentation of fundamental techniques to study and relate logics, an uniform and detailed exposition of a num¬ber of logical systems, and a categorical formalization of relations between these formalisms by way of maps between institutions.

Made available in DSpace on 2014-06-12T15:49:26Z (GMT). No. of bitstreams: 1 license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2009 / Esta tese trata de um problema muito comum em verificação formal: explosão de estados. O problema desabilita a verificação automática de propriedades através da verificação de modelos. Isto é superado pelo uso de abstração de dados, em que o espaço de estados de umsistema é reduzido usandoumprincípio simples: descartando detalhes de tal forma que o espaço de estados torna-se finito exibindo ainda propriedades desejáveis. Isso habilita o uso de verificacao de modelos, já que o modelo mais simples (abstrato) pode ser usado no lugar do modelo original (concreto). Entretanto, abstrações podem perder propriedades já que o nível de precisão é degradado, para algumas propriedades. Abstrair tipos de dados é, normalmente, uma tarefa não-trivial e requer uma profunda experiência: o usuário deve prover domínios abstratos, uma relacao matemática entre os estados (concreto e abstrato), uma inicialização abstrata, e uma versão abstrata para cada operação. A abordagem proposta nesta tese transfere a maior parte dessa experiência para um procedimento sistemático que calcula relações de abstração. Essas relações são a base para as relações matemáticas entre os estados, como também suas imagens determinam os domínios abstratos (os valores de dados mínimos para preservar propriedades). Também propomos meta-modelos para estabelecer como o sistema abstrato é inicializado e como operações são tornadas fechadas sob os domínios abstratos. Isso elimina o conhecimento requerido do usuário para fornecer as versões abstratas para a inicialização e operações. Os meta-modelos garantem a correspondência entre os sistemas concreto e abstrato. Assim, nós derivamos especificações abstratasa partir de concretas de tal formaque a especificação concreta é mais determinística que a abstrata por construção. Esta é a idéia por trás da teoria sobrejacente de nossa abordagem de abstração de dados: refinamento de dados. A notação adotada é CSPZ uma integração formal das linguagens de especificação CSP e Z. Uma especificação CSPZ tem duas partes: uma parte comportamental (CSP) e outra de dados (Z). O procedimento de cálculo foca na parte de Z, mas os resultados são usados na especificação CSPZ por completo; isso segue da independência de dados da parte de CSP (os dados não podem afetar seu comportamento). Ao final, a verificação automática é obtida pela conversão da especificação CSPZ em CSP puro e em seguida pelo reuso do verificador de modelos padrão de CSP. Nossa abordagem compreende as seguintes tarefas: nós extraímos a parte de Z de uma especificação CSPZ (puramente sintática), calculamos as relações de abstração (através de uma análise sistemática de predicados com uso de ferramenta de suporte), construímos as relações matemáticas entre os estados, os esquemas abstratos (definidos por meta-modelos), e realizamos um pós-processamento na especificação abstrata. A última tarefa pode resultar em alguns ajustes nas relações de abstração. A novidade prática e maior contribuição de nossa abordagem é o cálculo sistemático das das relações de abstração, que são os elementos chave de todas abordagens de abstração de dados que estudamos ao longo dos últimos anos. O refinamento de dados entre o sistema produzido por nossa abordagem e o original (concreto) é a segunda contribuição deste trabalho. O procedimento sistemático é na verdade uma técnica de análise de predicado que usa as restrições sobre os dados para determinar seus valores mínimos que são suficientes para preservar o comportamento do sistema. Isso evita a execução (concreta ou simbólica) do sistema analisado. Os passos produzem mapeamentos que revelam alguns elementos cruciais: o espaço de estados abstrato e as relações matemáticas entre ele e o espaço de estados concreto. Essas relações são usadas para construir o sistema abstrato seguindo o formato estabelecido pelos meta-modelos. As limitações de nossa abordagem são também discutidas. Nós aplicamos a abordagem a alguns exemplos também analisados por outras técnicas da literatura. Discutimos também sobre trabalhos relacionados procurando destacar vantagens, desvantagens e aspectos complementares. Finalmente, apresentamos nossas conclusões e futuras direções para este trabalho

The term verification can mean different things to different people based on their background and the context of research. Comparably the term runtime might bring about similar disarray with lesser confusion. Whilst a software application executes on a system, there are libraries and codes that facilitates the execution of that binary, these processes and libraries make up the runtime environment, and verification in this context refers to the concrete techniques that verify a run and checks if it satisfies or defies the specified requirements. This study is specifically concerned with runtime verification systems, and how to make use of them in a limited-resource environment such as embedded systems or Programmable Logic Controller (PLC). It is of utmost importance to validate the conformance of a system, specially those in automotive and transportation industry. Vehicles such as trains are responsible to transport millions of people everyday which makes safety and reliability of the system the most prime component of bunch. Many manufacturers employs state of the art technologies and processes to endure the safety of the final product. Since most of the parts in vehicles (including trains) are computer controlled, the system (OS, application, control system, etc.) should undergo proper and comprehensive tests to single out even the smallest anomalies and misbehaviour. While traditional software testing can detect most of the anomalies, runtime verification can be used as a complementary method to passively monitor the running system and point out those behaviours and malfunctioning that are otherwise close to impossible to be caught. This thesis investigates runtime verification in train manufacturing, and propose a structured, contemporary process and system to monitor the train control system for conformance. Furthermore several methods of formal specification to be used for declaration of specification were explored and a suitable choice for this case study was suggested, in addition a proof of concept tool to demonstrate the entire process is developed as well.

We present a pattern system for property specification. It extends the existing patterns identified in [4] which allow to reason about occurrence and order of events, but not about time conditions. Introducing time-related patterns allows the specification of real-time requirements. The paper is limited to 3 pages. Therefore it contains only basic ideas. The details can be found in [9].

Many industrial control systems use programmable logic controllers (PLCs) since they provide a highly reliable, off-the-shelf hardware platform. On the programming side, function blocks (FBs) are reusable PLC components that can be composed to implement the required system behaviour. A higher quality system may be realized if the FBs are pre-certified to be compliant with an international standard such as IEC 61131-3. Unfortunately, the set of programming notations defined in IEC 61131-3 lack well-defined formal semantics. As a result, tool vendors and users of PLCs may have inconsistent interpretations of the expected system behaviour. To address this issue, we propose an engineering method for formally verifying the conformance of candidate implementations of FBs (and their compositions) to their high-level, input-output requirements. The proposed method is sufficiently general to handle FBs supplied by IEC 61131-3, and industrial FB applications involving real-time requirements. Our method involves several steps. First, we use tabular expressions to ensure the completeness and disjointness of the requirements for the FB. Second, we formalize the candidate implementation(s) of the FB in question. Third, we state and prove theorems regarding the consistency and correctness of the FB. All three steps are performed using the Prototype Verification Systems (PVS) proof assistant. As a first case study, we apply our approach to the IEC 61131-3 standard to examine the entire library of FBs and their supplied implementations described in structured text (ST) and function block diagrams (FBDs). As a second case study, we apply our approach to two realistic sub-systems taken from the nuclear domain. Applying the proposed method, we identified three kinds of issues: ambiguous behavioural descriptions, missing assumptions, and erroneous implementations. Furthermore, we suggest solutions to these issues. / Thesis / Doctor of Philosophy (PhD) / A formal verification approach for the function block based control systems

The use of third-party components is helpful while writing complex software systems, but it can be difficult to debug software that interacts with third-party components. To address this problem, a mechanism for determining if one is using the component correctly would be beneficial. Reading component documentation may or may not help, depending on its clarity and precision. A formally specified contract for that component would be better, and would also allow run-time contract verification via assertions. The client of the component could enable these assertions during development and debugging, and then disable them for the final production release to increase performance. This thesis presents nContract, a tool that provides configurable run-time contract verification without requiring component recompilation or source code access. nContract allows component developers to formally specify .NET components using attributes. This contract information is retrieved from the compiled component's metadata and a subclass is generated for each formally specified type. All members of the component's interface are overridden and contract assertions are wrapped around calls to the base class. As long as the component client uses a factory to create instances of the component's types, the decision of whether or not to create assertion-checked or unchecked objects can be deferred until run-time. / Master of Science

In recent years, there has been a flood of continuously changing information from a variety of web resources such as web databases, web sites, web services and programs. Online Social Networks (OSNs) represent such a field where huge amounts of information are being posted online over time. Due to the nature of OSNs, which offer a productive source for qualitative and quantitative personal information, researchers from various disciplines contribute to developing methods for extracting data from OSNs. However, there is limited research which addresses extracting data automatically. To the best of the author's knowledge, there is no research which focuses on tracking the real time changes of information retrieved from OSN profiles over time and this motivated the present work. This thesis presents different approaches for automated Data Extraction (DE) from OSN: crawler, parser, Multi Agent System (MAS) and Application Programming Interface (API). Initially, a parser was implemented as a centralized system to traverse the OSN graph and extract the profile's attributes and list of friends from Myspace, the top OSN at that time, by parsing the Myspace profiles and extracting the relevant tokens from the parsed HTML source files. A Breadth First Search (BFS) algorithm was used to travel across the generated OSN friendship graph in order to select the next profile for parsing. The approach was implemented and tested on two types of friends: top friends and all friends. In case of top friends, 500 seed profiles have been visited; 298 public profiles were parsed to get 2197 top friends' profiles and 2747 friendship edges, while in case of all friends, 250 public profiles have been parsed to extract 10,196 friends' profiles and 17,223 friendship edges. This approach has two main limitations. The system is designed as a centralized system that controlled and retrieved information of each user's profile just once. This means that the extraction process will stop if the system fails to process one of the profiles; either the seed profile (first profile to be crawled) or its friends. To overcome this problem, an Online Social Network Retrieval System (OSNRS) is proposed to decentralize the DE process from OSN through using MAS. The novelty of OSNRS is its ability to monitor profiles continuously over time. The second challenge is that the parser had to be modified to cope with changes in the profiles' structure. To overcome this problem, the proposed OSNRS is improved through use of an API tool to enable OSNRS agents to obtain the required fields of an OSN profile despite modifications in the representation of the profile's source web pages. The experimental work shows that using API and MAS simplifies and speeds up the process of tracking a profile's history. It also helps security personnel, parents, guardians, social workers and marketers in understanding the dynamic behaviour of OSN users. This thesis proposes solutions for web database processing on data extraction from OSNs by the use of parser and MAS and discusses the limitations and improvements.

Process algebra, formal specification, and model checking are all well studied techniques in the analysis of concurrent computer systems. More recently these techniques have been applied to the analysis of biochemical systems which, at an abstract level, have similar patterns of behaviour to concurrent processes. Process algebraic models and temporal logic specifications, along with their associated model-checking techniques, have been used to analyse biochemical systems. In this thesis we develop a spatio-temporal logic, the Logic of Behaviour in Context (LBC), for the analysis of biochemical models. That is, we define and study the application of a formal specification language which not only expresses temporal properties of biochemical models, but expresses spatial or contextual properties as well. The logic can be used to express, or specify, the behaviour of a model when it is placed into the context of another model. We also explore the types of properties which can be expressed in LBC, various algorithms for model checking LBC - each an improvement on the last, the implementation of the computational tools to support model checking LBC, and a case study on the analysis of models of post-translational biochemical oscillators using LBC. We show that a number of interesting and useful properties can be expressed in LBC and that it is possible to express highly useful properties of real models in the biochemistry domain, with practical application. Statements in LBC can be thought of as expressing computational experiments which can be performed automatically by means of the model checker. Indeed, many of these computational experiments can be higher-order meaning that one succinct and precise specification in LBC can represent a number of experiments which can be automatically executed by the model checker.

[pt] Neste trabalho propomos uma arquitetura para a verificação formal de protocolos e algoritmos distribuídos. Esta pode ser vista como uma camada mais abstrata sobre o processo tradicional de verificação formal, onde temos a especificação e propriedade a serem verificadas, o verificador e o resultado retornado por este. O objetivo é simplificar o processo de especificação e verificação formal de protocolos e algoritmos distribuídos através de um ambiente mais dedicado. A parte principal desta arquitetura é a linguagem de especificação LEP, que contém construções de domínio-especifíco para simplificar a especificação destes sistemas. Outra característica desta linguagem é separar as especificações da topologia e do protocolo propriamente dito. Acreditamos que esta separação é válida pois torna mais clara a intenção das partes e ainda permite, por exemplo, o reuso de uma topologia entre diferentes especificações de protocolos. Assim, visamos oferecer uma linguagem cujos exemplos de especificações devem se assemelhar às descrições de algoritmos encontradas nos livros didáticos. Além disso, de forma a se ter a entrada e a saída dos verificadores formais de forma a obter a saída no nível de abstração de LEP. / [en] In this work we propose an architecture for the formal verification of protocols and distribued algoritms. This can be see as a more abstract layer over the ordinary process of formal verification, where we have just the specification of the protocol and properties to be verified, and the formal tool. Our goal is to simplifu the specification and formal verification of protocols and distributed algorithms through a dedicated environment. The core of the architecture is its input specification language (Lep), which provides domain-specific constructions for simplifying the specification of those systems. With LEP the specification of the protocol and the specification of the topology to be referred to protocol are given separetely. We feel that this division improves the legibility of both and allows the reuse of the specification of a topology among distinct protocols. Using this approach we try to offer a language whose specifications should be similar to the descriptions of the algorithms found on the didactic books. Moreover, in order to have the input and output of the architecture compatible, we also propose a way of processing the result of the formal verification tool. Then we could have the result on the abstract level of LEP.