Abstract
Dynamically adaptive multi-agent systems (DAMS) consist of multiple agents that adapt to changing system and environmental conditions in order to achieve collaborative goals. As DAMS are found in applications across various domains, ensuring the correct and safe adaptations of DAMS has become more important. Formal verification techniques such as model checking present a promising approach to guaranteeing the correctness of a software system with respect to certain system requirements. Previous works on formal verification for dynamically adaptive system or multi-agent system, however, have not addressed the runtime and collaborative nature inherent to DAMS operations. This work proposes a runtime verification framework for DAMS (DAMS-RV) based on an adaptive feedback loop, which is activated for each adaptation that system makes after a change in the system or environment. The proposed framework is described using a collaborative nurse agent system as a running example. A case study with an application scenario provides insights into how DAMS-RV can serve as a feasible and effective framework for DAMS verification.