HolBA is a binary analysis library that can be used to formally verify binary programs using contracts. It is developed in the interactive theorem prover HOL4 to achieve a high degree of trust in verification, the result of verification is a machine-checked proof demonstrating its correctness. This thesis presents two proof-producing procedures. The first resolve indirect jumps in BIR, the binary intermediate language used in HolBA, given their possible targets. The second transfers contracts proved on resolved BIR programs without indirect jumps to the original ones containing indirect jumps. This allows the existing weakest precondition generator to automatically prove contracts on loop-free BIR fragments containing indirect jumps. The implemented proof-producing procedures were evaluated on a small binary program and generated synthetic BIR programs. It was found that the first proof-producing procedure is not very efficient, which could pose a problem when verifying large binary programs. Future work could include improving the efficiency of the first proof-producing procedure and integrate it with an external tool that automatically finds possible targets of indirect jumps. / HolBA är ett bibliotek för binär analys som kan användas för att formellt verifiera binära program med kontrakt. Det är utvecklat i den interaktiva teorembevisaren HOL4 för att åstadkomma en hög grad av tillit till verifiering, resultatet av verifiering är ett maskin-kontrollerat bevis som demonstrerar dess korrekthet. Detta arbete presenterar två bevis-producerande procedurer. Den första bestämmer indirekta hopp i BIR, den binära mellanliggande representationen som används i HolBA, givet deras möjliga mål. Den andra överför kontrakt bevisade för bestämda BIR program utan indirekta hopp till originalen med indirekta hopp. Detta möjliggör den existerande svagaste förutsättning generatorn att automatiskt bevisa kontrakt för sling-fria BIR fragment som innehåller indirekta hopp. De implementerade bevis-producerande procedurerna utvärderades med ett litet binärt program och med genererade syntetiska BIR program. Det visades att den första bevis-producerande proceduren inte är särskilt effektiv, vilket skulle kunna vara ett problem vid verifiering av stora binära program. Framtida arbete skulle kunna inkludera att förbättra effektiviteten för den första bevis-producerande proceduren och att integrera den med ett externt verktyg som automatiskt kan hitta de möjliga målen för indirekta hopp.

Formal analysis of security protocols is becoming increasingly relevant. In formal analysis, a model is created of a protocol or system, and propositions about the security of the model are written. A program is then used to verify that the propositions hold, or find examples of where they do not. This report uses formal methods to analyse the authentication aspect of a protocol that allows private individuals, enterprises, and systems to securely and asynchronously share sensitive data. Unpublished, early drafts of the protocol were studied and algorithms described in it were verified with the help of the formal verification tool Tamarin Prover. The analysis revealed two replay attacks. Improvements to the protocol were suggested based on this analysis. In later versions of the protocol, the improvements have been implemented by the protocol developers. / Det blir alltmer relevant med formell analys av säkerhetsprotokoll. I formell analys så skapas en modell av ett protokoll eller ett system, och påståenden om modellens säkerhet skrivs. Ett program används sedan för att verifiera att påståendena gäller, eller för att hitta exempel där de inte gäller. Den här rapporten avänder formella metoder för att analysera autentiseringsaspekten av ett protokoll som tillåter privatpersoner, företag och system att asynkront dela känslig information på ett säkert sätt. Opublicerade och tidiga utkast av protokollet studerades och de algoritmer som beskrivs i protokollet verifierades med hjälp av Tamarin Prover. Analysen avslöjade två återspelningsattacker. Förbättringar till protokollet föreslogs baserat på denna analys. I senare versioner har protokollutvecklarna implementerat förslagen.

