Le model checking est une technique établie pour vérifier automatiquement qu’un modèle vérifie une propriété temporelle donnée. Lorsque le modèle viole la propriété, le model checker retourne un contre-exemple, i.e., une séquence d’actions menant à un état où la propriété n’est pas satisfaite. Comprendre ce contre-exemple pour le débogage de la spécification est une tâche compliquée pour plusieurs raisons: (i) le contre-exemple peut contenir un grand nombre d’actions; (ii) la tâche de débogage est principalement réalisée manuellement; (iii) le contre-exemple n’indique pas explicitement la source du bogue qui est caché dans le modèle; (iv) les actions les plus pertinentes ne sont pas mises en évidence dans le contre-exemple; (v) le contre-exemple ne donne pas une vue globale du problème.Ce travail présente une nouvelle approche qui rend plus accessible le model checking en simplifiant la compréhension des contre-exemples. Notre solution vise à ne garder que des actions dans des contre-exemples pertinents à des fins de débogage. Pour y parvenir, on détecte dans les modèles des choix spécifiques entre les transitions conduisant à un comportement correct ou à une partie du modèle erroné. Ces choix, que nous appelons neighbourhoods, se révèlent être de grande importance pour la compréhension du bogue à travers le contre-exemple. Pour extraire de tels choix, nous proposons deux méthodes différentes. La première méthode concerne le débogage des contre-exemples pour la violations de propriétés de sûreté. Pour ce faire, elle construit un nouveau modèle de l’original contenant tous les contre-exemples, puis compare les deux modèles pour identifier les neighbourhoods. La deuxième méthode concerne le débogage des contre-exemples pour la violations de propriétés de vivacité. À partir d’une propriété de vivacité, elle étend le modèle avec des informations de préfixe / suffixe correspondants à cette propriété. Ce modèle enrichi est ensuite analysé pour identifier les neighbourhoods.Un modèle annoté avec les neighbourhoods peut être exploité de deux manières. Tout d’abord, la partie erronée du modèle peut être visualisée en se focalisant sur les neighbourhoods, afin d’avoir une vue globale du comportement du bogue. Deuxièmement, un ensemble de techniques d’abstraction que nous avons développées peut être utilisé pour extraire les actions plus pertinentes à partir de contre-exemples, ce qui facilite leur compréhension. Notre approche est entièrement automatisée par un outil que nous avons implémenté et qui a été validé sur des études de cas réels dans différents domaines d’application. / Model checking is an established technique for automatically verifying that a model satisfies a given temporal property. When the model violates the property, the model checker returns a counterexample, which is a sequence of actions leading to a state where the property is not satisfied. Understanding this counterexample for debugging the specification is a complicated task for several reasons: (i) the counterexample can contain a large number of actions; (ii) the debugging task is mostly achieved manually; (iii) the counterexample does not explicitly point out the source of the bug that is hidden in the model; (iv) the most relevant actions are not highlighted in the counterexample; (v) the counterexample does not give a global view of the problem.This work presents a new approach that improves the usability of model checking by simplifying the comprehension of counterexamples. Our solution aims at keeping only actions in counterexamples that are relevant for debugging purposes. This is achieved by detecting in the models some specific choices between transitions leading to a correct behaviour or falling into an erroneous part of the model. These choices, which we call "neighbourhoods", turn out to be of major importance for the understanding of the bug behind the counterexample. To extract such choices we propose two different methods. One method aims at supporting the debugging of counterexamples for safety properties violations. To do so, it builds a new model from the original one containing all the counterexamples, and then compares the two models to identify neighbourhoods. The other method supports the debugging of counterexamples for liveness properties violations. Given a liveness property, it extends the model with prefix / suffix information w.r.t. that property. This enriched model is then analysed to identify neighbourhoods.A model annotated with neighbourhoods can be exploited in two ways. First, the erroneous part of the model can be visualized with a specific focus on neighbourhoods, in order to have a global view of the bug behaviour. Second, a set of abstraction techniques we developed can be used to extract relevant actions from counterexamples, which makes easier their comprehension. Our approach is fully automated by a tool we implemented and that has been validated on real-world case studies from various application areas.

