Automatic Generation of Software Behavioral Models