Model checking is a formal verification technique for verifying temporal properties in state-transition models. The main problem with using model checking is the state explosion problem, where the number of states in the model can grow exponentially, making verification infeasible. Previous work has tried to mitigate the state explosion problem by representing code blocks as Hoare-logic contracts in an abstract state-transition model using the temporal logic TLA. This is achieved by treating the block as atomic. In order to ensure that the abstract state-transition model is faithful with respect to the temporal properties you want to verify, only some code blocks can be considered atomic. This thesis aims to answer how atomic code blocks can be identified atomically and evaluate their potential for reducing state space during model checking. We give a theoretical foundation of what it means for a code block to be considered as atomic in TLA. Moreover, we introduce a property that characterizes these atomic code blocks and presents an algorithm to identify them for sequential programs written in a subset of C. Experimental results demonstrate that the identification of atomic code blocks using our algorithm can be used to significantly reduce the state space during model checking, with an average reduction factor of 62. The potential of this verification approach is promising, however, further case studies are necessary to better understand the extent of this reduction across different program types and properties. / Modellkontroll är en formell verifieringsteknik för att bekräfta tidsrelaterade egenskaper i tillståndsövergångsmodeller. Huvudproblemet med modellkontroll är problemet med tillståndsexplosion, där antalet tillstånd i modellen kan öka exponentiellt och göra verifieringen ogenomförbar. Tidigare arbete har försökt mildra problemet med tillståndsexplosion genom att representera kodblock som Hoare-logiska kontrakt i en abstrakt tillståndsövergångsmodell med hjälp av tidslogiken TLA. Detta uppnås genom att behandla blocket som atomiskt. För att säkerställa att den abstrakta tillståndsövergångsmodellen är trogen med avseende på de tidsrelaterade egenskaper du vill verifiera kan endast vissa kodblock betraktas som atomiska. Denna avhandling syftar till att besvara hur atomiska kodblock kan identifieras automatiskt och utvärdera deras potential för att minska tillståndsutrymmet under modellkontroll. Vi ger en teoretisk grund för vad det innebär för ett kodblock att betraktas som atomiskt inom TLA. Dessutom introducerar vi en egenskap som karaktäriserar dessa atomiska kodblock och presenterar en algoritm för att identifiera dem för sekventiella program skrivna i en delmängd av C. Experimentella resultat visar att identifieringen av atomiska kodblock med hjälp av vår algoritm kan användas för att betydligt minska tillståndsutrymmet under modellkontroll, med en genomsnittlig reduktionsfaktor på 62. Potentialen för denna verifieringsmetod är lovande, men ytterligare fallstudier krävs för att bättre förstå omfattningen av denna reduktion över olika typer av program och egenskaper.

