Modeling and verification of a telecommunication application using live sequence charts and the Play-Engine tool