Combining agent-oriented conceptual modelling with formal methods

Agent-oriented conceptual modelling notations such as i* have received considerable recent attention as a useful approach to early-phase requirements engineering. Agent-oriented conceptual modelling notations are highly effective in representing requirements from an intentional stance and answering questions such as what goals exist, how key actors depend on each other and what alternatives must be considered. Formal methods such as those based on the Z notation offer a complementary set of representational facilities. We explore how these two otherwise disparate approaches might be used in a synergistic fashion.