Specification and Verification of the PowerScaleTM Bus Arbitration Protocol: An Industrial Experiment with LOTOS