Background: Generative AI has achieved rapid and widespread acclaim over a short period since the inception of recent models that have opened up opportunities not possible before. Large Language Models (LLMs), a subset of generative AI, have become an essential part of code generation for software development. However, there is always a risk that the generated code does not fulfill the programmer's intent and contains faults or bugs that can go unnoticed. To that end, we propose that verification of generated code should increase its quality and trust. Objectives: This thesis aims to research generation of code that is both functionally correct and verifiable by implementing and evaluating four prompting approaches and a reinforcement learning solution to increase robustness within code generation, using unit-test and verification rewards. Methods: We used a Rapid Literature Review (RLR) and Design Science methodology to get a solid overview of the current state of robust code generation. From the RLR and related works, we evaluated the following four prompting approaches: Base prompt, Documentation prompting, In-context learning, and Documentation + In-context learning on the two datasets: MBPP and HumanEval. Moreover, we fine-tuned one model using Proximal Policy Optimization (PPO) for the novel task. Results: We measured the functional correctness and static verification success rates, amongst other metrics, for the four proposed approaches on eight model configurations, including the PPO fine-tuned LLM. Our results show that for the MBPP dataset, on average, In-context learning had the highest functional correctness at 29.4% pass@1, Documentation prompting had the highest verifiability at 8.48% verfiable@1, and finally, In-context learning had the highest functionally correct verifiable code at 3.2% pass@1 & verifiable@1. Moreover, the PPO fine-tuned model showed an overall increase in performance across all approaches compared to the pre-trained base model. Conclusions: We found that In-context learning on the PPO fine-tuned model yielded the best overall results across most metrics compared to the other approaches. The PPO fine-tuned with In-context learning resulted in 32.0% pass@1, 12.8% verifiable@1, and 5.0% pass@1 & verifiable@1. Documentation prompting was better for verifable@1 on MBPP. However, it did not perform as well for the other metrics. Documentation prompting + In-context learning was performance-wise between Documentation prompting and In-context learning, while Base prompt performed the worst overall. For future work, we envision several improvements to PPO training, including but not limited to training on Nagini documentation and utilizing expert iteration to create supervised fine-tuning datasets to improve the model iteratively. / Bakgrund: Generativ AI har uppnått snabb och utbredd popularitet under en kort tid sedan lanseringen av språk- och bildmodeller som har öppnat upp nya möjligheter. Large Language Models (LLMs), en del av generativ AI, har blivit en viktig del inom mjukvaruutveckling för kodgenerering. Det finns dock alltid en risk att den genererade koden inte uppfyller programmerarens avsikt och innehåller fel eller buggar som kan förbli oupptäckta. För att motverka detta föreslår vi formell verifiering av den genererade koden, vilket bör öka dess kvalitet och därmed förtroendet för den. Syfte: Detta examensarbetets syfte är att undersöka generering av kod som är bååde funktionellt korrekt och verifierbar genom att implementera och utvärdera fyra prompt-metoder samt en ny lösning genom reinforcement learning. Detta för att öka robusthet inom kodgenerering genom unit-test och verifieringsbelöningar. Metoder: Vi använde Rapid Literature Review (RLR) och Design Science metodik för att få en solid översikt över det nuvarande tillståndet för robust kodgenerering. Från RLR:en och relaterade arbeten utvärderade vi följande fyra prompt-metoder: Base prompt, Documentation prompting, In-context learning och Documentation + In-context learning. Dessutom fine-tune:ade vi en modell med Proximal Policy Optimization (PPO) för denna uppgift. Resultat: Vi mätte funktionell korrekthet- och verifieringsvinst-statistiken samt andra mätvärden för de fyra föreslagna prompten på åtta modellkonfigurationer, inklusive den PPO fine-tune:ade LLM:en. Våra resultat visar på MBPP datasetet att i genomsnitt hade In-context learning den högsta funktionella korrektheten vid 29,4% pass@1, Documentation prompting hade den högsta verifierbarheten vid 8,48% verifiable@1, och slutligen hade In-context learning mest funktionellt korrekta verifierbara kod vid 3.2% pass@1 & verifiable@1. Utöver detta visade den PPO fine-tune:ade modellen konsekventa förbättringar gentemot den förtränade basmodellen. Slutsatser: Vi fann att In-context learning med den fine-tune:ade PPO-modellen gav de bästa övergripande resultaten över de flesta mätvärden jämfört med de andra metoderna. Den PPO fine-tune:ade modellen med In-context learning resulterade i 32.0% pass@1, 12.8% verifiable@1, och 5.0% pass@1 & verifiable@1. Documentation prompting va bättre för verifable@1, men den fungerade inte lika bra för de andra mätvärdena. Documentation + In-context learning hamnade mellan Documentation prompting och In-context learning prestationsmässigt. Base prompt presterade sämst av de utvärderade metoderna. För framtida arbete ser vi flera förbättringar av träningen av PPO-modellen. Dessa innefattar, men är inte begränsade till, träning med Nagini dokumentation samt användning av expert iteration för att bygga ett dataset i syfte att iterativt förbättra modellen.

Verification of knowledge-bases is a critical step to ensure the quality of a knowledge-based system. The success of these systems depends heavily on how qualitative the knowledge is. Manual verification is however cumbersome and error prone, especially for large knowledge-bases. This thesis provides a design theory, based upon the suggested framework by Gregor and Jones (2007). The theory proposes a general design of automated verification tools, which have the abilities of verifying heuristic knowledge in rule-based systems utilizing certainty factors. Included is a verification of completeness and consistency technique customized to this class of knowledge-based systems. The design theory is instantiated in a real-world verification tool development project at Uppsala University. Considerable attention is given to the design and implementation of this artifact – uncovering issues and considerations involved in the development process. For the knowledge management practitioner, this thesis offers guidance and recommendations for automated verification tool development projects. For the IS research community, the thesis contributes with extensions of existing design theory, and reveals some of the complexity involved with verification of a specific rule-based system utilizing certainty factors.

