In this paper we present a novel approach to reduce the effort for creating the model and facilitate its appliance in industry. We stick to the foundations of constructive enumeration to create a complete, traceably correct, and consistent model, but we do first decompose the task into manageable units by input/output dependency analysis. The expected behavior is formalized in temporal logic. The resulting model is a composition of all models, that run in parallel. As time is explicitly considered during the creation of the model, timing information is available for structured testing of non functional, e.g. real time requirements, as well as for the determination of measures and dependability estimators.
By this approach, the subsequent activities for quality assurance, such as validation and verification, measurement of coverage criteria, and dependability estimators, e.g. of reliability, safety, and risk, profit from this approach, as they rely on a provably correct basis. We applied the method to an embedded system of a German automotive OEM, that was designed in Matlab Simulink and architectured with AUTOSAR 3.2 methodology. An existing test suite was at hand, that was created with the established method. This existing test suite served as benchmark to assess the quality of the new test suite, derived from the model. We compared the reachability of the test cases inside the implementation with code coverage measures and examined the variance of use imposed by the test suites. We present the promising results in this paper.