We present a case study where we use automated formal analysis to reason about problem-frame concerns. The descriptions of the problem domains, machine and requirements are written in 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.
展开▼
