Abstract: Model-based development is increasingly becoming the method of choice for developing embedded systems for applications in automotive and aerospace industries. It relies on tool-suites consisting of a variety of tools including model-processing tools like simulators, model-translators and code-generators. Correctness of these tools used in the development process is a key requirement for safety critical applications. This work proposes a novel testing methodology for the rigorous verification of model processing tools.

The proposed methodology generates test-models, and test-inputs for testing model processing tools. It takes as input the syntactic and semantic meta-model of modeling language, expressed in the form of inference-rules, and using coverage criteria over this meta-model, generates test-models and test-inputs for these test-models. Apart from testing syntactic aspects of the translation, our test-generation aims to test subtle semantic interactions of the modeling language that are potentially mis-translated by model-processing tools.

We illustrate the methodology with a simple prototypical process-calculus, and report on experimentation we have carried out with Stateflow, which is a variant of hierarchical state-machines implemented in the Matlab/Simulink toolset.

S. Ramesh has more than 15 years of research experience in the areas of high level language design, validation and verification of distributed systems, embedded software and hardware designs. Currently he is a technical fellow at the General Motors India Science Laboratory in Bangalore. As a technical fellow, he plays a key role in setting up a Centre of Excellence in rigorous control software engineering for automotive embedded systems. As part of this Centre, he is involved in directing a group of young researchers in devising and developing rigorous methods and tools for model-based development and verification of distributed embedded software. Earlier, he was a full Professor in the Dept of Computer Science and Engineering, Indian Institute of Technology, Bombay. At IIT Bombay, he was also the head of the Centre for Formal Design and Verification of Software which he co-founded. As part of this centre activities, he carried out many industry-sponsored projects on verification of hardware and embedded software. S. Ramesh has been involved in many international collaborative research projects. This include Indo-French and Indo-US projects and some Australian Research Council projects involving researchers from INRIA, Sophia Antipolis, France, Technical University of Eindhoven, The Netherlands, University of New South wales, Sydney, Australia, University of Auckland, New Zealand and SUNY, Stony Brooks, USA. He was involved in many industrial projects funded by various Governmental organizations and private companies which include Bhabha Atomic Research Centre (BARC), Vikram Sarabhai Space Centre (VSSC), Aeronautical Development Agency (ADA) and Texas Instruments India. Appointments: dcm@cs.cmu.edu