Formal Modelling and Reasoning on Assurance Cases Expressed with GSN in Event-B
摘要
An Assurance Case (AC) is a structured argumentation for certification describing how industrial activities support system requirements. The most widely used notation for AC is the Goal Structuring Notation (GSN), which provides a graphical representation of argument structures. Despite the advances in the definition of a methodology for developing AC using the GSN, establishing the soundness of ACs relies essentially on experts reviews. Indeed, the lack of rigorous semantics for the GSN hinders the application of formal methods to check the consistency of ACs. The objective of our work is to design a logical (i.e., proof-based) framework supporting the definition of formalised ACs, in order to assist system designers and certification authorities in building goal structures and checking their consistency with respect to the formalised semantics and domain knowledge model that formalises system-specific concepts. The proposed framework will be grounded in the Event-B method and associated algebraic theories.