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.
Keyword(s)
A PHP Error was encountered
Severity: Notice
Message: Undefined variable: pub_keywords
Filename: front/publication.php
Line Number: 77
Backtrace:
File: /home/prdbpk/public_html/application/views/front/publication.php
Line: 77
Function: _error_handler
File: /home/prdbpk/public_html/application/controllers/Front.php
Line: 221
Function: view
File: /home/prdbpk/public_html/index.php
Line: 315
Function: require_once
A PHP Error was encountered
Severity: Warning
Message: Invalid argument supplied for foreach()
Filename: front/publication.php
Line Number: 77
Backtrace:
File: /home/prdbpk/public_html/application/views/front/publication.php
Line: 77
Function: _error_handler
File: /home/prdbpk/public_html/application/controllers/Front.php
Line: 221
Function: view
File: /home/prdbpk/public_html/index.php
Line: 315
Function: require_once
A PHP Error was encountered
Severity: Notice
Message: Undefined variable: pub_info
Filename: front/publication.php
Line Number: 84
Backtrace:
File: /home/prdbpk/public_html/application/views/front/publication.php
Line: 84
Function: _error_handler
File: /home/prdbpk/public_html/application/controllers/Front.php
Line: 221
Function: view
File: /home/prdbpk/public_html/index.php
Line: 315
Function: require_once