Evaluation of Maude as a Test Generation Engine for Automotive Operating Systems

This work evaluates Maude, an expressive and executable algebraic specification language, as a potential test sequence generation engine in the context of constraint-based test sequence generation for automotive operating systems. Our approach defines requirement specifications for automotive operating systems compliant with the OSEK/VDX international standard, and specifies constraint patterns in Maude. The correctness of the Maude specification is verified using LTL model checking and the test sequences from each classified environment are generated using reach ability computation provided by the Maude rewriting engine. Experimental evaluation shows that constraint-based test generation using Maude can be as effective as that of using NuS MV, a state machine based specification language specialized for model checking and specification-based testing, but more expressive and flexible.