In large-scale model-based development, developers periodically need to combine collections of interrelated models. These models may capture different features of a system, describe alternative perspectives on a single feature, or express ways in which different features alter one another's structure or behaviour. We refer to the process of combining a set of interrelated models as "model fusion". A number of factors make model fusion complicated. Models may overlap, in that they refer to the same concepts, but these concepts may be presented differently in each model, and the models may contradict one another. Models may describe independent system components, but the components may interact, potentially causing undesirable side effects. Finally, models may cross-cut, modifying one another in ways that violate their syntactic or semantic properties. In this thesis, we study three instances of the fusion problem for "behavioural models", motivated by real-world applications. The first problem is combining "partial" models of a single feature with the goal of creating a more complete description of that feature. The second problem is maintenance of "variant" specifications of individual features. The goal here is to combine the variants while preserving their points of difference (i.e., variabilities). The third problem is analysis of interactions between models describing "different" features. Specifically, given a set of features, the goal is to construct a composition such that undesirable interactions are absent. We provide an automated tool-supported solution to each of these problems and evaluate our solutions. The main novelties of the techniques presented in this thesis are (1) preservation of semantics during the fusion process, and (2) applicability to large and evolving collections of models. These are made possible by explicit modelling of partiality, variability and regularity in behavioural models, and providing semantic-preserving notions for relating these models.

In large-scale model-based development, developers periodically need to combine collections of interrelated models. These models may capture different features of a system, describe alternative perspectives on a single feature, or express ways in which different features alter one another's structure or behaviour. We refer to the process of combining a set of interrelated models as "model fusion". A number of factors make model fusion complicated. Models may overlap, in that they refer to the same concepts, but these concepts may be presented differently in each model, and the models may contradict one another. Models may describe independent system components, but the components may interact, potentially causing undesirable side effects. Finally, models may cross-cut, modifying one another in ways that violate their syntactic or semantic properties. In this thesis, we study three instances of the fusion problem for "behavioural models", motivated by real-world applications. The first problem is combining "partial" models of a single feature with the goal of creating a more complete description of that feature. The second problem is maintenance of "variant" specifications of individual features. The goal here is to combine the variants while preserving their points of difference (i.e., variabilities). The third problem is analysis of interactions between models describing "different" features. Specifically, given a set of features, the goal is to construct a composition such that undesirable interactions are absent. We provide an automated tool-supported solution to each of these problems and evaluate our solutions. The main novelties of the techniques presented in this thesis are (1) preservation of semantics during the fusion process, and (2) applicability to large and evolving collections of models. These are made possible by explicit modelling of partiality, variability and regularity in behavioural models, and providing semantic-preserving notions for relating these models.

Since the emergence of branding as an approach to marketing, the concept has been received with a great deal of interest and has stimulated ever increasing research in the area. Businesses have realized the importance of retaining existing customers and have begun to identify and apply ways to build long-term relationships with customers. These relationships with customers require an understanding of customer needs, business requirements and the influences that create a long-term relation which is more commonly known as brand loyalty. Several research studies including this one present the results of brand loyalty research in the form of a conceptual framework. From an academic viewpoint, the identification and application of all the relevant influences are essential in the construction of a framework that can guide the promotion of brand loyalty. The aim of this study was to identify the influences that are most important in creating and measuring brand loyalty in the fast moving consumer goods (FMCG) sector. The study builds a conceptual framework using the identified influences and also presents the interrelationships between the influences. The primary theoretical background and concepts in brand loyalty for this study ranged from the history of branding to the results of brand loyalty studies conducted over the past five years. The extensive review of literature and previously tested brand loyalty models resulted in the identification of 12 influences that impact directly on brand loyalty. Reducing the identified set of influences into a manageable set for this thesis involved selecting the most commonly used reliable and valid brand loyalty influences. The empirical study which followed was conducted among a sample of 550 customers who had access to a wide range of FMCG. The empirical study based on the selected 12 brand loyalty influences yielded results that measured the strength of each influence and the interrelationship of influences. The results were analysed by the process of factor analysis, and were presented in the form of a conceptual framework that could be applied in the FMCG segment to measure the strength of brand loyalty influences and determine if the same influences apply to all FMCG. The results of the study confirmed that different influences have different effects on brand loyalty in the FMCG segment. The study revealed that the psychological influences such as brand commitment, brand affect, perceived value and relationship proneness had a far stronger effect on brand loyalty than the brand performance influences such as customer satisfaction or brand performance. Furthermore, the study found an extremely close relationship between influences as far as the specific products were concerned. This study confirmed that FMCG could all be treated as a single entity when evaluating the influences of brand loyalty. The uniqueness and value of the study lies in the evaluation of each brand loyalty influence that is collectively assembled in one framework. The most important contribution of the study is therefore the construction of this conceptual framework through which brand loyalty could be measured and strategically managed. / Thesis (Ph.D. (Business Administration))--North-West University, Potchefstroom Campus, 2011.

