Stateflowmodels are used for describing logic and implementing state machines in modern safety-critical software. However, the complete Stateflowmodelling language is hard to formally define, therefore a subset relevant for industrial models has been developed in previous works. Proving that the execution of Stateflow models satisfies certain safety properties is intractable in general. However, bounded model checking (BMC) can be used to either prove that safety properties are satisfied up to a bounded execution depth, commonly referred to as the reachability diameter, or find a concrete counterexample. One particular safety property of interest is an invariant property. This thesis project contributes with the following. A bounded model checking tool based on symbolic execution has been developed and is called Stateflow Model Verification Tool (SMVT). This tool has been tested on synthetic models and industrial models. The performance of Stateflow Model Verification Tool (SMVT) has been measured, but not compared against the Simulink DesignVerifier (SLDV) due to licensing issues. The study has shown that many industrial models share a similar model structure. Furthermore, it has been shown that SMVT can perform well for several models. / Stateflow-modeller används för att beskriva logik and implementation av tillståndsmaskiner i modern säkerhetskritisk mjukvara. Det kompletta Stateflowspråket är väldigt komplext, och därför har forskare tidigare definierat en begränsad version av språket relevant för industriella modeller. Bevisning att exekvering av Stateflow-modeller måste uppfylla säkerhetsegenskaper, är svårlösligt rent generellt. Begränsad modellprovning kan användas antingen för att bevisa att säkerhetsegenskaper uppfylls till ett begränsat exekveringsdjup, eller för att hitta ett motexempel. En väldigt viktig säkerhetsegenskap kallas för invariant. Detta examensarbete bidrar med följande. En begränsad modellprövare baserad på symbolisk exekvering har utvecklats och kallas för SMVT. Detta verktyg har blivit testat på syntetiska modeller samt industriella modeller. Prestandan har blivit mätt, men på grund av Simulink Design Verifier (SLDV) licens har ingen jämförelse kunnat göras. Studien har visat att många industriella modeller delar samma modellstruktur. Vidare har det utvecklade verktyget SMVT visats prestera väl för flertalet modeller.

Security protocols are ubiquitously used in various applications with the intention to ensure secure and private communication. To achieve this goal, a mechanism offering reliable and systematic protocol verification is needed. Accordingly, a major interest in academic research on formal methods for protocol analysis has been apparent for the last two decades. Such methods formalize the operational semantics of a protocol, laying the base for protocol verification with automatic model checking tools. So far, little work in this field has focused on protocol standardization. Within this thesis a security analysis of a novel Authenticated Key-Exchange (AKE) protocol for secure association handover between two Long-Term Evolution (LTE) base stations (which support dual-connectivity) is carried out by applying two state-of-the-art tools for automated model checking (Scyther and Tamarin Prover). In the course of this a formal protocol model and tool input models are developed. Finally, the suitability of the used tools for LTE protocol analysis is evaluated. The major outcome is that none of the two applied tools is capable to accurately model and verify the dual-connectivity protocol in such detail that it would make them particularly useful in the considered setting. The reason for this are restrictions in the syntax of Scyther and a degraded performance of Tamarin when using complex protocol input models. However, the use of formal methods in protocol standardization can be highly beneficial, since it implies a careful consideration of a protocol’s fundamentals. Hence, formal methods are helpful to improve and structure a protocol’s design process when applied in conjunction to current practices. / Säkerhetsprotokoll används i många typer av applikationer för att säkerställa säkerhet och integritet för kommunikation. För att uppnå detta mål behövs en behövs mekanismer som tillhandahåller pålitlig och systematisk verifiering av protokollen. Därför har det visats stort akademiskt intresse för forskning inom formell verifiering av säkerhetsprotokoll de senaste två decennierna. Sådana metoder formaliserar protokollsemantiken, vilket lägger grunden till automatiserad verifiering med modellverifieringsverktyg. Än så la¨nge har det inte varit stort focus på praktiska tilla¨mpningar, som t.ex. hur väl metoderna fungerar för de problem som dyker upp under en standardiseringsprocess. I detta examensarbete konstrueras en formell modell för ett säkerhetsprotokoll som etablerar en säkerhetsassociation mellan en terminal och två Long-Term Evolution (LTE) basstationer i ett delsystem kallat Dual Connectivity. Detta delsystem standardiseras för närvarande i 3GPP. Den formella modellen verifieras sedan med bästa tillgängliga verktyg för automatiserad modellverifiering (Scyther och Tamarin Prover). För att åstadkomma detta har den formella modellen implementerats i inmatningsspråken för de två verktygen.  Slutligen ha de två verktygen evaluerats. Huvudslutsatsen är att inget av de två verktygen tillräckligt väl kan modellera de koncept där maskinstödd verifiering som mest behövs. Skälen till detta är Scythers begränsade syntax, och Tamarins begränsade prestanda och möjlighet att terminera för komplexa protokollmodeller. Trots detta är formella metoder andvändbara i standardiseringsprocessen eftersom de tvingar fram väldigt noggrann granskning av protokollens fundamentala delar. Därför kan formella metoder bidra till att förbättra strukturen på protokollkonstruktionsprocessen om det kombineras med nuvarande metoder.

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.

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.