With the recent rise of 3D-printing as a form of manufacturing and their advantages for quick prototyping there is an interest for 3D-printed optical components. This thesis tests how well 3D-printed quasi-optical components preform and verify measurements with electromagnetic simulations. Measurements were made using a 60GHz FM-CW radar as well with a trihedral reflector, and tested on 3D-printed PLA lenses printed using an Ultimaker 2+. The measurements made are of the refractive index of the material, as well as the focal length of the lenses. Results showed PLA having a refractive index close to n = 1.654 in the 60GHz region. Results also showed the lenses having consistent properties like focal length and gain, two lenses having focal length of 23.7 and 23.9 mm which are close to the simulation of 24.05 mm. These findings shows 3D printed quasi-optical components have sufficient performance for use of prototyping or production depending on use. There are also some questions that have arisen like how does crystallisation in the plastic affect the components properties? And how does the PLA degrading affect the quality of the lenses over time? / På grund av framgångar inom 3D-utskrivning på senaste tiden som en form av tillverkning och dess fördelar med snabb framtagande av prototyper finns det ett intresse för utskrivna optiska komponenter. Detta examensarbete testar hur väl 3D-utskrivna kvasioptiska komponenter funger\-ar och verifierar testresultat med elektromagnetiska simuleringar. Mät\-ning\-arna gjordes med en FM-CW radar och en trihedral reflektor, och testade PLA linser utskrivna med en Ultimaker 2+. Mätningar\-na gjordes på materialets brytningsindex samt linsernas brännvidd. Resultaten visade att PLA har ett brytningsindex nära n = 1.654 i 60GHz området. Resultaten visade även hur linserna har konsekventa egenskaper som brännvidd och förstärkning. De två slutgiltiga linserna hade en brännvidd på 23.7 and 23.9 mm vilket är nära simuleringen på 24.05 mm. Dessa resultat visar att 3D-utskrivna komponenter har tillräcklig prestanda för användning i framtagande av prototyper eller produktion beroende på användning. Det finns en del frågor som kommit till, som hur påverkar plastens kristallisation komponentens egenskaper? Och hur påverkar PLAs nedbrytande linsernas kvalité?

Året är 2017 och den ökande användningen av enheter som är kopplade mot internet har exploderat okontrollerat. Enheter modifieras i en snabb takt för att kunna kopplas samman med syftet att få en mer effektivare vardag, i folkmun häftigare enheter och framförallt för att generera en ökad försäljning av dessa produkter. Kommunikationsverktygen kopplas samman och därmed samlas en stor mängd data på enskilda enheter som kan bli sårbara i form av övervakning, intrång och övertagande för syften som innehavaren kan vara helt omedveten om. Om individens enhet är medverkande i scenariot att stänga ned servern som håller en samhällstjänst uppe under en tidpunkt av en allvarlig fysisk attack mot Sverige: Vem bär i så fall skulden? Detta kallas överbelastningsattack och är en av många potentiella sårbarheter i dagens samhälle.   Internet of Things är ett nytt fenomen som är relativt outforskat med många öppna och obesvarade frågor. Forskningen ligger otvivelaktigt steget efter. Det gemensamma i forskningsartiklarna är slutsatsen: vi ska forskare vidare inom detta område. Alarmerande eftersom enheterna redan är närvarande i vardagen. Informationssäkerheten och individens personliga integritet är vad som står på spel, och frågan är vad individerna är villiga att offra för att ha de senaste produkterna.   Metoden och genomförandet av denna kandidatuppsats har bestått av det explorativa tillvägagångssättet. En litteraturstudie av forskningsartiklar och personliga intervjuer har genomförts med relevanta individer inom området.   Denna kandidatuppsats kommer inte att ge facit på vad som bör göras härnäst. Målet är att upplysa om olika problemställningar avseende fenomenet Internet of Things. I uppsatsen ligger fokuseringen på att generera en beskrivning av hur informationssäkerhet och personlig integritet kan påverka skapande och användandet av enheter som är uppkopplade mot Internet of Things.   Syftet med denna explorativa studie är att identifiera och beskriva faktorer som bidrar med ett framgångsrikt skapande och användande av Internet of Things enheter med fokusering på informationssäkerhet och personlig integritet. Slutsatserna är att faktorer som påverkar är bekräftelse av identitet, standarder, otillgänglig åtkomst samt användarkontroll.

