No description available.

[pt] A avaliação de desempenho em operações humanitárias é questão-chave, pois possibilita melhores resultados e rapidez no atendimento. Uma das perspectivas de avaliação está relacionada a quanto as operações humanitárias podem ser efetivas e eficientes na ajuda aos beneficiários. Nesse sentido, o objetivo principal deste estudo é propor um framework para avaliação de desempenho de operações humanitárias, a partir da percepção dos beneficiários. Para isso, 22 artigos são selecionados e 130 indicadores são identificados por meio de uma revisão sistemática da literatura. Com base nestes resultados, são propostos uma taxonomia de critérios pré e pós-desastres, uma agenda de pesquisa específica para aprimoramento do tópico e um framework para avaliação do desempenho. Em seguida, um estudo empírico abordando o caso sobre a queda da área de lazer de um prédio é conduzido, composto por uma survey, com os moradores do prédio e um estudo de caso com a empresa responsável pela obra. A survey apresenta 44 respostas com satisfações, insatisfações, pontos positivos e negativos da operação pós-desastre, onde os principais resultados apontam que existem insatisfações relacionadas a questão de adaptação ao novo local de moradia e o principal ponto positivo diz respeito a rapidez nos primeiros atendimentos as pessoas afetadas. Os resultados do estudo de caso apontam que a empresa se preocupa com a satisfação dos seus clientes e é flexível para atendimento das necessidades dos mesmos. Assim, os resultados conferem uma primeira validação do framework, sendo sugerido como pesquisas futuras o desenvolvimento de estudos aprofundando outros tipos de desastres. / [en] Performance evaluation in humanitarian operations is a vital issue, as it enables better results and faster service. One of the evaluation perspectives is related to how humanitarian operations can be effective and efficient in helping beneficiaries. In this sense, the main objective of this study is to propose a framework for evaluating the performance of humanitarian operations, based on the beneficiaries perception. For this, 22 articles are selected and 130 indicators are identified through a systematic review of the literature. Based on these results, a taxonomy of pre- and post-disaster criteria, a specific research agenda for topic improvement, and a framework for performance evaluation are proposed. Then, an empirical study addressing the case about the fall of the leisure area of a building is conducted, consisting of a survey, with the residents of the building and a case study with the company responsible for the work. The survey presents 44 responses with satisfactions, dissatisfactions, positives, and negatives of the post-disaster operation, where the main results indicate that there are dissatisfactions related to the issue of adaptation to the new place of residence and the main positive point concerns the speed of the first visits affected people. The results of the case study indicate that the company is concerned with the satisfaction of its customers and is flexible to meet their needs. Thus, the results give a first validation of the framework, being suggested as future research the development of studies deepen other types of disasters.

Given a formal model of the behavior of a system, an objective and some notion of control the goal of controller synthesis is to construct a (finite-state) controller that ensures that the system always satisfies the objective. Often, the controller can base its decisions only on limited observations of the system. This notion of limited observability induces a partial-information game between the controller and the uncontrollable part of the system. A successful controller then realizes an observation-based strategy that enforces the objective. In this thesis we consider the controller synthesis problem in the linear-time setting where the behavior of the system is given as a nondeterministic, labeled transitions system A, where the controller can only partially observe and control the behavior of A. The goal of the thesis is to develop a compositional approach for constructing controllers, suitable to treat conjunctive cascades of linear-time objectives P_1, P_2, ..., P_k in an online manner. We iteratively construct a controller C_1 for system A enforcing P_1, then a controller C_2 enforcing P_2 for the parallel composition of the first controller with the system, and so on. It is crucial for this approach that each controller C_i enforces P_i in a most general manner, being as permissive as possible. Otherwise, behavior that is needed to enforce subsequent objectives could be prematurely removed. Standard notions of strategies and controllers only allow the most general treatment for the limited class of safety objectives. We introduce a novel concept of most general strategies and controllers suited for the compositional treatment of objectives beyond safety. We demonstrate the existence of most general controllers for all enforceable, observation-based omega-regular objectives and provide algorithms for the construction of such most general controllers, with specialized variants for the subclass of safety and co-safety objectives. We furthermore adapt and apply our general framework for the compositional synthesis of most general controllers to the setting of exogenous coordination in the context of the channel-based coordination language Reo and the constraint automata framework and report on our implementation in the verification toolset Vereofy. The construction of most general controllers in Vereofy for omega-regular objectives relies on our tool ltl2dstar for generating deterministic omega-automata from Linear Temporal Logic (LTL) formulas. We introduce a generic improvement for exploiting insensitiveness to stuttering during the determinization construction and evaluate its effectiveness in practice. We further investigate the performance of recently proposed variants of Safra\'s determinization construction in practice.

