151 |
Software product and process quality improvement using formal methodsMishra, Satish 04 June 2015 (has links)
Die erweiterte CSP-CASL Syntax wird dazu verwendet, sowohl positive als auch negative Testfälle zu generieren. Auf diese Weise wird sichergestellt, dass erwartetes und unerwünschtes Verhalten in den Testfäallen enthalten ist. Ferner werden Testterminologien für die CSP-CASL Spezifikation beschrieben, welche Softwareverfeinerungen und Erweiterungen untersuchen. Anschliessend wird die formale Definition von Softwareeigenschaften verwendet, um die Wiederverwendbarkeit von Testbestandteilen zu überprüfen. Diese Definitionen beschreiben die grundlegenden Eigenschaften im vorgeschlagenen Produkt und Prozessqualitäts- Framework. Ferner wird die Möglichkeit untersucht, die vorgeschlagenen Formalismus für die Entwicklung eines CMMI Prozesskonformen Frameworks zu verwenden. Dabei werden die Kernaspekte des CMMI Prozessmodells berücksichtigt. Das CMMI Compliance Bewertungssystem wurde entwickelt, um den Grad der Konformit ät der eingesetzten Softwareentwicklungsmethoden mit formalen Methoden zu bewerten. Ein generischer Algorithmus wird vorgeschlagen, um das Compliance Level der CMMI Prozessfelder und ihrer Komponenten zu ermitteln. Das Framework wird durch ein Tool unterstützt. Dieses Tool erlaubt es, die theoretischen Aspekte der vorgeschlagenen Theoreme praktisch zu unterstützen. Die Verwendbarkeit des vorgeschlagenen Frameworks wird an einem Anwendungsbeispiel aus der Medizintechnik gezeigt. Im Rahmen dieser Arbeit wird das Verständnis der Anwendung von formalen Methoden auf das Organisatorische Prozessmodell CMMI erweitert. Das komplette Framework wird repräsentiert durch die formale Spezifikationssprache CSP- CASL sowie der Prozessmodell CMMI. Ähnliche Ergebnisse können auch mit anderen formalen Methoden und Prozessverbesserungsmodellen erzielt werden. Diese Forschungsarbeit dagegen bildet einen Startpunkt für eine Prozessmodellkonformit ät mit einen auf formalen Methoden basierenden Softwaresystems sowie deren Entwicklung und Wartung. / The proposed formalisms and the other properties of formal methods are used to propose a framework of CMMI process model compliance. The core aspects of the CMMI process model are the process areas. A process area is a collection of best practices in a selected area. The CMMI compliance grading scheme is developed to evaluate the level of compliance with formal method based software development. A compliance algorithm is proposed to evaluate the process model through the evaluation of its components. The CMMI process areas are evaluated with a proposed algorithm. The compliance evaluation result is presented in the thesis. The complete framework is supported with a developed tool. This tool allows us to practically support our theoretical concepts. As a proof of concept, we explore our proposed framework for a medical instrument development and maintenance. In this thesis, the understanding of formal methods applicability is extended to the organizational process model, CMMI. The complete framework is presented for a formal specification language, CSP-CASL and process model, CMMI. However, similar result can be achieved with other formal methods for the compliance of other process models. This research is a starting point of process model compliance with formal methods. This has significant potential to automate the achievement of process and product quality goals of software systems.
|
152 |
Um método de refinamento para desenvolvimento de software embarcado: uma abordagem baseada em UML-RT e especificações formais. / A refinement method for embedded software development: a based UML-RT and formal specification approach.Polido, Marcelo Figueiredo 18 May 2007 (has links)
Neste trabalho é apresentado um método de refinamento para especificações de sistemas embarcados, baseado na linguagem de especificação gráfica UML-RT e na linguagem de especificação formal CSP-OZ. A linguagem UML-RT é utilizada para descrever a arquitetura de sistemas de tempo real distribuídos e esses mapeados para uma especificação formal através de CSP-OZ. A linguagem de especificação formal CSP-OZ é a combinação da linguagem orientada a objetos Object-Z e a algebra de processos CSP, que descreve o comportamento de processos concorrentes. O método de refinamento proposto é baseado na integração de dois métodos: o de bi-simulação, para refinar a parte comportamental da especificação descrita por CSP; e o de equivalência de especificações, para refinar as estruturas de dados descritas por Object-Z, permitindo assim que características de orientação a objetos possam ser utilizadas. Com o método proposto é possível refinar especificações e, conseqüentemente, verificá-las com sua implementação. O desenvolvimento desse método é rigoroso, incluindo a definição formal para um metamodelo da UML-RT. Um exemplo detalhado é apresentado no final deste trabalho. / In this work, a method of refinement of embedded systems specifications based on the graphical specification language UML-RT and the formal specification CSP-OZ is introduced. The UML-RT is used to model real time distributed architecture systems and these are mapped onto formal specifications using CSP-OZ. The CSP-OZ formal specification language is a combination of the state-based object oriented language Object-Z and the CSP process algebra that describes behavioral models of concurrent processes. The rationale of the proposed refinement method is twofold, the use of bisimulation to refine the behavioral part and the specification matching algorithm to refine the state-based part, supporting object-oriented characteristics. Using this result, an equivalence between the specification-matching algorithm and simulation rules is showed. Using the proposed method it is possible to refine CSP-OZ specifications and verify them against their implementations. The development of the proposed refinement method is rigorous, including a formal definition for a UML-RT metamodel. A detailed study case is given at the end of this work.
|
153 |
Um método de refinamento para desenvolvimento de software embarcado: uma abordagem baseada em UML-RT e especificações formais. / A refinement method for embedded software development: a based UML-RT and formal specification approach.Marcelo Figueiredo Polido 18 May 2007 (has links)
Neste trabalho é apresentado um método de refinamento para especificações de sistemas embarcados, baseado na linguagem de especificação gráfica UML-RT e na linguagem de especificação formal CSP-OZ. A linguagem UML-RT é utilizada para descrever a arquitetura de sistemas de tempo real distribuídos e esses mapeados para uma especificação formal através de CSP-OZ. A linguagem de especificação formal CSP-OZ é a combinação da linguagem orientada a objetos Object-Z e a algebra de processos CSP, que descreve o comportamento de processos concorrentes. O método de refinamento proposto é baseado na integração de dois métodos: o de bi-simulação, para refinar a parte comportamental da especificação descrita por CSP; e o de equivalência de especificações, para refinar as estruturas de dados descritas por Object-Z, permitindo assim que características de orientação a objetos possam ser utilizadas. Com o método proposto é possível refinar especificações e, conseqüentemente, verificá-las com sua implementação. O desenvolvimento desse método é rigoroso, incluindo a definição formal para um metamodelo da UML-RT. Um exemplo detalhado é apresentado no final deste trabalho. / In this work, a method of refinement of embedded systems specifications based on the graphical specification language UML-RT and the formal specification CSP-OZ is introduced. The UML-RT is used to model real time distributed architecture systems and these are mapped onto formal specifications using CSP-OZ. The CSP-OZ formal specification language is a combination of the state-based object oriented language Object-Z and the CSP process algebra that describes behavioral models of concurrent processes. The rationale of the proposed refinement method is twofold, the use of bisimulation to refine the behavioral part and the specification matching algorithm to refine the state-based part, supporting object-oriented characteristics. Using this result, an equivalence between the specification-matching algorithm and simulation rules is showed. Using the proposed method it is possible to refine CSP-OZ specifications and verify them against their implementations. The development of the proposed refinement method is rigorous, including a formal definition for a UML-RT metamodel. A detailed study case is given at the end of this work.
|
154 |
Styrelsens könsfördelning och dess effekt på företagets hållbarhetsprestation : en kvantitativ studie om förhållandet mellan BGD och CSP hos europeiska bolag / The board’s gender distribution and its effect on the company’s sustainability performance : a quantitative study about the relationship between BGD and CSP in European companiesAlfredsson, Pierre, Wikström, Linnéa January 2019 (has links)
Syfte: Studien genomförs i syfte att undersöka om det finns ett samband mellan BGD (Board Gender Diversity) och total CSP (Corporate Social Performance) samt mellan BGD och miljödimensionen respektive den sociala dimensionen. Metod: I studien antas en positivistisk forskningsfilosofi med hypotetiskt-deduktiv ansats. Två urval med olika bolagssystem undersöks. Totalt undersöks 403 europeiska bolag. 121 bolag med dualistiskt bolagssystem och 282 bolag med monistiskt bolagssystem. Studiens kvantitativa forskningsstrategi formas utifrån en longitudinell design vilken implementerats mellan åren 2008-2017. All data samlades in via Thomson Reuters Datastream och analyserades sedan i SPSS. Resultat & slutsats: Studien finner ett signifikant positivt samband mellan BGD och total CSP samt mellan BGD och miljödimensionen respektive den sociala dimensionen. Företag med högre BGD tycks ha större benägenhet att investera i CSR. hållbarhetsprestation. Sambandet påvisas inom såväl det dualistiska som det monistiska bolagssystemet. BGD:s påverkanseffekt är dock starkare inom det monistiska bolagssystemet. Examensarbetets bidrag: Med studien erhålls ny kunskap om relationen mellan BGD och total CSP samt mellan BGD och miljödimensionen samt den sociala dimensionen. Studien är bland de första att göra en jämförelse mellan det dualistiska och det monistiska bolagssystemet. Resultatet är relevant med hänsyn till att det ställs allt högre krav på företag att agera hållbart samt den pågående debatten om huruvida EU bör införa obligatorisk könskvotering i styrelser. Förslag till fortsatt forskning: Ytterligare forskning på land- och branschnivå behövs då sambandet kan skilja sig åt mellan de olika länderna och branscherna, och således påverka logiken bakom obligatorisk könskvotering. Framtida forskning föreslås även inkludera det tredje bolagssystemet, mixed board structure. Vidare ges förslaget att titta närmre på företagsrisken och dess betydelse inom olika bolagssystem, dels med avseende på företagens hållbarhetsprestation, men även med avseende på BGD. Slutligen föreslås framtida forskning undersöka de enskilda CSP-dimensionerna närmre i syfte att utröna vad som kan ligga bakom BGD:s större inverkan på den sociala dimensionen. / Aim: The study is carried out in order to investigate whether there is a link between BGD (Board Gender Diversity) and total CSP (Corporate Social Performance) as well as between BGD and the environmental and social dimension respectively. Method: In this study we adopt a positivist research philosophy with a hypothetical-deductive approach. Two samples with different board systems are studied. 403 European companies in total are studied. 121 companies with a two-tier board system and 282 companies with a one-tier board system. The quantitative research strategy is based on a longitudinal design implemented between 2008-2017. All data was collected through Thomson Reuters Datastream and then analyzed using SPSS. Result & Conclusions: The study finds a significant positive relationship between BGD and total CSP as well as between BGD and the environmental dimension and the social dimension respectively. Companies with higher BGD seems to be more likely to invest in CSR. The relationship is found within the two-tier board system as well as the one-tier board system. However, the impact of BGD is stronger within the one-tier board system. Contribution of the thesis: The study provides new knowledge about the relationship between BGD and total CSP as well as between BGD and the environmental dimension and the social dimension. The study is among the first to make a comparison between the two-tier board system and the one-tier board system. The result is relevant in view of the increasing demands on companies to act sustainably as well as the ongoing debate on whether the EU should introduce mandatory gender quotas on boards. Suggestions for future research: Further research at country and industry level is needed as the relationship may differ between different countries and industries, thus affecting the logic behind mandatory gender quotas. Future research is also proposed to include the third board system, mixed board structure. Furthermore, the proposal to look more closely at the corporate risk and its importance within various board systems, partly with regard to the companies’ sustainability performance, but also with regard to BGD, is given. Finally, it is proposed that future research could investigate the individual CSP dimensions more closely in order to determine what may be behind BGDs greater impact on the social dimension.
|
155 |
Sambandet mellan Corporate Social Performance och finansiell risk : - En kvantitativ studie som undersöker nordiska företag / The relationship between Corporate Social Performance and Financial Risk : A quantitative study that examines Nordic companiesJohannesson, Gustav, Westport, Martin January 2018 (has links)
Examensarbete, Civilekonomprogrammet, Ekonomihögskolan vid Linnéuniversitetet Författare: Gustav Johannesson och Martin Westport Handledare: Andreas Stephan Medbedömare: Anna Stafsudd Titel: Sambandet mellan Corporate Social Performance och finansiell risk - En kvantitativ studie som undersöker nordiska företag Bakgrund: Företags sociala ansvar har ständigt funnits på företagsagendan under senaste åren efter ökade globala utmaningar och större påtryckningar från intressenter. Man kan se allt större risker som är kopplade till företags hållbarhetsarbete. Med bakgrund till detta finns det ett stort intresse och en uppåtgående trend kring hållbara investeringar där Norden är ledande inom området. Syfte: Studiens syfte är att förklara sambandet mellan Corporate Social Performance, både på en sammanslagen och individuell nivå, och finansiell risk. Metod: Genom den deduktiva forskningsansatsen och den kvantitativa forskningsstrategin som är baserad på paneldata testar författarna sina hypoteser. Författarna bygger sina hypoteser på intressentteorin och riskhanteringsteorin som testas med ett nordiskt urval på 144 företag under tidsperioden 2002-2016. Slutsats: Studiens resultat visar att det finns ett negativt samband mellan Corporate Social Performance och finansiell risk. Det finns även ett negativt samband mellan företags sociala prestationer och finansiell risk. Detta är i linje med författarnas förväntningar. Däremot visar resultatet inga samband mellan företags miljömässiga och styrningsmässiga prestationer och deras finansiella risk. / Degree Project, The Business Administration and Economics Programme, School of Business and Economics at Linnaeus University Authors: Gustav Johannesson and Martin Westport Supervisor: Andreas Stephan Co-assessor: Anna Stafsudd Title: The relationship between Corporate Social Performance and Financial Risk - A quantitative study that examines Nordic companies Background: Corporate Social Responsibility has been on the corporate agenda in recent years following increased global challenges and greater pressure from stakeholders. One can see more risks associated with corporate sustainability. This has led to a great interest globally and an upward trend in Socially Responsible Investing where the Nordic region is at the leading edge. Purpose: The purpose of the study is to explain the relationship between Corporate Social Performance, both at a combined and an individual level, and financial risk. Method: Through the deductive research approach and the quantitative research strategy that is based on panel data, the authors test their hypotheses. The authors base their hypotheses on stakeholder theory and risk management theory and test them with a Nordic sample of 144 companies over the period 2002-2016. Conclusion: The study results show that there is a negative relationship between Corporate Social Performance and financial risk. There is also a negative relationship between social performance and financial risk. This is in line with the authors’ expectations. However, the results show no relationship between companies’ environmental and governance performance and their financial risk.
|
156 |
Optimisation de l’architecture de systèmes embarqués par une approche basée modèle / Architecture Optimization of Embedded Systems with a Model Based ApproachLeserf, Patrick 02 May 2017 (has links)
L’analyse de compromis d’un modèle système a pour but de minimiser ou de maximiser différents objectifs tels que le coût ou les performances. Les méthodes actuelles de type OOSEM avec SysML ou ARCADIA sont basées sur la classification ; il s’agit de définir les différentes variantes de l’architecture d’un système de base puis d’analyser ces variantes. Dans ces approches, les choix d’architecture sont contraints : la plateforme d’exécution et la topologie sont déjà figées. Nous proposons la notion de « points de décision » pour modéliser les différents choix du système, en utilisant de nouveaux stéréotypes. L’avantage est d’avoir une modélisation plus « compacte » des différentes variantes et de piloter l’exploration des variantes en utilisant des contraintes. Lorsque le concepteur définit l’architecture du système, des points de décisions sont insérés dans le modèle du système. Ils permettent de modéliser la redondance ou le choix d’une instance pour un composant, les variations des attributs d’un composant, ou l’allocation des activités sur les blocs. Les fonctions objectifs sont définies dans un contexte d’optimisation à l’aide du diagramme paramétrique de SysML. Nous proposons des transformations du modèle SysML vers un problème de satisfaction de contraintes pour l’optimisation (CSMOP) dont la résolution nous permet d’obtenir l’ensemble des architectures optimales. Cette transformation est implantée dans un démonstrateur (plug-in Eclipse) permettant une utilisation conjointe de l’outil Papyrus et de solveurs, disponibles sous forme de logiciels libres. La méthode est illustrée avec des cas d’étude constitués d’une caméra stéréoscopique puis d’un drone, l’ensemble étant modélisé avec Papyrus. / Finding the set of optimal architectures is an important challenge for the designer who uses the Model-Based System Engineering (MBSE). Design objectives such as cost, performance are often conflicting. Current methods (OOSEM with SysML or ARCADIA) are focused on the design and the analysis of a particular alternative of the system. In these methods, the topology and the execution platform are frozen before the optimization. To improve the optimization from MBSE, we propose a methodology combining SysML with the concept of “decision point”. An initial SysML model is complemented with “decisions points” to show up the different alternatives for component redundancy, instance selection and allocation. The constraints and objective functions are also added to the initial SysML model, with an optimiza-tion context and parametric diagram. Then a representation of a constraint satisfaction problem for optimization (CSMOP) is generated with an algorithm and solved with an existing solver. A demonstrator implements this transformation in an Eclipse plug-in, combining the Papyrus open-source tool and CSP solvers. Two case studies illustrate the methodology: a stereoscopic camera sensor module and a mission controller for an Unmanned Aerial Vehi-cle (UAV).
|
157 |
Är hållbarhet lönsamt? : En undersökning av cirkulära orsakssamband mellan hållbarhetsprestationer och lönsamhet / Is sustainability profitable? : An examination of circular causation between sustainability performance and profitability.Olofsson, Jenny, Lundell, Clara January 2018 (has links)
Titel: Är hållbarhet lönsamt? – En undersökning av cirkulära orsakssamband mellan hållbarhetsprestationer och lönsamhet Nivå: Examensarbete på Grundnivå (kandidatexamen) i ämnet företagsekonomi Författare: Clara Lundell och Jenny Olofsson Handledare: Jan Svanberg Datum: 2018 – januari Syfte: Hundratals forskare har studerat om ett företags engagemang i Corporate Social Responsibility (CSR) har positiv inverkan på dess lönsamhet, den finansiella prestationen (FP). CSR är inget kvantitativt mått och därför används begreppet Corporate Social Performance (CSP). De tidigare studierna har resulterat i varierande utfall och för att tydliggöra relationen mellan CSP och FP har ett fåtal forskare även undersökt FP:s effekt på CSP, vilket genererar en dubbelriktad relation. För att en gång för alla kunna förklara relationen mellan CSP och FP samt urskilja existensen av eventuellt dubbelriktade relationer mellan dem har vi delat in CSP i de tre dimensionerna miljö, den sociala dimensionen och företagsstyrning. Vi undersöker sedan om det existerar en god cirkel mellan dessa dimensioner och FP. Metod: Studien antar en positivistisk forskningsfilosofi med en hypotetisk-deduktiv ansats. Tidsperspektivet består av en longitudinell design som genomförts med data över tio år på 546 bolag över hela världen. Studien är enbart baserad på data av sekundär art och variablernas information har inhämtats från databasen Thomson Reuters Datastream. Datan har analyserats i de två statistikprogrammen SPSS och Stata. Resultat & slutsats: Resultatet ger bevis för att det existerar en positiv dubbelriktad relation mellan total CSP och FP samt mellan CSP-dimensionen företagsstyrning och FP. Företag som har en hög nivå av FP väljer att spendera mer på CSP, CSP-investeringar som i sin tur genererar högre nivå av FP, det existerar en god cirkel. CSP-dimensionen miljö och den sociala CSP-dimensionen visar negativa dubbelriktade relationer med FP. Examensarbetets bidrag: Studien ger bevis för att den positiva cirkeln mellan total CSP och FP tycks erhållas enbart genom CSP-dimensionen företagsstyrning. De andra två CSP-dimensionerna genererar negativa dubbelriktade relationer. Resultatet bidrar med värdefull teoretisk information avseende varför tidigare studier visat olika resultat för relationen mellan CSP och FP, men också praktiska bevis för hur CSP ska implementeras för att bli lönsam. Förslag till fortsatt forskning: Ett förslag till fortsatt forskning är att använda förmedlande variabler för att urskilja orsakssamband, att det verkligen är ökade CSP-aktiviteter som leder till ökat FP. Eftersom studien inte kan generaliseras till mindre bolag är ett andra förslag till framtida forskning att genomföra en liknande studie på sådana bolag. Vidare föreslår vi att en liknande studie genomförs men med en tidsförskjutning mellan variablerna för CSP-dimensionerna och FP för att se om ett annat resultat erhålls. / Title: Is sustainability profitable? – An examination of circular causation between sustainability performance and profitability. Level: Student thesis, final assignment for Bachelor Degree in Business Administration Author: Clara Lundell and Jenny Olofsson Supervisor: Jan Svanberg Date: 2018 – january Aim: Hundreds of scientists have studied companies commitment in Corporate Social Responsibility (CSR), if it has any positive effect on its profitability, the financial performance (FP). CSR is not a quantitative measure, and therefore the term Corporate Social Performance (CSP) is used. Previous studies have varying outcomes and to clarify the relationship between CSP and FP, a few researchers have also investigated FPs effect on CSP, which generates a bidirectional relationship between them. To explain the relationship between CSP and FP once and for all and to distinguish the existence of potentially bidirectional relationships between them, we have divided CSP into the three dimensions of environment, the social dimension and corporate governance. We then examine if a good circle between these dimensions and FP exists. Method: The study assumes a positivistic research philosophy with a hypothetical-deductible approach. The time perspective consists of a longitudinal design, implemented with ten-year data of 546 companies worldwide. The study is only based on data of secondary art and the variables information have been collected from the database Thomson Reuters Datastream. The data have been analyzed in two statistical programmes called SPSS and Stata. Result & Conclusions: The result gives evidence that positive bidirectional relationships between total CSP and FP, and CSP for corporate governance and FP, exists. Companies whom have a high level of FP choose to spend more money on CSP, CSP-investments in turn generates higher levels of FP, a good circle exists. The CSP dimension environment and the social CSP dimension show negative bidirectional relationships with FP. Contribution of the thesis: The study that we have done gives evidence that the entire positive circle between the total measure of CSP and FP appears to be obtained only through the CSP dimension corporate governance. This is when the other two CSP dimensions generated negative bidirectional relationships. The result gives valuable theoretical information as to why earlier studies have different results for the relationship between CSP and FP, but also practical evidence of how CSP should be implemented to become profitable. Suggestions for further research: One suggestion for further research is to use intermediary variables to separate causation and that it really is the increased CSP-activities that leads to increased FP. The study cannot be generalized to smaller companies, therefore a second proposal for future research is to do a similar study but on data obtained from these. Furthermore, we suggest that a similar study is made with a time-lag between the CSP dimensions and FP to see if it shows different results.
|
158 |
Stratégies de génération de tests à partir de modèles UML/OCL interprétés en logique du premier ordre et système de contraintes. / Test generation strategies from UML/OCL models interpreted with first order logic constraints systemCantenot, Jérôme 13 November 2013 (has links)
Les travaux présentés dans cette thèse proposent une méthode de génération automatique de tests à partir de modèles.Cette méthode emploie deux langages de modélisations UML4MBT et OCL4MBT qui ont été spécifiquement dérivées d’ UML et OCL pour la génération de tests. Ainsi les comportements, la structure et l’état initial du système sont décrits au travers des diagrammes de classes, d’objets et d’états-transitions.Pour générer des tests, l’évolution du modèle est représente sous la forme d’un système de transitions. Ainsi la construction de tests est équivalente à la découverte de séquences de transitions qui relient l’´état initial du système à des états validant les cibles de test.Ces séquences sont obtenues par la résolution de scénarios d’animations par des prouveurs SMT et solveurs CSP. Pour créer ces scénarios, des méta-modèles UML4MBT et CSP4MBT regroupant formules logiques et notions liées aux tests ont été établies pour chacun des outils.Afin d’optimiser les temps de générations, des stratégies ont été développé pour sélectionner et hiérarchiser les scénarios à résoudre. Ces stratégies s’appuient sur la parallélisation, les propriétés des solveurs et des prouveurs et les caractéristiques de nos encodages pour optimiser les performances. 5 stratégies emploient uniquement un prouveur et 2 stratégies reposent sur une collaboration du prouveur avec un solveur.Finalement l’intérêt de cette nouvelle méthode à été validée sur des cas d’études grâce à l’implémentation réalisée. / This thesis describes an automatic test generation process from models.This process uses two modelling languages, UML4MBT and OCL4MBT, created specificallyfor tests generation. Theses languages are derived from UML and OCL. Therefore the behaviours,the structure and the initial state of the system are described by the class diagram, the objectdiagram and the state-chart.To generate tests, the evolution of the model is encoded with a transition system. Consequently,to construct a test is to find transition sequences that rely the initial state of the system to thestates described by the test targets.The sequence are obtained by the resolution of animation scenarios. This resolution is executedby SMT provers and CSP solvers. To create the scenario, two dedicated meta-models, UML4MBTand CSP4MBT have been established. Theses meta-models associate first order logic formulas withthe test notions.7 strategies have been developed to improve the tests generation time. A strategy is responsiblefor the selection and the prioritization of the scenarios. A strategy is built upon the properties ofthe solvers and provers and the specification of our encoding process. Moreover the process canalso be paralleled to get better performance. 5 strategies employ only a prover and 2 make theprover collaborate with a solver.Finally the interest of this process has been evaluated through a list of benchmark on variouscases studies.
|
159 |
Constructive extensibility of trust worthy component-based systemsOLIVEIRA, José Dihego da Silva 04 March 2016 (has links)
Submitted by Fabio Sobreira Campos da Costa (fabio.sobreira@ufpe.br) on 2017-07-12T14:15:46Z
No. of bitstreams: 2
license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5)
TESE_JOSE_DIHEGO_DA_SILVA_OLIVEIRA_CIN_UFPE_2016.pdf: 1113539 bytes, checksum: 124effe0f62c8dd44008517c1e0045ee (MD5) / Made available in DSpace on 2017-07-12T14:15:46Z (GMT). No. of bitstreams: 2
license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5)
TESE_JOSE_DIHEGO_DA_SILVA_OLIVEIRA_CIN_UFPE_2016.pdf: 1113539 bytes, checksum: 124effe0f62c8dd44008517c1e0045ee (MD5)
Previous issue date: 2016-03-04 / As computer systems become ubiquitous, the demand for rigorous and compositional development methods increase dramatically. In the component-based model driven development (CB-MDD) approach, complex systems (sometimes intractable by humans) are build from simple elements, called components. To achieve the CB-MDD goals towards becoming a rigorously development discipline, components and composition rules must be formalised. Moreover, as requirements continuously evolve, there must be mechanisms to refine and safely extend component-based systems. The BRIC component model formalises the CB-MDD core concepts and supports a constructive design based on composition rules that preserves behavioural properties, but do not provide support for component model evolution. In this work we propose inheritance and refinement relations for BRIC. We define a congruent semantics for this model that considers component structure and behaviour. We define refinement as a preorder relation, which is monotonic with respect to the BRIC composition rules. We enhance this component model with support for extensibility via inheritance. The proposed relations allow extension of functionality, whilst preserving service conformance, which we define by means of a convergence notion. We also establish an algebraic connection between component extensibility and refinement. As far as we are aware this is the first time componente inheritance relations are developed for a formal and sound CB-MDD approach. We also integrate the aspect-oriented paradigm into BRIC. We contribute with an approach to capture, specify and use aspects to safely evolve component-based systems. We establish that components extended by aspects preserve the proposed convergence relation that guarantees service conformance. Furthermore, we establish a connection between componente inheritance and aspects, presenting inheritance as a mechanism to define families of componentes and aspects to capture orthogonal concerns over them. The practical relevance of the proposed relations is illustrated by three case studies. One is an autonomous healthcare system, which evolve by the addition of new functionalities via inheritance and by the modularisation of its crosscutting concerns in a reusable and maintainable manner with aspects. Another case study is a bank system, whose functionalities are progressively realised and extended by refinement and inheritance, respectively. Finally, we model a P2P system extended by inheritance to reduce the network traffic. / Na medida em que os sistemas computacionais se tornam mais pervasivos, a demanda por métodos de desenvolvimento rigorosos e composicionais cresce dramaticamente. No desenvolvimento baseado em componentes (CB-MDD), sistemas complexos (muitas vezes humanamente intangíveis) são construídos a partir de elementos mais simples, chamados componentes. Para atingir os objetivos desta abordagem na direção de torná-la uma disciplina formal de desenvolvimento, componentes e regras de composição devem ser formalizados. Além disso, considerando que os requisitos de um sistema estão em constante evolução, necessitamos de mecanismos para refinar e estender de forma confiável tais sistemas. O modelo de componentes BRIC formaliza os conceitos chave da abordagem CB-MDD, além de garantir corretude por construção se baseando em regras de composição que preservam propriedades comportamentais. BRIC, porém, por não possuir relações de extensão, não suporta evolução de modelos baseados em componentes. Neste trabalho propomos relações de herança e refinamento para BRIC. Definimos uma semântica congruente que considera tanto a estrutura quanto o comportamento de componentes. Definimos refinamento como uma relação de pré-ordem, a qual é monotônica em relação as regras de composição de BRIC. Estendemos este modelo de componentes com suporte a extensibilidade via herança. As relações propostas permitem extensão de funcionalidade, ao mesmo tempo em que preservam conformidade de serviços, a qual é definida em termos de uma noção de convergência. Estabelecemos também uma conexão algébrica entre extensibilidade de componentes e refinamento. Até onde estamos cientes, este trabalho é pioneiro no desenvolvimento de noções de herança de componentes para uma abordagem CB-MDD formal e consistente. Também integramos o paradigma orientado a aspectos em BRIC. Contribuímos com uma abordagem para capturar, especificar e adotar aspectos no desenvolvimento confiável de sistemas baseados em componentes. Estabelecemos que componentes estendidos por aspectos preservam convergência, o que garante conformidade de serviços. Além disso, desenvolvemos uma conexão entre herança e aspectos, apresentando herança como um mecanismo para definir famílias de componentes e aspectos para capturar conceitos ortogonais sobre as mesmas. Ilustramos a relevância prática das relações propostas através de três estudos de caso. No primeiro, modelamos um sistema autônomo de cuidados médicos, estendido pela adição de novas funcionalidades via herança e pela modularização de conceitos transversais de forma reusável e manutenível via aspectos. Na sequência, modelamos um sistema bancário, cujas funcionalidades são progressivamente implementadas e estendidas pelo uso de herança e refinamento. Finalmente, modelamos um sistema P2P cujo tráfico é reduzido por extensão via herança.
|
160 |
Erfarenheter från användning av sekantpålning som stödkonstruktion : Fallstudier från projekt i Sverige / Experiences from the use of secant piling as a support structure : Case studies from projects in SwedenHöglund, Marcus, Forsén, Oscar January 2015 (has links)
Målet med rapporten är att redovisa erforderliga maskiner, personal och erfarenhetsdata för sekantpålning. Detta kan utnyttjas vid jämförelse med andra pålningsmetoder av företag. Sekantpålning används som en stödkonstruktion, vars uppgift är att stötta jordmassor vid schakt. De positiva egenskaperna med denna är en bidragande faktor till ett ökat utnyttjande av metoden. Genom att uppnå lägre vibrationsnivåer och minimera grundvattensänkning får metoden ett ökat mervärde. Sekantpålningsmetoden används i större utsträckning utomlands och det är först nu den börjar brukas i Sverige. Genom att Trafikverket har godkänt sekantpålning som en permanent konstruktion, kan metoden bryta ny mark i Sverige. Sekantpålningsmetoden i sig påverkas ej av det svenska mark- och klimatförhållandet. Det är den teknik som man utnyttjar vid sekantpålningen, som påverkas av de geologiska och hydrogeologiska förutsättningarna. Mark som består av rikligt med stenblock eller varierande sten storlekar bör man använda CSP-tekniken med foderrörsborrning. Tekniker som inte klarar av dessa markförhållanden är CFA och CAP, som istället utnyttjar en augerborr. Dessa tekniker utnyttjas när marken består av fastlera eller friktionsjord, vilket gör arbetet för augerborren betydligt lättare än om marken består av stenblock. Slutsatsen i rapporten visar att sekantpålning är det dyrare alternativet och att metoden inte kan konkurrera med de mer konventionella stödkonstruktionerna ur kostnadssynpunkt. För att sekantpålningen ska vara fördelaktig måste metoden ses ur ett större perspektiv och hänsyn tas till omgivningspåverkan och markförhållanden. På så sätt kan ett mervärde skapas. Metoden lämpar sig väl i innerstadsmiljö med närliggande byggnader, då buller och vibrationer är en påverkande faktor. Projekt som har utnyttjat sekantpålningsmetoden har varierande kostnader, då de har använt olika sekantpålningstekniker. Vid Norra länken 12 och 22 tillämpades CSP-tekniken som hade en kapacitet till att göra 2,5 pålar per dag till en kostnad av 11.500 kr/m². Vid Bargers plats i Malmö tillämpades CFA-tekniken till en kostnad av 2.500 kr/m². Vid Folkungagatan i Stockholm användes CAP-tekniken till en kostnad av 4.500 kr/m². Metoden har både för och nackdelar. Fördelarna är att metoden är flexibel vilket innebär att den kan anpassas efter önskad geometri. Metoden bidrar till mindre vibrationer som i sin tur minimerar risken för sättningar. Nackdelarna är att sekantpålning är dyrare än konventionella stödkonstruktioner p.g.a. att metoden är tidskrävande. Vid sekantpålning som permanent stödkonstruktion görs efterspänning av ankarstag som är tidskrävande. I rapporten presenteras byggprojekt där sekantpålning använts. Projekt som redovisas i rapporten är Odenplan station, Spjutmo kraftstation, Norra länken 12 och 22, Bagers plats och Folkungagatan. / The goal of the report is to present machines, staff and requisite experience data within secant piling. The information may be utilized in comparison with other piling methods by corporations. Secant piling is used as a support structure whose task is to keep the soil from sliding in to the pit during excavation. Its positive aspects of the environment are a contributing factor to increased use of the method. By achieving lower vibration levels and minimize the reduction in the groundwater level, the method adds value. The secant pile method is extensively used abroad and nowadays it begins to be operated in Sweden. Now when Trafikverket has approved secant piling as a permanent structure, the method can lead to more usage in Sweden. The secant pile method in itself is not affected by the Swedish soil and climatic condition. It is the technique you are utilizing when using secant piling that’s affected by the geological and hydrogeological conditions. Soil that is consisting of boulders or variable stone sizes should use CSP technology with casing drilling. Techniques that don’t work in these soil conditions is CFA and CAP, which instead uses an auger drill. These techniques are utilized when the soil consists of solid clay or friction soil, which makes the work of the auger drill much easier than if the land consists of stone blocks. The conclusion of the report indicate that secant piles are the more expensive option, and that the method cannot compete with the more conventional support structures in that regard. To understand that secant piles will be beneficial the method must be seen from a broader perspective and you have to look at the impact of the surroundings and the soil conditions. In this way, added value is created. The method is suitable in urban setting with nearby buildings, where noise and vibration is an influencing factor. Projects that have embraced the secant pile method have varying costs, since they have used different secant pile techniques. At Norra länken 12 and 22 they used the CSP technology that had a capacity to make 2.5 piles per day at a cost of 11,500 SEK/m². In Bagers Plats in Malmö they used the CFA technology at a cost of 2,500 SEK/m². At Folkungagatan in Stockholm they used the CAP technology at a cost of 4,500 SEK/m². The method has both advantages and disadvantages. The advantages are that the method is flexible which means that it can be adapted to the desired geometry. This method helps to reduce vibration, which in turn minimizes the risk of subsidence. The disadvantages are that secant piling is more expensive than conventional supporting structures because of the method is time consuming. When secant piles that are used as a permanent support structure the anchor rods have to be tightened often and that is time consuming. The report presents the construction projects where secant piling is used. Projects presented in the report are Odenplan station, Spjutmo kraftstation, Norra länken 12 and 22, Bagers plats and Folkungagatan.
|
Page generated in 0.0561 seconds