Under produktionen av kartong vid det integrerade massa- och kartongbruket, som ägs av Holmen Iggesund Paperboard AB, bildas klorat som är giftigt för vattenlevande organismer. Därför är det väsentligt att utsläppet av klorat till havet, via avloppsvattnet från bruket, hålls under de gränsvärden som fastställts. För att övervaka kloratutsläppet analyseras prover på avloppsvattnet rutinmässigt, och en jonkromatograf ämnades tas i drift för ändamålet. Jonkromatografi är en standardiserad metod för analys av klorat, som måste verifieras innan den tas i bruk. Inga explicita krav fanns på hur omfattande verifieringen skulle vara. Ett syfte med studien var därför att utveckla generella rekommendationer för omfattningen av verifieringen av en standardiserad analysmetod. Litteratur angående verifiering eftersöktes och summerades, och utifrån den togs en verifieringsplan för jonkromatografisk analys av klorat fram. Mätresultat som erhölls utvärderades statistiskt. Slutsatserna var; att verifiering bör planeras på ett sätt så att kalibrering och underhåll av instrumentet sker i samma omfattning som är tänkt vid rutinanvändning av analysmetoden; selektivitet bör testas tidigt, och riktiga prover bör analyseras i ett tidigt skede; omfattningen av verifieringen med avseende på provmatriser och koncentrationsnivåer ska återspegla de provmatriser och koncentrationer som analysmetoden kommer att innefatta i rutinarbetet; antalet försök som bör inkluderas beror på kraven som ställs på de olika egenskaper som definierar prestandan. Minst 6 försök på varje provmaterial var ett riktmärke för precision och riktighet, medan ett försök räckte vid utvärdering av selektivitet och instrumentets mätområde. För att kunna säkerställa god analyskvalité, är utbildning i analysmetodik en viktig del. Ytterligare ett syfte med denna studie var att undersöka utbildningsverksamhetens lärandemål, samt vilka utmaningar som fanns inom utbildningen i analysmetodik. Genom fokusgruppintervjuer och observationer samlades information inom utbildningsverksamheten och dess utmaningar. Utifrån det teoretiska ramverket självstyrd inlärning utfördes en deduktiv tematisk analys av den insamlade datan. Slutsatserna av arbetet löd: Det övergripande syftet med upplärningen inom en analysmetod var att personen som genomgått utbildningen ska kunna ansvara för att tillämpa analysmetoden självständigt utifrån instruktionen, ha kunskap om rimliga mätresultat, kunna reflektera över sitt arbete, samt ha kunskap om syftet med analysmetoden. Ingen standardiserad mall för vad som ska ingå i utbildningen inom en analysmetod fanns, vilket bidrog till osäkerheter angående huruvida likvärdig kompetens uppnåddes för personer under utbildning; dagens utbildningsupplägg inbjöd inte till att personen under upplärning tog på sig ansvaret för uppfyllandet av lärandemålen i den utsträckning som önskades. För att möjliggöra detta föreslogs att ett förberedande moment skulle införas, samt att den lärande skulle få mer tid och möjlighet att genomföra delar av utbildningen självständigt. / During the production of paperboard at the integrated pulp and paperboard mill, owned by Holmen Iggesund Paperboard AB, chlorate is formed, which is a toxic compound for aquatic organisms. It is therefore essential that the chlorate levels in the wastewater from the mill, which is released to the ocean, are below the established limit. In order to monitor the effluent of chlorate, wastewater samples are routinely analyzed, and for this purpose an ion chromatograph was intended to be put to use. Ion chromatography is a standardized method for chlorate analysis, which needs to be verified before being used for routine analyses. No explicit requirements regarding the extent of the verification existed. One purpose of this study was therefore to develop general recommendations regarding the extent of verification of a standardized analytical method. Literature regarding verification was sought for and summarized. Based on the literature, a plan for verifying ion chromatographic analysis of chlorate was constructed. The measurement results obtained were evaluated statistically. Conclusions drawn were: calibration and maintenance of the instrument during the verification process should reflect the frequency of maintenance and calibration planned during the routine use; selectivity should be tested early on, as well as real samples; the extent of the verification with respect to matrices and concentration levels should reflect those that will be included in the routine use of the analytical method; the number of experiments included depends on the requirements imposed on the performance characteristics of the method. At least 6 experiments for each sample was a good aim for verifying precision and trueness, while one experiment was enough for verification of selectivity and the working range of the instrument. In order to ensure satisfactory analysis quality, training in analytical methods is an important aspect. Another purpose of this study was to investigate the learning objectives of the educational activities as well as what challenges could be identified with respect to training in analytical methods. Through focus group interviews and observations, data was collected about the educational activities and challenges. Based on the theoretical framework self-directed learning, a deductive thematic analysis was performed. Conclusions were: The overall purpose of the training in analytical methods was that the person who underwent training should be able to independently apply the analytic method, with the aid of the analytical instruction, have the necessary knowledge about reasonable results, be able to reflect about their work and have knowledge about the purpose of the analytical method. No standardized template regarding what should be included in the training existed, which contributed to uncertainties regarding if equivalent knowledge was achieved for persons under training. The educational approach of today did not encourage the person under training enough to take responsibility for fulfilling the learning objectives. To enable this, it was suggested that a preparation element should be included in the training, and also that the person under training should get more time and opportunities to complete some of the training independently.

