An Automated Verification Method for Distributed Systems Software Based on Model Extraction