A Formal Specification of the PVM Architecture