Glas är ett styvt material som används bland annat inom byggbranschen och fordonsindustrin. Glas har hög styvhet och hög hållfasthet men är ett sprött material. När en spricka uppstår i en laminerad glasbalk minskas dess bärförmåga och styvhet och säkerhetsrisken ökar. För att garantera en hög säkerhet används laminerat glas där tunna plastfilmer limmar ihop flera skikt av glas (som även kallas för lameller). När glaset lamineras fungerar det som ett paket där spänningarna kan överföras mellan de olika lamellerna. Användningsområden inom byggbranschen kan vara plana element, till exempel för fönster eller balkonräcken, dessutom finns både liggande balkar (böjning i den tunna riktningen) samt stående balkar. Även i balkar av laminerat glas kan sprickor i en av lamellerna uppstå. Dessa fångas dock upp av de andra lamellerna så att hela balken förblir intakt och hålls på plats. En sprucken balk tappar då en del av bärförmågan och styvheten jämfört med en osprucken balk. Spruckna balkar kan alltså inte bära samma last. Syftet med arbetet är att öka kunskapen om beteendet hos laminerat glas som är sprucket och få bättre förståelse för hur laminerat glas beter sig när det går till brott. Målet är att verifiera den numeriska beräkningsmodellen av Abdul Khader, Basim & Reshid (2020) genom experimentella försök. Modellen beskriver liggande balkar av laminerat glas, både spruckna och ospruckna balkar. I detta examenarbete användes olika metoder: litteraturundersökning, tillämpning av en beräkningsmodell samt experiment. Litteratundersökningen gav ett fördjupande förståelse dels om ämnet glas exempelvis om olika typer av glas och glasets generella egenskaper, dels om laminerat glas, hur det är uppbyggt, tillverkat och egenskaper förbättras genom lamineringen. Beräkningsmodellen som detta arbete bygger på är från en tidigare studie, där en beräkningsmetod för spruckna glasbalkar beskrevs med hjälp av den så kallade effektiva tjockleksmetoden för böjstyvhet av laminerat glas. Experiment genomfördes för att studera hur laminerade glasbalkar med och utan spricka i mitten beter sig när de utsätts för belastning. Resultaten visar skillnaden mellan ospruckna och spruckna balkar av laminerat glas med två skikt när det gäller böjstyvheten och bärförmågan. Experimenten visar att nedböjningen för spruckna balkar är dubbelt så stor som för ospruckna balkar. Skillnaden beror på att böjstyvheten hos spruckna balkar är lägre än hos ospruckna balkar. På grund av sprickan i mitten överförs lasterna endast i en skiva, och dessutom minskas böjstyvheten i den ospruckna delen. Beräkningsmodellen överensstämde väl med resultaten från de utförda experimenten. Detta bekräftar att modellen kan tillämpas för laminerade glasbalkar. Mer omfattande studier bör dock genomföras där de ingående parametrarna varieras, till exempel genom längre balkar, sprickor på andra ställen än i mitten, samt att olika material för mellansiktet används.

