Formal Modeling of a Mail Transport System based on Multi-Agent System-of-Systems
Keywords:
Safety-Critical System, Multi-agent System, System-of-System (SoS), Labelled Transition System (LTS), Correctness, Safety; Liveness, Finite System Processing (FSP)Abstract
The role of multi-agent System-of-Systems (SoS) has become important in modern complex systems. SoS is a composition of systems having constituent elements as independent functional autonomous systems. It is a specialized system with greater complexity having an emergent behavior. We have proposed a methodology centered on formal modeling, model checking, and formal verification of a Mail Transport System based on multi-agent SoS. The proposed multi-agent SoS is a safety-critical system that must be correct, safe, and reliable. It must ensure the safety and liveness properties of correctness. Our objective in this work is to propose a formal methodology that ensures correctness properties of safety and liveness of the Mail Transport System. Our contribution consists of specifying Gaia based formal multi-agent requirement and design specifications, the liveness properties are specified using regular expression and the safety property is specified in first-order predicate calculus. The verification of Gaia safety and liveness properties and Gaia organizational abstractions by Finite State Processes (FSP) and Labelled Transition System (LTS). Then these FSP specifications are modeled in Event-B for creating exhaustive proofs.