Engineering and verifying agent-oriented requirements augmented by business constraints with \({\mathcal{B}}\)-Tropos

摘要

We propose \({\mathcal{B}}\)-Tropos as a modeling framework to support agent-oriented systems engineering, from high-level requirements elicitation down to execution-level tasks. In particular, we show how \({\mathcal{B}}\)-Tropos extends the Tropos methodology by means of declarative business constraints, inspired by the ConDec graphical language. We demonstrate the functioning of \({\mathcal{B}}\)-Tropos using a running example inspired by a real-world industrial scenario, and we describe how \({\mathcal{B}}\)-Tropos models can be automatically formalized in computational logic, discussing formal properties of the resulting framework and its verification capabilities.