-
Validation-Driven Development
Authors:
Sebastian Stock,
Atif Mashkoor,
Alexander Egyed
Abstract:
Formal methods play a fundamental role in asserting the correctness of requirements specifications. However, historically, formal method experts have primarily focused on verifying those specifications. Although equally important, validation of requirements specifications often takes the back seat. This paper introduces a validation-driven development (VDD) process that prioritizes validating requ…
▽ More
Formal methods play a fundamental role in asserting the correctness of requirements specifications. However, historically, formal method experts have primarily focused on verifying those specifications. Although equally important, validation of requirements specifications often takes the back seat. This paper introduces a validation-driven development (VDD) process that prioritizes validating requirements in formal development. The VDD process is built upon problem frames - a requirements analysis approach - and validation obligations (VOs) - the concept of breaking down the overall validation of a specification and linking it to refinement steps. The effectiveness of the VDD process is demonstrated through a case study in the aviation industry.
△ Less
Submitted 11 August, 2023;
originally announced August 2023.
-
Trace Refinement in B and Event-B
Authors:
Sebastian Stock,
Atif Mashkoor,
Michael Leuschel,
Alexander Egyed
Abstract:
Traces are used to show whether a model complies with the intended behavior. A modeler can use trace checking to ensure the preservation of the model behavior during the refinement process. In this paper, we present a trace refinement technique and tool called BERT that allows designers to ensure the behavioral integrity of high-level traces at the concrete level. The proposed technique is evaluat…
▽ More
Traces are used to show whether a model complies with the intended behavior. A modeler can use trace checking to ensure the preservation of the model behavior during the refinement process. In this paper, we present a trace refinement technique and tool called BERT that allows designers to ensure the behavioral integrity of high-level traces at the concrete level. The proposed technique is evaluated within the context of the B and Event-B methods on industrial-strength case studies from the automotive domain.
△ Less
Submitted 28 July, 2022;
originally announced July 2022.
-
Application of Validation Obligations to Security Concerns
Authors:
Sebastian Stock,
Atif Mashkoor,
Alexander Egyed
Abstract:
Our lives become increasingly dependent on safety- and security-critical systems, so formal techniques are advocated for engineering such systems. One of such techniques is validation obligations that enable formalizing requirements early in development to ensure their correctness. Furthermore, validation obligations help hold requirements consistent in an evolving model and create assurances abou…
▽ More
Our lives become increasingly dependent on safety- and security-critical systems, so formal techniques are advocated for engineering such systems. One of such techniques is validation obligations that enable formalizing requirements early in development to ensure their correctness. Furthermore, validation obligations help hold requirements consistent in an evolving model and create assurances about the model's completeness. Although initially proposed for safety properties, this paper shows how the technique of validation obligations enables us to also reason about security concerns through an example from the medical domain.
△ Less
Submitted 7 July, 2022;
originally announced July 2022.
-
Formalization of Advanced VOs semantics and VO Refinement
Authors:
Sebastian Stock,
Fabian Vu,
David Geleßus,
Atif Mashkoor,
Michael Leuschel,
Alexander Egyed
Abstract:
This document lays out the foundations for VO and requirement refinement, abstractions of models, and instantiations. Also, VOs on abstractions and instantiations are considered.
This document lays out the foundations for VO and requirement refinement, abstractions of models, and instantiations. Also, VOs on abstractions and instantiations are considered.
△ Less
Submitted 18 May, 2022;
originally announced May 2022.
-
IVOIRE Deliverable 1.1: Classification of existing VOs & tools and Formalization of VOs semantics
Authors:
Sebastian Stock,
Fabian Vu,
Atif Mashkoor,
Michael Leuschel,
Alexander Egyed
Abstract:
This report discusses the foundations of the VO approach. Then, it explores multiple directions and argues about structure and applications.
This report discusses the foundations of the VO approach. Then, it explores multiple directions and argues about structure and applications.
△ Less
Submitted 12 May, 2022;
originally announced May 2022.
