Using the ConGolog and CASL Formal Agent Specification Languages for the Analysis, Verification,and Simulation of i~* Models

摘要

This chapter describes an agent-oriented requirements engineering approach that combines informal i~* models with formal specifications in the multiagent system specification formalisms ConGolog and its extension CASL. This allows the requirements engineer to exploit the complementary features of the frameworks, i~* can be used to model social dependencies between agents and how process design choices affect the agents' goals. ConGolog or CASL can be used to model complex processes formally. We introduce an intermediate notation to support the mapping between i~* models and ConGolog/CASL specifications. In the combined i~*-CASL framework, agents' goals and knowledge are represented as their subjective mental states, which allows for the formal analysis and verification of, among other things, complex agent interactions and incomplete knowledge. Our models can also serve as high-level specifications for multiagent systems.