Företag som utvecklar produkter strävar mot att korta ner sin utvecklingstid för att kunna bibehålla konkurrenskraft samt snabbare realisera vinster. Parallellt har den tekniska utvecklingen resulterat iatt produkters komplexitet ökat. Det har medfört att osäkerheten i början av projekt och beroendet mellan utvecklingsaktiviteter ökat. Resultatet av detta blir större svårigheter att effektivt och adekvat planera utvecklingsprojekt och sätta deadlines. Syftet med denna rapport är att undersöka vad som påverkar och försvårar planering för ett produktutvecklande företag samt hur det påverkar produktutvecklingstiden. Inledningsvis utfördes en litteraturstudie vilken utgjorde grunden för vår intervjuguide. Datainsamling genomfördes sedan med stöd av intervjuguiden på ett företag som utvecklar komplexa produkter. Utifrån insamlad data identifierades svårigheter och faktorer som påverkar produktutvecklingen. Tillföljd av resultatets omfång krävdes en fördjupad litteraturstudie för att kunna jämföra resultat med teori. Övergripande svårigheter och faktorer som identifierades och analyserades var tidplan, målsättning, formella metoder och aktiviteters beroende av varandra. Resultatet stämmer i stor utsträckning överens med den teori som presenteras om ämnet i rapporten. De utmaningar man bör förhålla sig till när man planerar för utveckling av komplexa produkter är främst hantering av målsättningar och beroende aktiviteter. Utan tydliga mål och en dynamisk process riskerar utvecklingen att fortlöpa längre än den behöver. Slutligen bör företag som utvecklar komplicerade produkter sträva efter en formell metod utvecklad specifikt för det egna företaget, så att framgångsrika projekt enkelt kan upprepas. / Companies that develop products strive to shorten their development time to maintain competitiveness and realize profits faster. Simultaneously, technical development has resulted in an increase in the complexity of products. This has meant that the uncertainty at the beginning of projects and the dependence between development activities has increased. The result of this will be greater difficulties in efficiently and adequately planning development projects and setting deadlines. The purpose of this report is to examine what affects and complicates planning for a product development company and how it affects product development time. Initially, a literature study was conducted, which formed the basis for our interview guide. Data collection was then carried out with the support of the interview guide at a company that develops complex products. Based on the collected data, difficulties and factors affecting product development were identified. Due to the scope of the results, an in-depth literature study was required to be able to compare results with theory. Overall difficulties and factors that were identified and analyzed were schedule, objectives, formal methods, and activities' interdependence. The results are largely in line with the theory presented on the subject in the report. The challenges that should be considered when planning for the development of complex products are mainly management of objectives and dependent activities. Without clear objectives and a dynamic process, development risks taking longer than it needs to. Finally, companies that develop complex products should strive to use a formal method developed specifically for their own company, so that successful projects can be easily repeated.