Hos Veidekke Entreprenad AB har det i tidigare projekt visat sig att placeringar av objekt i en 3D-modell inte stämmer överens med dess tänkta placeringar. Enligt en förfrågan av Veidekke undersöks i denna studie felaktiga placeringar av objekt i 3D-modeller för prefabricerade stomelement och el. Specifika objekt som undersöks är eldosor i prefabricerade väggar och eluttag från elprojektör. Syftet med studien är att med hjälp av en regelkontroll i mjukvara för 3D- modellering upptäcka och eliminera fel redan i ett projekts projekteringsstadie. Målet är att utveckla en regelkontroll som efterfrågas av Veidekke att applicera i ett aktuellt projekt, likväl att använda i framtida projekt. Studien har genomförts under tio veckor. Enligt tidigare forskning ligger kostnader för felaktigheter i byggprojekt i spannet 2–6,5 procent av produktionskostnaden. De största möjligheterna att påverka och förebygga kostnader för felaktigheter finns i projekteringsskedet. De mest frekventa orsakerna till fel är misstag, slarv, nonchalans, okunskap och otydliga beställningar. Detta tillsammans med allt mer komplexa tekniska system och högre krav på funktionalitet, miljö, energi och estetik. Från år 1950 fram till millennieskiftet steg installationskostnader från 10 till 50 procent av entreprenadkostnaden. Undersökningar visar att 32 procent av kostnader på grund av felaktigheter uppkommer i projekts tidiga stadie, vid beställning och projektering. Kunskap och motivation är de orsaker till fel som sticker ut mest. Andra betydande orsaker är tidsbrist, ansvarsförskjutning, kostnadsbesparingar och brist i samordning. Användandet av BIM pekas i studien ut som en väsentligt bidragande lösning på att reducera mängden fel i projekteringsskedet som leder till extra kostnader. Kollisioner mellan objekt i handlingar från olika projektörer betraktas som en av de största faktorerna till extrakostnader. Detta kan motverkas genom visualisering i BIM och 3D-modellering, där modell- och kollisionskontroller används för att upptäcka fel. I studiens nulägesbeskrivning redogörs den regelkontroll som utgör mål att utveckla åt Veidekke. Regelkontrollen ska varna BIM-samordnaren då ett eluttag är beläget på ett icke-acceptabelt avstånd från dess tillhörande eldosa inuti en prefabricerad vägg. Regelkontrollen utvecklas och ämnas användas tillsammans med aktörer inom ett av Veidekkes projekt. Regelkontrollen utvecklas i mjukvaran Solibri Model Checker och testas framgångsrikt i en mindre 3D-modell. Information i IFC-filer från en projektör visar sig dock inte vara tillräcklig. Detta åtgärdas genom en beskrivning hur en korrekt export av IFC-filer görs. Regelkontrollen valideras därefter i ett verkligt projekt där faktiska felaktigheter hittas. Enligt intervjustudien ställer sig alla respondenter positiva till BIM-projektering och användandet av modell- och kollisionskontroller, samt att de implementeras och används tidigare i projekt än vad som nu är vanligt. Installationer anses som ett av de områden där flest fel upptäcks och beror enligt respondenterna på ansvarsförskjutning och bristande samordning. Efter genomförande och resultat leder studien till slutsatsen att kostnader kan reduceras om projektering och samordning ägnas mer resurser och tid samtidigt som modell- och kollisionskontroller bör utvecklas och implementeras tidigt i projekt. Regelkontrollen visar sig möjlig att ta fram enligt förfrågan och valideras i ett verkligt projekt. Studien mynnar ut i ett antal rekommendationer åt Veidekke: Mjukvaran BricsCAD rekommenderas framför AutoCAD Architecture för export av IFC-filer från IMPACT Ställa högre krav på metadata i IFC-filer Införa samordning tidigare Tillägna projektering och samordning mer tid och resurser / At Veidekke Entreprenad AB it has in earlier projects shown the positionof objects in a 3D-model do not represent the intended positions. According to an enquiry from Veidekke this study researches incorrect placements of objects in 3D-models for prefabricated structural walls and electrical systems. The study specifically covers electrical conduit boxes inside the prefabricated structural walls and electrical sockets from an electrical design engineer. The purpose of the study is to use a ruleset in 3D-modeling software to detect and eliminate inaccuracies in the design phase of a project. The goal is to elaborate a ruleset that is requested by Veidekke and apply in a current project. According to previous research, cost for errors and inaccuracies in construction projects range from 2 to 6,5 percent of the production cost. The greatest opportunities for influencing and preventing costs for errors and inaccuracies are in the design phase. The use of BIM in the study is identified as a significant contributing solutionto reducing the number of errors in the design phase leading to extra costs. Collisions between objects in drawings from different engineers are considered one of the major factors of extra cost and can be countered by model- and collision checks. The study's current state description describes the ruleset which is the goal of developing for Veidekke. By using the ruleset, it should alert the BIM-coordinator when an electrical outlet is located at an unacceptable distance from its associated electrical conduit box inside a prefabricated wall. The ruleset is developed and intended to be used together with 3D-models from different engineers in one of Veidekke's projects. The ruleset is developed in Solibri Model Checker software and successfully tested in a smaller 3D-model. However, information in IFC files from an engineer does not prove to be sufficient. This is addressed by describing how toproperly export IFC-files. The ruleset is then validated in a real projectwhere actual errors are found. After implementation and results, the study concludes that costs can be reduced if design and coordination are given more resources and time, while model- and collision checks should be developed and implemented early in projects. The rule check proves possible to develop according to the request and also validated in a real project.

