An approach to formal automated analysis of problem-frame concerns

We present an approach to performing automated formal analysis of the concerns found in descriptions that follow the problem-frames technique. The descriptions of the problem domains, machine and requirements are written in a formal language. The approach is explained through a case study using the Alloy language. We show that an evaluation of results and counter-examples provided by a model checker can reveal useful information that can help remove inconsistencies as well as composition errors.