Privacy policies often place restrictions on the purposes for which a governed entity may use personal information. For example, regulations, such as the Health Insurance Portability and Accountability Act (HIPAA), require that hospital employees use medical information for only certain purposes, such as treatment, but not for others, such as gossip. Thus, using formal or automated methods for enforcing privacy policies requires a semantics of purpose restrictions to determine whether an action is for a purpose. We provide such a semantics using a formalism based on planning. We model planning using a modified version of Markov Decision Processes (MDPs), which exclude redundant actions for a formal definition of redundant. We argue that an action is for a purpose if and only if the action is part of a plan for optimizing the satisfaction of that purpose under the MDP model. We use this formalization to define when a sequence of actions is only for or not for a purpose. This semantics enables us to create and implement an algorithm for automating auditing, and to describe formally and compare rigorously previous enforcement methods. We extend this formalization to Partially Observable Markov Decision Processes (POMDPs) to answer when information is used for a purpose. To validate our semantics, we provide an example application and conduct a survey to compare our semantics to how people commonly understand the word “purpose”.

No description available.

Concurrent programs are known to be complicated because synchronisation is required amongst the processes in order to ensure safety (nothing bad ever happens) and progress (something good eventually happens). Due to possible interference from other processes, a straightforward rearrangement of statements within a process can lead to dramatic changes in the behaviour of a program, even if the behaviour of the process executing in isolation is unaltered. Verifying concurrent programs using informal arguments are usually unconvincing, which makes formal methods a necessity. However, formal proofs can be challenging due to the complexity of concurrent programs. Furthermore, safety and progress properties are proved using fundamentally different techniques. Within the literature, safety has been given considerably more attention than progress. One method of formally verifying a concurrent program is to develop the program, then perform a post-hoc verification using one of the many available frameworks. However, this approach tends to be optimistic because the developed program seldom satisfies its requirements. When a proof becomes difficult, it can be unclear whether the proof technique or the program itself is at fault. Furthermore, following any modifications to program code, a verification may need to be repeated from the beginning. An alternative approach is to develop a program using a verify-while-develop paradigm. Here, one starts with a simple program together with the safety and progress requirements that need to be established. Each derivation step consists of a verification, followed by introduction of new program code motivated using the proofs themselves. Because a program is developed side-by-side with its proof, the completed program satisfies the original requirements. Our point of departure for this thesis is the Feijen and van Gasteren method for deriving concurrent programs, which uses the logic of Owicki and Gries. Although Feijen and van Gasteren derive several concurrent programs, because the Owicki-Gries logic does not include a logic of progress, their derivations only consider safety properties formally. Progress is considered post-hoc to the derivation using informal arguments. Furthermore, rules on how programs may be modified have not been presented, i.e., a program may be arbitrarily modified and hence unspecified behaviours may be introduced. In this thesis, we develop a framework for developing concurrent programs in the verify-while-develop paradigm. Our framework incorporates linear temporal logic, LTL, and hence both safety and progress properties may be given full consideration. We examine foundational aspects of progress by formalising minimal progress, weak fairness and strong fairness, which allow scheduler assumptions to be described. We formally define progress terms such as individual progress, individual deadlock, liveness, etc (which are properties of blocking programs) and wait-, lock-, and obstruction-freedom (which are properties of non-blocking programs). Then, we explore the inter-relationships between the various terms under the different fairness assumptions. Because LTL is known to be difficult to work with directly, we incorporate the logic of Owicki-Gries (for proving safety) and the leads-to relation from UNITY (for proving progress) within our framework. Following the nomenclature of Feijen and van Gasteren, our techniques are kept calculational, which aids derivation. We prove soundness of our framework by proving theorems that relate our techniques to the LTL definitions. Furthermore, we introduce several methods for proving progress using a well-founded relation, which keeps proofs of progress scalable. During program derivation, in order to ensure unspecified behaviour is not introduced, it is also important to verify a refinement, i.e., show that every behaviour of the final (more complex) program is a possible behaviour of the abstract representation. To facilitate this, we introduce the concept of an enforced property, which is a property that the program code does not satisfy, but is required of the final program. Enforced properties may be any LTL formula, and hence may represent both safety and progress requirements. We formalise stepwise refinement of programs with enforced properties, so that code is introduced in a manner that satisfies the enforced properties, yet refinement of the original program is guaranteed. We present derivations of several concurrent programs from the literature.

Thesis (Ph. D.)--University of New South Wales, 2000. / Addenda sheet inserted. Includes bibliographic references. Also available online.

Thesis (Ph.D.)--University of Wollongong, 2006. / Typescript. Includes bibliographical references: leaf 153-168.

