Det traditionella sättet att programmera industriella styrsystem har alltid varit ettkostsamt och oförutsägbart sätt att driftsätta produktionsutrustning. Detta beror påatt styrsystemen programmeras parallellt med driftsättningen som sker sent iprojektet vilket inte ger mycket rum för misstag. I det här examensarbetet har enstudie gjorts på hur programvaran SIMIT kan användas för virtuell driftsättning.Genom att använda SIMIT för att skapa en digital tvilling som kan simulera signaler iproduktionen. Detta ska då leda till att programmeringsfel och design fel som annarskan uppstå vid en traditionell driftsättning kan minskas.Undersökningen inkluderade vilka typer av komponenter som är lämpliga attsimulera med hjälp av SIMIT. Hur SIMIT kan användas på bästa sätt för att skapa endigital tvilling som klarar av att simulera signaler i en produktion. Om det går attskapa en automatiskt genererad modell som är tillräckligt bra föra att användas i ettFactory Acceptens Test (FAT). Om det är möjligt att använda ett skript somautomatiskt testar digitala tvillingen med styrsystemen. Om det är möjligt attansluta SIMIT till ett Manufacturing Execution System (MES) och SupervisoryControl And Data Acquisition (SCADA) system. För att undersöka detta gjordesflera tester där olika funktioner i SIMIT användes för att skapa en digital tvilling aven monteringscellen.I undersökningen har flera olika sätt att skapa en digital tvilling undersökts där olikafunktioner i SIMIT har testats i delmoment. Utifrån resultaten har slutsatser dragitsbaserat på vilket sätt som är lättast, vilket sätt som ger bäst resultat och vilket sättsom fungerar.Slutsatsen av studien är att SIMIT är en lämplig mjukvara för att simulera signalernaför komponenter som inte har ett eget styrsystem t.ex. kameror, knappar, motorereller säkerhetskomponenter. Det bästa sättet att skapa en digital tvilling är attkombinera SIMIT med andra mjukvaror som kan simulera komponenterna som hareget styrsystem. Det gick inte att använda skript funktionen för att automatiskt testakoden för styrsystemen utan att ha en helt fungerande simulering för helamonteringscellen. I undersökningen av automatiskt genererade modell framgick detatt det inte gick att skapa en automatiskt genererad modell som gick att använda iSIMIT. I undersökningen av att simulera signaler från högre nivåer av automationssystemet som t.ex. MES och SCADA systemen, framgick det att det går att kopplaSIMIT till både MES och SCADA systemet. / The traditional way of programming industrial control systems has always been acostly and unpredictable way of commissioning production equipment. This isbecause the control systems are programmed in parallel with commissioning, whichtakes place late in the project, which leaves little room for error. In this thesis, astudy has been made on how the SIMIT software can be used for virtualcommissioning. By using SIMIT to create a digital twin that can simulate signals inproduction. This should then lead to a reduction in programming errors anddesigner errors that can otherwise occur in a traditional commissioning.The survey included what types of components are suitable to simulate using SIMIT.How SIMIT can be used in the best way to create a digital twin that can simulatesignals in a production. If it is possible to create an automatically generated modelsthat are good enough to be used in a Factory Acceptance Test (FAT). If it is possibleuse a script that automatically tests the digital twin with the control systems. If it ispossible to connect SIMIT to a Manufacturing Execution System (MES) andSupervisory Control And Data Acquisition (SCADA) system. To investigate this,tests were carried out to create a digital twin for an assembly cell.In the survey, several different ways of creating a digital twin have been done wheredifferent functions of SIMIT have been tested. Based on the results, conclusions havebeen drawn based on which way is easiest, which way gives the best results andwhich way works.The conclusion of the study is that SIMIT is a suitable software for simulating thesignals for components that do not have their own control system, e.g. cameras,buttons, motors or safety components. The best way to create a digital twin is tocombine SIMIT with other software that can simulate the components that havetheir own control system. It was not possible to use the script function toautomatically test the code for the control systems without having a fully functionalsimulation for the entire assembly cell. In the investigation of automaticallygenerated models, it appeared that it was not possible to create an automaticallygenerated model that could be used in SIMIT. In the investigation of simulatingsignals from higher levels of the automation system such as e.g. MES and SCADAsystems, it appeared that it is possible to connect SIMIT to both the MES and theSCADA system.

