Formal Specification of Substitutability Property for Fault-Tolerance in Reactive Autonomic Systems
Heng Kuang, Jamal Bentahar, Olga Ormandjieva, Shafieidizaji Nassir, Stan Klasa · Frontiers in artificial intelligence and applications · 2010
Multi-Agent Systems (MAS) have been widely proposed and applied to various application domains, such as space exploration missions. MAS can offer greater redundancy, efficiency, and scalability; however, they also raise new challenges, for instance, complex and often unexpected emergent group behavior, which require a formal specification as well as verification. Therefore, we have proposed a formal approach, named Reactive Autonomic Systems Framework (RASF), based on category theory to tackle those challenges. In this paper, we focus on the formal specification of substitutability property for the fault-tolerance and illustrate our approach through a Mars-world case study implemented as MAS using JADEX.