A Formal Model for English Auction Protocol

Formal methods are commonly used to model complex behavior of a system without ambiguities and specification errors. This paper presents a formal model of the multi-agent requirements using finite-state automata (FSA). We describe application of formal methods to model multi-agent systems using the example of English Auction Protocol (EAP). It is shown that the proposed approach increases the behavior handling and semantic characterization. The use of a formal specification language such as Z ensures the correctness, reliability and consistency at the analysis and design stage. This is because capturing the errors and inconsistencies at initial stages could greatly affect the time and cost spent in later stages of the system development lifecycle. We also show that our formal model of the EAP incorporates security properties such as anonymity, traceability and unforgeability.