An important issue in software evolution is the time and effort needed to understand existing applications. Reverse engineering software to recover behavioural models is difficult and is complicated due to the lack of a standardized way of extracting and visualizing knowledge. In this thesis, we study a technique for automatically extracting static and dynamic data from software, filtering and analysing the data, and visualizing the behavioural model of a selected feature of a software application. We also investigate the usefulness of the generated diagrams as documentation for the software. We present a literature review of studies that have used static and dynamic data analysis for software comprehension. A set of criteria is created, and each approach, including this thesis’ technique, is compared using those criteria. We propose an approach to simplify lengthy traces by filtering out software components that are too low level to give a high-level picture of the selected feature. We use static information to identify and remove small and simple (or uncomplicated) software components from the trace. We define a utility method as any element of a program designed for the convenience of the designer and implementer and intended to be accessed from multiple places within a certain scope of the program. Utilityhood is defined as the extent to which a particular method can be considered a utility. Utilityhood is calculated using different combinations of selected dynamic and static variables. Methods with high utilityhood values are detected and removed iteratively. By eliminating utilities, we are left with a much smaller trace which is then visualized using the Use Case Map (UCM) notation. UCM is a scenario language used to specify and explain behaviour of complex systems. By doing so, we can identify the algorithm that generates a UCM closest to the mental model of the designers. Although when analysing our results we did not identify an algorithm that was best in all cases, there is a trend in that three of the best four algorithms (out of a total of eight algorithms investigated) used method complexity and method lines of code in their parameters. We also validated the algorithm results by doing a comparison with a list of methods given to us by the creators of the software and doing precision and recall calculations. Seven out of the eight participants agreed or strongly agreed that using UCM diagrams to visualize reduced traces is valid approach, with none who disagreed.

Since the emergence of branding as an approach to marketing, the concept has been received with a great deal of interest and has stimulated ever increasing research in the area. Businesses have realized the importance of retaining existing customers and have begun to identify and apply ways to build long-term relationships with customers. These relationships with customers require an understanding of customer needs, business requirements and the influences that create a long-term relation which is more commonly known as brand loyalty. Several research studies including this one present the results of brand loyalty research in the form of a conceptual framework. From an academic viewpoint, the identification and application of all the relevant influences are essential in the construction of a framework that can guide the promotion of brand loyalty. The aim of this study was to identify the influences that are most important in creating and measuring brand loyalty in the fast moving consumer goods (FMCG) sector. The study builds a conceptual framework using the identified influences and also presents the interrelationships between the influences. The primary theoretical background and concepts in brand loyalty for this study ranged from the history of branding to the results of brand loyalty studies conducted over the past five years. The extensive review of literature and previously tested brand loyalty models resulted in the identification of 12 influences that impact directly on brand loyalty. Reducing the identified set of influences into a manageable set for this thesis involved selecting the most commonly used reliable and valid brand loyalty influences. The empirical study which followed was conducted among a sample of 550 customers who had access to a wide range of FMCG. The empirical study based on the selected 12 brand loyalty influences yielded results that measured the strength of each influence and the interrelationship of influences. The results were analysed by the process of factor analysis, and were presented in the form of a conceptual framework that could be applied in the FMCG segment to measure the strength of brand loyalty influences and determine if the same influences apply to all FMCG. The results of the study confirmed that different influences have different effects on brand loyalty in the FMCG segment. The study revealed that the psychological influences such as brand commitment, brand affect, perceived value and relationship proneness had a far stronger effect on brand loyalty than the brand performance influences such as customer satisfaction or brand performance. Furthermore, the study found an extremely close relationship between influences as far as the specific products were concerned. This study confirmed that FMCG could all be treated as a single entity when evaluating the influences of brand loyalty. The uniqueness and value of the study lies in the evaluation of each brand loyalty influence that is collectively assembled in one framework. The most important contribution of the study is therefore the construction of this conceptual framework through which brand loyalty could be measured and strategically managed. / Thesis (Ph.D. (Business Administration))--North-West University, Potchefstroom Campus, 2011.