Different security issues are a top subject around the world, especially since the terror threats seem to intensify. In the same time, the transport industry suffer from problems with smuggling and theft of valuable goods. One way to increase the security might be to have a verification system installed in commercial trucks, in order to assure that the driver is the proper one. This thesis has two purposes. One is to find appropriate methods for driver verification and build a prototype of a verification system which can be used for testing and further development. The other is to study how truck drivers perceive such a system and how their conception goes along with the growing demand for higher security. The present work is the result of a cooperation between an engineer and a cognitive scientist. The thesis focuses on the transport industry and was performed for Volvo Technology Corporation (VTEC), Gothenburg, Sweden. Eleven available verification methods were studied. To enable a well-based selection of methods to implement in the prototype, inquiries and interviews with truck drivers and haulage contractors were carried out to complement the theoretical study. One regular and three biometric verification methods were chosen for the test; fingerprint verification, face recognition, voice recognition and PIN verification. These methods were put together to a prototype system that was implemented in a truck simulator. A graphical user interface was developed in order to make the system user friendly. The prototype system was tested by 18 truck drivers. They were thoroughly interviewed before and after the test in order to retrieve their background, expectations and opinions as well as their perceptions and experiences of the test. Most of the test participants were positive to the prototype system. Even though they did not feel a need for it today they believed it to “be the future”. However, some participants felt uncomfortable with the system since they felt controlled by it. It became clear how important it is to have a system that respect the users’ privacy and to assure that the users are well informed about how the system is used. Some of the technology used for the verification system requires more development to fit in the automotive context, but it is considered to be possible to achieve a secure and robust system.

For Siemens Industrial Turbomachinery to meet its business objectives a modular authentication concept has to be implemented. Such a mechanism must be cost- effective while providing a well-balanced level of security, easy maintenance and be as user-friendly as possible. Authenticating users securely involves the combination of two fields, theory of authentication mechanisms in information systems and human computer interaction. To construct a strong user authentication system the correlations of these fields has to be understood and provide guidance in the design. Strong user authentication mechanisms enforce the use of two-factor authentication or more. The combinations implemented rely on knowledge, possession and sometimes logical-location. A user authentication system has been implemented using leading industrial products as building blocks glued together with security analysis, programming and usability research. The thesis is divided into two parts, the first part giving the theoretical background of cryptography, authentication theory and protocols needed for the understanding of the second part, providing security analysis, blueprints, and detailed discussions on the implemented system. Conclusions have been drawn regarding the implemented system and its context as well as from strict theoretical reasoning regarding the authentication field in general. Conclusions include: · The unsuitability of remote authentication using biometrics · The critical importance of client security in remote authentication · The importance of a modular structure for the security of complex network-based systems

Volvo Group Trucks Operations (GTO) i Skövde är ett utvecklande och framgångsrikt företag som arbetar med ständiga förbättringar och effektiviserar arbetsuppgifterna, för att snabbt kunna möjliggöra förutsättningarna för att hitta problemlösningar. Volvo GTO och Projektengagemang vill genomföra en ombyggnation av kärnskjutmaskinen, där installation och programmering av ett nytt styrsystem ingår. För att korta ner den verkliga driftsättningstiden i projektet, har Volvo ambitionen att kunna utföra olika testkörningar samt virtuellt verifiera styrsystemets program och funktion mot en emuleringsmodell. Huvudsyftet med examensarbetet är att bygga en emuleringsmodell i emuleringsmjukvaran Simumatik3D, där den virtuella modellen efterliknar och avspeglar den verkliga produktionsutrustningen (Digital tvilling). Med hjälp av modellen, kan en virtuell driftsättning tillämpas genom att verifiera och validera den verkliga PLC-logiken mot emuleringsmodellen samt upptäcka alla felaktigheter innan implementeringen i verkligheten. PLC-logiken programmeras i programmeringsmjukvaran Tia Portal V14. Den teroetiska referensramen har genomförts för att fördjupa sig i den teoretiska bakgrunden kring emulering och virtuell driftsättning. Litteraturstudien tar upp och analyserar olika fallstudier som tidigare gjorts inom området. Modellen och PLC-logiken validerades mot varandra för att undersöka hur verklighetstrogen modellen var. Kommunikationen mellan de olika mjukvarorna har erhållits för att med hjälp av PLC-logiken kunna styra de olika rörelserna i produktionssystemet. PLCSIM Advanced har använts där det föreställer en verklig PLC-hårdvara för att kunna exekvera PLC-logiken i en virtuell styrenhet.  Det som levereras är en emuleringsmodell med 3D-CAD modeller och en virtuell driftsättning har gjorts med hjälp av modellen. PLC-logiken har validerats och verifierats mot emuleringsmodellen, där många olika felaktigheter har upptäckts och korrigerats.