Thesis (M.S.)--University of Texas at El Paso, 2008. / Title from title screen. Vita. CD-ROM. Includes bibliographical references. Also available online.

Title from first page of PDF document. Includes bibliographical references (p. Xx-Xx).

Control of complex systems satisfying rich temporal specification has become an increasingly important research area in fields such as robotics, control, automotive, and manufacturing. Popular specification languages include temporal logics, such as Linear Temporal Logic (LTL) and Computational Tree Logic (CTL), which extend propositional logic to capture the temporal sequencing of system properties. The focus of this dissertation is on the control of high-dimensional systems and on timed specifications that impose explicit time bounds on the satisfaction of tasks. This work proposes and evaluates methods and algorithms for synthesizing provably correct control policies that deal with the scalability problems. Ideas and tools from formal verification, graph theory, and incremental computing are used to synthesize satisfying control strategies. Finite abstractions of the systems are generated, and then composed with automata encoding the specifications. The first part of this dissertation introduces a sampling-based motion planning algorithm that combines long-term temporal logic goals with short-term reactive requirements. The specification has two parts: (1) a global specification given as an LTL formula over a set of static service requests that occur at the regions of a known environment, and (2) a local specification that requires servicing a set of dynamic requests that can be sensed locally during the execution. The proposed computational framework consists of two main ingredients: (a) an off-line sampling-based algorithm for the construction of a global transition system that contains a path satisfying the LTL formula, and (b) an on-line sampling-based algorithm to generate paths that service the local requests, while making sure that the satisfaction of the global specification is not affected. The second part of the dissertation focuses on stochastic systems with temporal and uncertainty constraints. A specification language called Gaussian Distribution Temporal Logic is introduced as an extension of Boolean logic that incorporates temporal evolution and noise mitigation directly into the task specifications. A sampling-based algorithm to synthesize control policies is presented that generates a transition system in the belief space and uses local feedback controllers to break the curse of history associated with belief space planning. Switching control policies are then computed using a product Markov Decision Process between the transition system and the Rabin automaton encoding the specification.The approach is evaluated in experiments using a camera network and ground robot. The third part of this dissertation focuses on control of multi-vehicle systems with timed specifications and charging constraints. A rich expressivity language called Time Window Temporal Logic (TWTL) that describes time bounded specifications is introduced. The temporal relaxation of TWTL formulae with respect to the deadlines of tasks is also discussed. The key ingredient of the solution is an algorithm to translate a TWTL formula to an annotated finite state automaton that encodes all possible temporal relaxations of the given formula. The annotated automata are composed with transition systems encoding the motion of all vehicles, and with charging models to produce control strategies for all vehicles such that the overall system satisfies the mission specification. The methods are evaluated in simulation and experimental trials with quadrotors and charging stations.

A abordagem de sistemas multiagentes tem sido cada vez mais utilizada para o desenvolvimento de sistemas complexos, o que despertou o interesse das pesquisas na área de engenharia de software orientada a agentes (AOSE) e modelos organizacionais. Neste contexto, esta tese estuda a aplicabilidade de alguns métodos formais tradicionais de engenharia de software para a especificação formal de organizações de sistemas multiagentes, analisando o uso da linguagem de especificação formal RSL para representar o modelo organizacional PopOrg. A escolha da linguagem RSL ocorreu pelo fato de ela ser uma linguagem de especificação formal que cobre amplo espectro de métodos de especificação formal (baseados em modelos e baseados em propriedades, aplicativos e imperativos, sequenciais e concorrentes) e o modelo PopOrg foi escolhido por ser um modelo mínimo de organização de sistemas multiagentes, concebido para representar o conjunto mínimo de aspectos estruturais e operacionais que tais organizações devem ter. O uso da linguagem RSL foi avaliado tanto para a especificação do aspecto estrutural dos sistemas PopOrg, quanto para especificação operacional desses sistemas. Um estudo preliminar realizado com a linguagem CSP para a especificação operacional do modelo PopOrg também é apresentado, visto que serviu como base para a especificação em RSL. Ao final, apresenta-se uma sugestão de extensão da linguagem RSL para sua maior aplicabilidade à especificação de sistemas multiagentes. / The multiagent systems approach have been increasingly used for the development of complex systems, which aroused the interest of research in Agent Oriented Software Engineering (AOSE) and organizational models. In this context, this thesis studies the applicability of some traditional formal methods of software engineering for the formal specification of multiagent systems organizations, analyzing the use of RSL formal specification language to represent the PopOrg organizational model. The choice of RSL language occurred because it is a formal specification language that covers a wide spectrum of formal specification methods (models-based and properties-based, applicative and imperative, sequential and concurrent) and the PopOrg model was chosen because it is a minimal model of multiagent systems organization, designed to represent the minimum set of structural and operational aspects that such organizations should have. The use of RSL language was evaluated both for specifying the structural aspect of PopOrg systems and the operational specification for these systems. A preliminary study carried out with the CSP language for the operational specification of PopOrg model is also presented, as was the basis for the specification in RSL. In the end, a suggestion is given for an extension of the RSL language, to allow for its wider applicability to the specification of multiagent systems.