Since 2009, Moving Target Defense (MTD) has become a new paradigm of defensive mechanism that frequently changes the state of the target system to confuse the attacker. This frequent change is costly and leads to a trade-off between misleading the attacker and disrupting the quality of service. Optimizing the MTD activation frequency is necessary to develop this defense mechanism when facing realistic, multi-step attack scenarios. Attack modeling formalisms based on DAG are prominently used to specify these scenarios. It represents the attack goal in the root of a tree that is recursively refined into subgoals to show the different ways the attacker can compromise the system. According to some specific models, the tree is augmented with countermeasures, time, costs, or probabilities. Our contribution is a new DAG-based formalism for MTDs and its translation into a Price Timed Markov Decision Process to find the best activation frequencies against the attacker’s time/cost-optimal strategies. For the first time, MTD activation frequencies are analyzed in a state-of-the-art DAG-based representation. Moreover, this is the first paper that considers the specificity of MTDs in the automatic analysis of attack modeling formalisms. Finally, we present some experimental results using UPPAAL STRATEGO to demonstrate its applicability and relevance. / Sedan 2009 har Moving Target Defense (MTD) blivit ett nytt paradigm av defensiv mekanism som ofta ändrar målsystemets tillstånd för att förvirra angriparen. Denna frekventa förändring är kostsam och leder till en avvägning mellan att vilseleda angriparen och att störa målsystemets tillförlitlighet. Att optimera MTD-aktiveringsfrekvensen är nödvändigt för att utveckla denna försvarsmekanism när man står inför realistiska attackscenarier i flera steg. Attackmodelleringsformalismer baserade på DAG är de främst använda metoderna för att specificera dessa scenarier. Metoden representer attackmålet i roten av ett träd som rekursivt förfinas till delmål för att visa de olika sätt som angriparen kan äventyra systemet. Enligt vissa specifika modeller är trädet utökat med motåtgärder, tid, kostnader eller sannolikheter. Vårt bidrag är en ny DAG-baserad formalism för MTD:er och dess översättning till en Price Timed Markov Decision Process för att hitta de bästa aktiveringsfrekvenserna mot angriparens tids-/kostnadsoptimala strategier. För första gången analyseras MTD-aktiveringsfrekvenser i en toppmodern DAG-baserad representation. Dessutom är detta det första rapporten som överväger specificiteten hos MTD:er i den automatiska analysen av attackmodelleringsformalismer. Slutligen presenterar vi några experimentella resultat med UPPAAL STRATEGO för att visa dess tillämpbarhet och relevans.

With the prevalence of technology and computer systems in today’s society, it is crucial to ensure that the systems we use are secure. The fields that study these issues, cybersecurity and cybersafety, use the formal verification technique of modelchecking. This paper tackles one aspect of the work needed to develop model-checking methods as we try to improve the efficiency and the reliability of model-checking techniques using the Time Petri Net model. Formal methods based on Time Petri Nets are not exempt from the state-explosion problem, and we study here different approaches to circumvent this problem. In particular, we show that limiting the exploration of such a model to runs with integer dates maintains the integrity of the model-checking result. We also show that it is possible to set a limit on the number of runs that can be explored while maintaining the probability that the observation is correct above a certain threshold. / Med tanke på hur vanligt det är med teknik och datorsystem i dagens samhälle är det viktigt att se till att de system vi använder är säkra. De områden som studerar dessa frågor, cybersäkerhet och cybersafety, använder den formella verifieringstekniken modellkontroll. Denna artikel tar upp en aspekt av det arbete som krävs för att utveckla metoder för modellkontroll, eftersom vi försöker förbättra effektiviteten och tillförlitligheten hos metoder för modellkontroll med hjälp av Time Petri Netmodellen. Formella metoder baserade på Time Petri Nets är inte undantagna från problemet med tillståndsexplosion, och vi studerar här olika tillvägagångssätt för att kringgå detta problem. I synnerhet visar vi att om man begränsar utforskningen av en sådan modell till körningar med heltalsdatum bibehålls integriteten hos resultatet av modellkontrollen. Vi visar också att det är möjligt att sätta en gräns för antalet körningar som kan utforskas samtidigt som sannolikheten för att observationen är korrekt hålls över ett visst tröskelvärde.

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.