Passenger safety and comfort are important aspects in the process of vehicle development. The world is heading towards developing the safest possible vehicle on the road. Using vehicle motion control functions is one of the ways to enhance vehicle stability. These motion control functions need to be developed in an energy optimised way. By complementing some of the development process with virtual models, both the development time and cost could be minimised. Hence, a sustainable way of control function development could be achieved. In order to verify, validate and calibrate vehicle motion control functions, an accurate model of the virtual vehicle is required. Hence, a research question on how good the virtual model needs to be for the purpose has been addressed. This report suggests a framework in order to determine the capabilities of a virtual vehicle.In this report, a comparison study has been carried out by exciting the real car and virtual model of a Volvo XC90 with a focus of covering the six degrees of freedom (Yaw, pitch, roll, longitudinal, lateral and vertical). A semi automated framework that possesses the capability of automating the testing in a virtual platform has been established. From the test results, the virtual vehicle capabilities were determined. Further, in the second part of the report, an example use case has been considered by taking two calibration sets of Electronic stability control (ESC) system in order to verify the previously established framework.The analysis includes various levels of plant and controller complexity such as Model-in-loop, Software-in-loop and Hardware-in-loop and on two different road surfaces, low friction and high friction. From the observations, the virtual models considered correlates well for the purpose of verification and validation. However, for the purpose of calibration, the models need to be fine-tuned in the virtual platform. Furthermore, the correlation on low friction road surface could be improved by simulating the tests using an advanced tyre model. Overall, this study helps in choosing the correct complexity of various subsystems in a vehicle for the purpose of verification, validation and calibration of vehicle motion control functions. / Passagerarsäkerhet och komfort är viktiga aspekter i utvecklingen av ett fordon. Världen är på väg mot att utveckla säkraste möjliga fordon på vägen. Användning av fordonetse rörelsekontrollfunktioner är ett av sätten att förbättra fordonets stabilitet. Dessa rörelsekontrollfunktioner måste utvecklas på ett energioptimerat sätt. Genom att komplettera en del av utvecklingsprocessen med virtuella modeller kan både utvecklingstid och kostnad minimeras. Därför kan ett hållbart sätt att utveckla funktionerna för kontrollfunktioner uppnås. För att verifiera, validera och kalibrera fordonets rörelsekontrollfunktioner krävs en detaljerad modell av ett virtuellt fordon. Därför har en forskningsfråga om hur bra den virtuella modellen måste vara för ändamålet behandlats. Denna rapport föreslår ett ramverk för att bestämma funktionerna hos virtuella fordon.I denna rapport har en jämförelsestudie genomförts genom att excitera den verkliga bilen och den virtuella modellen av en Volvo XC90 med fokus på att täcka de sex frihetsgraderna (gir, nick, roll, längs, lateral, vertikal). Ett semi-automatiserat ramverk som har förmågan att automatisera testningen i en virtuell plattform har skapats. Från testresultaten bestämdes de virtuella fordonsfunktionerna. Vidare har i den andra delen av rapporten ett exempel på användningsfall beaktats genom att man tar två kalibreringsuppsättningar av ESC-system (Electronic Stability Control) för att verifiera det tidigare etablerade ramverket.Analysen innefattar olika nivåer av modell- och styrenhetskomplexitet såsom Model-in-loop, Software-in-loop och Hardware-in-loop och på två olika vägytor, låg friktion och hög friktion. Enligt observationerna är de virtuella modellerna väl korrelerade för verifiering och validering. För kalibreringen måste dock modellerna finjusteras på den virtuella plattformen. Dessutom kunde korrelationen på lågfriktionsvägytan förbättras genom att simulera testerna med hjälp av en avancerad däckmodell. Sammantaget hjälper den här studien att välja rätt komplexitet hos olika delsystem i ett fordon för verifiering, validering och kalibrering av fordonets rörelsekontrollfunktioner.