This paper presents an empirical study of the effectiveness of test cases generated from UML state diagrams using transition coverage as the testing criterion. The test cases production is mainly based on an adaptation of a probabilistic method, called statistical testing based on testing criteria. This technique was automated with the aid of the Rational Software Corporation's Rose Rea Time tool. The test strategy investigated combines statistical test cases with (few) deterministic test cases focused on domain boundary values. Its feasibility is exemplified on a research version of an avionics system implemented in Java: the Flight Guidance System case study (14 concurrent state diagrams). Then, the results of an empirical evaluation of the effectiveness of the created test cases are presented. The evaluation was performed using mutation analysis to assess the error detection power of the test cases on more than 1500 faults seeded one by one in the Java source code (115 c asses, 6500 LOC). A detailed analysis of the test results allows us to draw first conclusions on the expected strengths and weaknesses of the proposed test strategy.