Abstrakt. Ett säkerhetsanspråk för ett system är en uppgift om att systemet, som är föremål för farliga villkor, uppfyller en viss uppsättning av egenskaper. Efter arbete av John Rushby och Bev Littlewood presenterar denna uppsats ett matematiskt ramverk som kan användas för att ange och formellt bevisa probabilistiska säkerhetspåståenden. Det gör det också möjligt att integrera farliga förhållanden, deras osäkerheter och deras interaktioner i säkerhetspåståendet. Detta ramverk ger en formell beskrivning av den probabilistiska sammansättningen av ett godtyckligt antal farliga förhållanden och deras effekter på systemets beteende. Ett exempel ges på ett probabilistiskt säkerhetsanspråk för en algoritm för upptäckt av konflikter för luftfartyg i ett 2D-luftrum. Motivet för att utveckla detta matematiska ramverk är att det kan användas i ett automatiserat teoremtest för att formellt verifiera säkerhetspåståenden.
Till skillnad från vårt tillvägagångssätt har dessutom den matematiska ramen för REF ännu inte formaliserats i ett teoremtest.
Formalizing Probabilistic Safety Claims ⋆
{'venue': 'NASA Formal Methods', 'journal': None, 'mag_field_of_study': ['Computer Science']}