Given a formal model of the behavior of a system, an objective and some notion of control the goal of controller synthesis is to construct a (finite-state) controller that ensures that the system always satisfies the objective. Often, the controller can base its decisions only on limited observations of the system. This notion of limited observability induces a partial-information game between the controller and the uncontrollable part of the system. A successful controller then realizes an observation-based strategy that enforces the objective. In this thesis we consider the controller synthesis problem in the linear-time setting where the behavior of the system is given as a nondeterministic, labeled transitions system A, where the controller can only partially observe and control the behavior of A. The goal of the thesis is to develop a compositional approach for constructing controllers, suitable to treat conjunctive cascades of linear-time objectives P_1, P_2, ..., P_k in an online manner. We iteratively construct a controller C_1 for system A enforcing P_1, then a controller C_2 enforcing P_2 for the parallel composition of the first controller with the system, and so on. It is crucial for this approach that each controller C_i enforces P_i in a most general manner, being as permissive as possible. Otherwise, behavior that is needed to enforce subsequent objectives could be prematurely removed. Standard notions of strategies and controllers only allow the most general treatment for the limited class of safety objectives. We introduce a novel concept of most general strategies and controllers suited for the compositional treatment of objectives beyond safety. We demonstrate the existence of most general controllers for all enforceable, observation-based omega-regular objectives and provide algorithms for the construction of such most general controllers, with specialized variants for the subclass of safety and co-safety objectives. We furthermore adapt and apply our general framework for the compositional synthesis of most general controllers to the setting of exogenous coordination in the context of the channel-based coordination language Reo and the constraint automata framework and report on our implementation in the verification toolset Vereofy. The construction of most general controllers in Vereofy for omega-regular objectives relies on our tool ltl2dstar for generating deterministic omega-automata from Linear Temporal Logic (LTL) formulas. We introduce a generic improvement for exploiting insensitiveness to stuttering during the determinization construction and evaluate its effectiveness in practice. We further investigate the performance of recently proposed variants of Safra\'s determinization construction in practice.

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.

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.

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.

The wrist is one of the most complex joints in the human body. As such, the wrist joint is difficult to model due to the number of bones involved and its intricate soft tissue interactions. Many studies have attempted modeling the wrist previously; however, the majority of these studies simplify the joint into two-dimensions or idealized mechanical joints to reduce the complexity of the simulation. While these approaches still yield valuable information, the omission of a third-dimension or geometry defined movements limits the models’ usefulness in predicting joint function under non-idealized conditions. Therefore, the goal of this study was to develop a computational model of the wrist joint complex using commercially available software, whereby joint motion and behavior is dictated by highly accurate three-dimensional articular contact, ligamentous constraints, muscle loads, and external perturbations only. As such, a computational model of the human wrist was created using computed tomography (CT) images of a cadaver right upper extremity. Commercially available medical imaging software and three-dimensional computer aided design (CAD) software were used to reconstruct the osteoarticular surfaces and accurately add soft tissue constraints, as well as calculate kinematic motion simulations. The model was able to reproduce physiologic motion including flexion/extension and radial/ulnar deviation. Validation of the model was achieved by comparing predicted results from the model to the results of a published cadaveric experiment that analyzed wrist function under effects of various surgical procedures. The model was used to replicate the exact testing conditions prescribed for the experiment, and the model was able to accurately reproduce the trends and, in many instances, the magnitudes of the range of motion measurements in the study. Furthermore, the model can now be used to predict the magnitudes for the joint contact forces within the wrist as well as the tension developed in ligaments in hopes locating potential areas of concern after these surgical procedures have been conducted, including further development of arthritis in the wrist and ligament breakdown.

Los métodos formales han alcanzado un uso más masivo en la construcción de sistemas reales, ya que ayudan a aumentar la calidad del software y la fiabilidad. Las especificaciones formales pueden ser usadas a lo largo de todo el ciclo de vida del desarrollo de software y también este desarrollo puede ser automatizado por medio de herramientas de amplia variedad y propósito como model checking, verificación, animación, generación de datos para testing, como también refinamiento de especificaciones a implementaciones. Cuando las especificaciones se usan en etapas iniciales del proceso, se ayuda a revelar ambigüedades, omisiones, inconsistencias, errores o interpretaciones erróneas que podrían ser detectados durante pruebas costosas y en las fases de depuración. Sin embargo, las especificaciones formales no son muy familiares para los stakeholders, cuya participación activa es crucial en los primeros estados del proceso de desarrollo de software para entender y comunicar un problema. Estas actividades son especialmente útiles en el análisis de dominio, pues su primera etapa consiste en capturar el conocimiento de un dominio en particular, lo que hace necesario disponer de un modelo que sea comprensible por los ingenieros de software y expertos del dominio. Para contribuir a reducir esta brecha, se trabaja en la integración de una fase de análisis de dominio con el método formal de desarrollo de software RAISE, a fin de especificar una familia de sistemas para producir aplicaciones cualitativas y fiables en un dominio, promover la reutilización temprana y reducción de los costos de desarrollo.

Advancements in computational capabilities have allowed researchers to turn towards modeling as an efficient tool to replicate and predict outcomes of complex systems. Computational models of the musculoskeletal system have gone through various iterations with early versions employing dramatic simplifications. In this work, a three-dimensional computational model of the wrist joint was developed. It accurately recreated the skeletal structures of the hand and wrist and represented the constraints imposed by soft tissue structures like ligaments, tendons, and other surrounding tissues. It was developed to function as a tool to investigate the biomechanical contributions of structures and the kinematic response of the wrist joint. The model was created with the use of a commercially available computer-aided design software employing the rigid body modeling methodology. It was validated against three different cadaveric experimental studies which investigated changes in biomechanical response following radioscapholunate fusion and proximal row carpectomy procedures. The kinematic simulations performed by the model demonstrated quantitatively accurate responses for the range of motions for both surgical procedures. It also provided some understanding to the trends in carpal bone contact force changes observed in surgically altered specimens. The model provided additional insight into the importance of structures like the triangular fibrocartilage and the capsular retinacular structures, both of which are currently not very well understood. As better understanding of components of the wrist joint is achieved, this model could function as an important tool in preoperative planning and generating individualized treatment regiments.