Validation and verification of Web services choreographies by using timed automata