Having well-functioning equipment for the soldiers and sailors in the Swedish Armed Forces to defend the nation’s territory has been a priority since the catastrophic failure of the flagship Vasa almost 400 years ago. The quality assurance of defense materiel that is procured for the Swedish Armed Forces by the Swedish Defence Materiel Administration (SDMA) is conducted using qualified verification and validation activities, which are supported using complex resources that either create the conditions for tests or gather data from tests. The department Test and Evaluation Marine (T&E Marine) in the SDMA, which works with verification and validation (VoV) of naval defense materiel, has a need to identify and develop new VoV resources for future naval acquisitions. The purpose is to find which needs the department of SDMA T&E Marine has regarding test resources and from the needs develop a specification of a possible VoV resource. In cooperation with the T&E Marine department, the study has used the Design Thinking methodology in a double diamond context and has through conducting interviews, observations, and a workshop created an analysis of the current state of VoV resources, which of these should be further developed, and which new resources the department could acquire to support future test and evaluation. The result of this study is that the analysis of the current situation shows that the department needs a modular remotely piloted aerial system. The result also includes a conceptual design of the VoV resource which the department could procure to support its future verification and validation work. The conclusion is that there is need for several different VoV resources. One VoV resource could be a modular remotely piloted aerial system, that is both easy to use and to carry. / Att svenska soldater och sjömän ska ha välfungerande och säker materiel för att hävda Sveriges territorium har varit en av statens prioriteringar sedan förlisningen av regalskeppet Vasa för snart 400 år sedan. Kvalitetssäkringen av försvarsmateriel som anskaffas till Försvarsmakten genom Försvarets Materielverk (FMV) sker idag genom kvalificerade verifierings- och valideringsaktiviteter och stöds utav komplexa resurser som antingen skapar förutsättningar för prov, eller samlar in data för proven. Avdelningen Test & Evaluering Marin (T&E Marin) på Försvarets Materielverk, som arbetar med verifiering och validering (VoV) av marin försvarsmateriel, har behov av att identifiera och utveckla nya VoV-resurser för framtida anskaffningar i marina domänen. Arbetet syftar till att ta reda på vilka behov som finns inom T&E Marins område för VoV-resurser och utifrån detta behov ta fram en specifikation på hur en VoV-resurs kan se ut. I samarbete med T&E Marin har studien använt sig av Design Thinking metodologin i en Double Diamond kontext, och har genom intervjuer, observationer och en workshop skapat en nulägesanalys för VoV-resurser, vilka som finns idag, vad som önskas vidareutvecklas, och vilka nya resurser som avdelningen kan ha för att stödja sitt arbete. Resultatet är en nulägesanalys som visar att ett behov är en uppdragsanpassningsbar fjärrmanövrerad flygfarkost. Resultatet innefattar också ett konceptförslag på den önskade VoV-resursen som avdelningen bör anskaffa för att stötta sitt framtida VoV-arbete. Slutsatsen är att det finns behov för flera olika VoV-resurser. En av dessa kan vara en fjärrstyrd flygfarkost med hög förmåga för uppdragsanpassning, som är enkel att använda och att bära med sig.

