Probabilistic guarantees in model-checking with Time Petri Nets
| Autor: | Lecart, Manon |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2023 |
| Předmět: | |
| Druh dokumentu: | Text |
| Popis: | 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. |
| Databáze: | Networked Digital Library of Theses & Dissertations |
| Externí odkaz: |
|