MARCILON, Thiago Braga. Contratos formais para derivação e verificação de componentes paralelos. 2012. 156 f. Dissertação (Mestrado em ciência da computação)- Universidade Federal do Ceará, Fortaleza-CE, 2012. / Submitted by Elineudson Ribeiro (elineudsonr@gmail.com) on 2016-07-12T18:10:13Z No. of bitstreams: 1 2012_dis_tbmarcilon.pdf: 1474623 bytes, checksum: e61fb07d3a835088ff5a53d4eb684f2d (MD5) / Approved for entry into archive by Rocilda Sales (rocilda@ufc.br) on 2016-07-22T12:39:34Z (GMT) No. of bitstreams: 1 2012_dis_tbmarcilon.pdf: 1474623 bytes, checksum: e61fb07d3a835088ff5a53d4eb684f2d (MD5) / Made available in DSpace on 2016-07-22T12:39:34Z (GMT). No. of bitstreams: 1 2012_dis_tbmarcilon.pdf: 1474623 bytes, checksum: e61fb07d3a835088ff5a53d4eb684f2d (MD5) Previous issue date: 2012 / The use of cloud computing to offer High Performance Computing (HPC) services has been widely discussed in the academia and industry. In this respect, this dissertation is included in the context of designing a cloud computing platform for the development of component-based parallel computing applications, referred as cloud of components. Many important challenges about using the cloud of components relate to parallel programming, an error-prone task due to synchronization issues, which may lead to abortion and production of incorrect data during execution of applications, and the inefficient use of computational resources. These problems may be very relevant in the case of long running applications with tight timelines to obtain critical results, quite common in the context of HPC. One possible solution to these problems is the formal analysis of the behavior of the components of an application through the cloud services, before their execution. Thus, the users of the components may know if a component can be safely used in their application. In this scenario, formal methods becomes useful. In this dissertation, it is proposed a process for specification and derivation of parallel components implementation for the cloud of components. This process involves the formal specification of the components behavior through contracts described using the Circus formal specification language. Then, through a refinement and translation process, which takes the contract as a start point, one may produce an implementation of a component that may execute on a parallel computing platform. Through this process, it becomes possible to offer guarantees to developers about the components behavior in their applications. To validate the proposed idea, the process is applied to contracts that have been described based on two benchmarks belonging to the NAS Parallel Benchmarks, widely adopted in HPC for evaluate the performance of parallel programming and computing platforms. / A aplicação de nuvens computacionais para oferecer serviços de Computação de Alto Desempenho (CAD) é um assunto bastante discutido no meio acadêmico e industrial. Esta dissertação está inserida no contexto do projeto de uma nuvem computacional para o desenvolvimento e execução de aplicações de CAD baseadas em componentes paralelos, doravante denominada nuvem de componentes. Um dos principais desafios na sua utilização consiste no suporte à programação paralela, tarefa bastante suscetível à erros, pois tais erros podem levar, ao longo do desenvolvimento, a problemas de sincronização de processos, que podem causar abortamento da execução e a produção de dados incorretos, bem como a problemas relacionados ao uso ineficiente dos recursos computacionais. É importante que tais problemas sejam tratados no caso de aplicações de longa duração cujo respeito a um cronograma para obtenção de resultados é crítico, aplicações estas bastante comuns no contexto de CAD. Uma possível solução para tais problemas consiste na verificação do comportamento e das propriedades dos componentes na nuvem, antes que seja feita a sua execução, tornando possível que os usuários dos componentes da nuvem saibam se um componente pode ser utilizado com segurança em sua aplicação. Nesse cenário, o uso de métodos formais surge como uma alternativa atraente. A contribuição desta dissertação consiste em um processo de derivação e verificação de propriedades de componentes na nuvem. Tal processo envolve a especificação formal do comportamento dos componentes por meio de contratos descritos pela linguagem Circus. Então, através de um processo de refinamento e tradução tendo como ponto de partida o contrato, chega-se à implementação de um componente para execução sobre uma plataforma de computação paralela. Através desse processo, torna-se possível oferecer garantias aos desenvolvedores em relação ao comportamento dos componentes no contexto de suas aplicações. Para a prova de conceito, o processo é aplicado sobre a especificação "papel-e-caneta" de dois benchmarks do NAS Parallel Benchmarks, IS e CG, bastante difundidos na área de CAD.