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.

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.

abstract: Critical infrastructures in healthcare, power systems, and web services, incorporate cyber-physical systems (CPSes), where the software controlled computing systems interact with the physical environment through actuation and monitoring. Ensuring software safety in CPSes, to avoid hazards to property and human life as a result of un-controlled interactions, is essential and challenging. The principal hurdle in this regard is the characterization of the context driven interactions between software and the physical environment (cyber-physical interactions), which introduce multi-dimensional dynamics in space and time, complex non-linearities, and non-trivial aggregation of interaction in case of networked operations. Traditionally, CPS software is tested for safety either through experimental trials, which can be expensive, incomprehensive, and hazardous, or through static analysis of code, which ignore the cyber-physical interactions. This thesis considers model based engineering, a paradigm widely used in different disciplines of engineering, for safety verification of CPS software and contributes to three fundamental phases: a) modeling, building abstractions or models that characterize cyberphysical interactions in a mathematical framework, b) analysis, reasoning about safety based on properties of the model, and c) synthesis, implementing models on standard testbeds for performing preliminary experimental trials. In this regard, CPS modeling techniques are proposed that can accurately capture the context driven spatio-temporal aggregate cyber-physical interactions. Different levels of abstractions are considered, which result in high level architectural models, or more detailed formal behavioral models of CPSes. The outcomes include, a well defined architectural specification framework called CPS-DAS and a novel spatio-temporal formal model called Spatio-Temporal Hybrid Automata (STHA) for CPSes. Model analysis techniques are proposed for the CPS models, which can simulate the effects of dynamic context changes on non-linear spatio-temporal cyberphysical interactions, and characterize aggregate effects. The outcomes include tractable algorithms for simulation analysis and for theoretically proving safety properties of CPS software. Lastly a software synthesis technique is proposed that can automatically convert high level architectural models of CPSes in the healthcare domain into implementations in high level programming languages. The outcome is a tool called Health-Dev that can synthesize software implementations of CPS models in healthcare for experimental verification of safety properties. / Dissertation/Thesis / Ph.D. Computer Science 2012

Conselho Nacional de Desenvolvimento CientÃfico e TecnolÃgico / 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. / 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 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.