The most performant Machine Learning (ML) classifiers have been labeled black-boxes due to the complexity of their decision process. eXplainable Artificial Intelligence (XAI) methods aim to alleviate this issue by crafting an interpretable explanation for a models prediction. A drawback of most XAI methods is that they are heuristic with some drawbacks such as non determinism and locality. Formal Explanations (FE) have been proposed as a way to explain the decisions of classifiers by extracting a set of features that guarantee the prediction. In this thesis we explore these guarantees for different use cases: speeding up the inference speed of tree-based Machine Learning classifiers, curriculum learning using said classifiers and also reducing training data. We find that under the right circumstances we can achieve up to 6x speedup by partially compiling the model to a set of rules that are extracted using formal explainability methods. / De mest effektiva maskininlärningsklassificerarna har betecknats som svarta lådor på grund av komplexiteten i deras beslutsprocess. Metoder för förklarbar artificiell intelligens (XAI) syftar till att lindra detta problem genom att skapa en tolkbar förklaring för modellens prediktioner. En nackdel med de flesta XAI-metoder är att de är heuristiska och har vissa nackdelar såsom icke-determinism och lokalitet. Formella förklaringar (FE) har föreslagits som ett sätt att förklara klassificerarnas beslut genom att extrahera en uppsättning funktioner som garanterar prediktionen. I denna avhandling utforskar vi dessa garantier för olika användningsfall: att öka inferenshastigheten för maskininlärningsklassificerare baserade på träd, kurser med hjälp av dessa klassificerare och även minska träningsdata. Vi finner att under rätt omständigheter kan vi uppnå upp till 6 gånger snabbare prestanda genom att delvis kompilera modellen till en uppsättning regler som extraheras med hjälp av formella förklaringsmetoder.

Formal methods is a subfield of computer science in which mathematics and logic are used to prove properties of programs and/or systems. Two families of methods within formal methods are model checking and deductive verification. One concrete model checking framework is the TLA+ specification language and the model checker TLC which can check properties of TLA+ models through state space exploration. TLC can also be used to check so-called temporal properties, e.g. liveness and safety properties, of C programs, if they are first translated to TLA+ models. Such a translation has previously been automated for a subset of C, but the models produced may be unnecessarily detailed, making checking slow. One suggested solution to this problem is to abstract away irrelevant details of the models. Such abstractions can be expressed for C programs using a specification language called ACSL, and then proven correct with automatic tools for deductive verification. Previous work has shown that using ACSL-based abstractions when converting C programs to TLA+ models can reduce the state space size for the resulting models and also the time required for checking certain properties with TLC. However, the knowledge about the impact of this approach is limited. This thesis therefore aims to extend that knowledge by investigating the use of the approach for different C programs and properties. An experiment is performed in which the approach is evaluated for 4 systematically constructed C programs and 2 different properties that those programs should satisfy. The results show that for the state space size reduction, abstracting away nondeterministic code, i.e. code which may execute in several different ways, led to a much greater reduction than abstracting away deterministic code. For the deterministic code, the reduction was also larger when abstracting away a greater number of C statements as opposed to a smaller number. For the running time of TLC when checking temporal properties, the reduction was also more significant when abstracting away nondeterministic code. The running time for TLC was much higher when checking a liveness property compared to when checking a safety property. / Formella metoder är ett område inom datalogin inom vilket matematik och logik används för att bevisa särskilda egenskaper hos program och/eller system. Två familjer av metoder inom detta område är modellprövning och deduktiv verifiering. Ett konkret ramverk för modellprövning är TLA+ och modellprövaren TLC, som kan pröva egenskaper hos TLA+ -modeller genom att utforska möjliga tillstånd. TLC kan också pröva så kallade temporala egenskaper hos C-program, exempelvis säkerhets- och aktivitetsegenskaper (liveness properties), förutsatt att dessa först översätts till TLA+ -modeller. En mekanism för automatisk sådan översättning har tidigare utvecklats för en delmängd av C, men de resulterande modellerna kan bli onödigt detaljrika, vilket gör prövning långsam. En föreslagen lösning på detta problem är att abstrahera bort irrelevanta detaljer i modellen. Sådana abstraktioner kan för C-program uttryckas med hjälp av ACSL, ett specifikationsspråk för C, och bevisas vara korrekta med hjälp av automatiska verktyg för deduktiv verifiering. Tidigare forskning har visat att ACSL-baserade abstraktioner, när Cprogram omvandlas till TLA+ -modeller, kan minska mängden möjliga modelltillstånd och dessutom tiden det tar att kontrollera vissa temporala egenskaper med TLC. Dock är kunskapen om effekterna av denna metod begränsad. Denna uppsats ämnar därför utöka denna kunskap genom att undersöka användningen av metoden för olika C-program och egenskaper. Ett experiment genomförs i vilket metoden utvärderas på 4 systematiskt konstruerade C-program och 2 egenskaper som dessa förväntas ha. Resultaten visar att avseende minskningen av antalet möjliga programtillstånd, så är abstraktion ifrån ickedeterministisk kod, alltså kod som kan exekveras på flera möjliga sätt, mycket mer effektiv än abstraktion ifrån deterministisk kod. För den deterministiska koden var minskningen också större när antalet Cprogramsatser som abstraherades bort var större jämfört med när antalet var mindre. Vad gäller körningstiderna för TLC när temporala egenskaper kontrollerades var minskningen också större vid abstraktion ifrån ickedeterministisk kod. Körningstiden för TLC var mycket högre vid prövning av en aktivitetsegenskap jämfört med en säkerhetsegenskap.

