Formal specification and proof of Gridjack

Good computational model design has always been a key factor in determining whether it will be a successful system. A new approach was proposed to formally specifying and proving the Gridjack computational model design which uses architectural description language WRIGHT together with the process algebra CSP. Formal specification in WRIGHT provides a convenient way to modeling the complex overall structure by describing the interfaces and computations of the component combination. Furthermore, the model was easily proved in terms of laws of the CSP operators by defining the hidden actions of component processes with model-checking tool FDR. This approach can also be applied to formalization of other computational models, which is helpful to rapidly check the model features and revise the design.