An important issue in software evolution is the time and effort needed to understand existing applications. Reverse engineering software to recover behavioural models is difficult and is complicated due to the lack of a standardized way of extracting and visualizing knowledge. In this thesis, we study a technique for automatically extracting static and dynamic data from software, filtering and analysing the data, and visualizing the behavioural model of a selected feature of a software application. We also investigate the usefulness of the generated diagrams as documentation for the software. We present a literature review of studies that have used static and dynamic data analysis for software comprehension. A set of criteria is created, and each approach, including this thesis’ technique, is compared using those criteria. We propose an approach to simplify lengthy traces by filtering out software components that are too low level to give a high-level picture of the selected feature. We use static information to identify and remove small and simple (or uncomplicated) software components from the trace. We define a utility method as any element of a program designed for the convenience of the designer and implementer and intended to be accessed from multiple places within a certain scope of the program. Utilityhood is defined as the extent to which a particular method can be considered a utility. Utilityhood is calculated using different combinations of selected dynamic and static variables. Methods with high utilityhood values are detected and removed iteratively. By eliminating utilities, we are left with a much smaller trace which is then visualized using the Use Case Map (UCM) notation. UCM is a scenario language used to specify and explain behaviour of complex systems. By doing so, we can identify the algorithm that generates a UCM closest to the mental model of the designers. Although when analysing our results we did not identify an algorithm that was best in all cases, there is a trend in that three of the best four algorithms (out of a total of eight algorithms investigated) used method complexity and method lines of code in their parameters. We also validated the algorithm results by doing a comparison with a list of methods given to us by the creators of the software and doing precision and recall calculations. Seven out of the eight participants agreed or strongly agreed that using UCM diagrams to visualize reduced traces is valid approach, with none who disagreed.