Application Specific Integrated Circuits (ASIC) and Field Programmable Gate Arrays (FPGA) verification is quite a time consuming phase in design flow cycle and it can be done using methodologies such as Universal Verification Methodology (UVM) and formal verification.The UVM methodology is simulation based verification where in the verifier will have to trigger the Design Under Test (DUT) manually by writing sequences which target different features of the DUT and the verification environment can also have verification directives such as assertions to spot design bugs. Formal verification on the other hand is purely assertion based verification where we describe the expected DUT behaviour using System Verilog Assertion (SVA) and we check for design sanity by exercising the assertions by letting the formal tool drive the inputs to the design in a constrained way. This completely eliminates the need of having to define sequences to drive the inputs. This thesis will bring up formal verification using jasper gold to light and will help verifiers to decide on how much of formal verification methodology can be used in verification of an IP with respect to the complexity of the design and the design behaviour to be verified. The results from this thesis proves how efficient formal verification was with respect to simulation based verification, to stress the design to test for corner case behaviour. The reason why formal verification cannot be extended for Top-Level Verification (TLV) and end to end functional verification is because of design complexity and this was also explored with the help of a complex ethernet design. Finally, a guideline as to when to use simulation based verification and formal verification was formulated. / ASIC och FPGA verifiering är en största del och är en tidskrävande fas av desingflödescyckeln. Det kan man göra den genom UVM eller Formell verifiering metoder.UVM metoder är simulering baserad verifiering där verifieraren måste utlösa DUT genom att skriva sekvenser som rikta olika funktioner av DUT och verifiering miljöer kan också ha verifiering direktiv som assertions som kan upptäcka designbugs.Formal verifiering är en assertion baserad verifiering metoder där i man kan beskriva förväntad DUT uppträdandet genom system verilog assertions (SVA) och verifiera designen genom använder assertions genom att låta det formal driva ingångarna till designen på ett begränsat sätt.Detta eliminerar helt behovet av att behöva definiera sekvenser för att driva ingångarna. Denna examensarbetena kommer att beskriva om formell verifiering med jasper gold och kommer att hjälpa verifierar bestämma hur mycket av den formal verifiering metoden kan man användas för att verifiera en ASIC IP med avseende på komplexitet och design uppträdandet att vara verifierat. Resultaten från denna examensarbetena kommer att bevisa hur effektiv formell metoderna var med avseende på simulering metoder att stressa design och verifiera den för undantags fall.Den ändleding varför formell verifiering metoder kan inte användande för TLV och från början till slut funktion verifiering är på grund av design komplexitet.Detta har analyserats med hjälp av en komplex ethernet design.En riktlinje för när kan man använda simulering metoder och formal metoder var föreslagit.

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.