Search

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.

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.

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.

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 report discusses the foundations of the VO approach. Then, it explores multiple directions and argues about structure and applications.