Change Impact Analysis for Rebel Specifications
Summary
The formal specification language Rebel is designed for the unambiguous derivation of source code in a provably correct way. As requirements change over time, specifications must be updated. Modifications may impact the state space defined by variables and values, in an undesired way. Being the largest bank of the Netherlands, ING can not permit any losses in continuity and data as a result of unexpected code behaviour. Therefore Rebel is used to model their financial entities. The changeability of specifications must become well-defined in order to incorporate the language in its entirety. Using formal methods, this study attempts to provide insights in the impact of a change to a Rebel specification.