Submitted by PPG Ci?ncia da Computa??o (ppgcc@pucrs.br) on 2017-11-13T21:43:46Z No. of bitstreams: 1 AMYR_BORGES_FORTES_NETO_TES.pdf: 2509779 bytes, checksum: 3513c7b9db941d3f24cfdc672eac46f9 (MD5) / Rejected by Caroline Xavier (caroline.xavier@pucrs.br), reason: Devolvido devido ? falta da folha de rosto (p?gina com as principais informa??es) no arquivo PDF, passando direto da capa para a ficha catalogr?fica. on 2017-11-21T12:48:40Z (GMT) / Submitted by PPG Ci?ncia da Computa??o (ppgcc@pucrs.br) on 2017-12-11T16:15:52Z No. of bitstreams: 1 AMYR_BORGES_FORTES_NETO_TES.pdf: 2507882 bytes, checksum: 0ef0935814ab8c8fd102985b55b443f6 (MD5) / Approved for entry into archive by Caroline Xavier (caroline.xavier@pucrs.br) on 2017-12-18T13:19:03Z (GMT) No. of bitstreams: 1 AMYR_BORGES_FORTES_NETO_TES.pdf: 2507882 bytes, checksum: 0ef0935814ab8c8fd102985b55b443f6 (MD5) / Made available in DSpace on 2017-12-18T13:24:43Z (GMT). No. of bitstreams: 1 AMYR_BORGES_FORTES_NETO_TES.pdf: 2507882 bytes, checksum: 0ef0935814ab8c8fd102985b55b443f6 (MD5) Previous issue date: 2017-03-09 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior - CAPES / Modelos de simula??o de multid?es t?m tido um papel importante em ci?ncias da computa??o j? h? algumas d?cadas desde os trabalhos pioneiros. No in?cio, agentes simulados em multid?es comportavam-se todos da mesma maneira, e tal comportamento era controlado pelas mesmas regras em todos os agentes. Com o tempo, os modelos de simula??o evoluiram, e come?aram a agregar uma maior variedade de comportamentos nos agentes. Modelos de simula??o de multid?es que implementam diferentes comportamentos nos agentes s?o chamados modelos de Multid?es Heterog?neas, em oposi??o aos modelos de Multid?es Homog?neas precedentes. Modelos de simula??o de multid?es que buscam criar agentes com comportamentos humanos realistas exploram heterogeneidade nos comportamentos dos agentes, na tentativa de atingir tal realismo. Em geral, estudos em psicologia e comportamento humano s?o usados como conhecimento de base, e os comportamentos observados nestes estudos s?o simulados em agentes virtuais. Nesta dire??o, trabalhos recentes em simula??o de multid?es exploram caracter?sticas de personalidade e modelos de emo??es. No campo de emo??es em agentes virtuais, pesquisadores est?o tentando recriar fen?menos de cont?gio de emo??es em pequenos grupos de agentes, ou mesmo estudar o impacto de cont?gio de emo??o entre agentes virtuais e participantes humanos. Sob a cren?a de que cont?gio de emo??o em agentes virtuais possa levar a comportamentos mais realistas em multi?es, este trabalho foca em recriar modelos computacionais de cont?gio de emo??es destinados a pequenos grupos de agentes, adaptando estes modelos para um contexto de simula??o de multid?es. / Crowd simulation models have been playing an important role in computer sciences for a few decades now, since pioneer works. At the beginning, agents simulated on crowds behaved all the same way, such behaviour being controlled by the same set of rules. In time, simulation models evolved and began to incorporate greater variety of behaviours. Crowd simulation models that implement different agent behaviours are so-called Heterogeneous Crowd models, opposing to former Homogeneous Crowd models. Advances in crowd simulation models that attempt to make agents with more realistic human-like behaviours explore heterogeneity of agent behaviours in order to achieve overall simulation realism. In general, human behavioural and psychological studies are used as base of knowledge to simulate observed human behaviours within virtual agents. Toward this direction, later crowd simulation works explore personality traits and emotion models. Some other work in the field of emotional virtual agents, researchers are attempting to recreate emotion contagion phenomena in small groups of agents, and even studying emotion contagion impact between virtual agents and human participants. Under the belief that emotion contagion in virtual agents might lead to more realistic behaviours on crowds, this work is focused on recreating emotion contagion computational models designed for small groups of agents, and adapting it for crowd simulation context.

This thesis deals with human – pilot behaviour modelling during a flight in terms of automatic control systems. For these purposes, the introduction to the issue of description and modelling of individual components of the whole pilot – aircraft interaction is presented. Based on that, the simulation models obtained from real measured data are designed. However, the acquisition of the real flight data is quite difficult. Therefore, the flight simulator at Brno University of Defence is used for the purposes of this work. Several experimental measurements were taken using this simulator. These were focused on measuring pilot’s reactions (responses) to visual stimulus with emphasis on obtaining judgements about their current state of training (in terms of dynamic behaviour) as well as attitude to aircraft control. In this phase, two sets of measurements with eight pilots were taken. On average, the pilots had 60 flight hours before the first set of measurements and about 80 flight hours before the second set. The obtained results are analysed using mainly the theory of automatic control approaches in order to evaluate the actual state of pilots’ abilities considering the effects of flight training.