Modeling and testing object-oriented distributed systems with linear-time temporal logic