Checking Correctness of Transactional Behaviors