To know more about TCS Research, email us at

Learn more about

Verification and Validation for Embedded Systems



The Verification and Validation (V&V) group at TCS Innovation Labs – Pune (TRDDC) has designed an innovative ‘towards zero defects’ approach to reduce the risk arising out of software defects. 

Moving Towards Zero Defects
Software defects can lead to loss of valuable time and money, poor customer experience, and even fatal accidents. Therefore, tools and technologies must continuously evolve to find new and existing defects, to improve the overall software quality.

The innovative design  ‘towards zero defects’ approach follows a unique two-step process.  It involves analyzing existing defect detection techniques and developing a tool that uses innovative analysis to identify defect patterns.

Key innovations in verification and validation techniques
The V&V group’s work can be broadly classified into the following areas:

  • Static analysis: The group's core strength is static analysis of the embedded C code. Some key initiatives include precision improvement to reduce the number of warnings generated and program slicing to help model checkers scale faster.
  • Model checking: The V&V group is actively working on new techniques to scale model checking of sequential and concurrent codes. Currently, the focus is on using loop abstractions for overcoming the limitations of bounded model checkers. This will help meet the needs of programs with loops and large bounds, unknown bounds, or those containing large arrays. Verification of synchronously composed systems, development of a systematic approach for timing analysis, and optimization of safety-critical automotive software are other key initiatives.                                                                          
  • Testing: We are exploring new possibilities in the area of testing. Current research is focused on the generation of test cases suitable for functional and structural testing. The group has developed a tool that automatically generates functional test cases based on the pattern matching notation. In the area of structural test data, the focus is on generating test suites for achieving user specified structural coverage criterion for a given embedded system C/C++ code or model.
    Tool development through collaborations

    We collaborate with our clients  in defining research problems, evaluating prototype implementations, and offering product development support. Some of the tools that we have developed to address our clients’ software quality needs are: 
  • TCS Embedded Code Analyzer (ECA): TCS-ECA is a static analysis tool for C/C++ code that detects standard errors and exceptions. Currently, we are exploring ways to combine SAT solving, invariant generation, and abstract interpretation to ensure a higher degree of precision without compromising on scalability.
  • AutoGen: This is an automated test generation tool for C code that  generates test data to satisfy various code coverage criteria including statement, decision, and modified condition/decision coverage (MC/DC). AutoGen has been successfully piloted on industrial size codes.
  • Expressive Decision Tables Tool: This tool generates functional test cases from the requirements written in the expressive decision tables (EDT),  a tabular and easy-to-use specification notation.  The tool has been successfully piloted for specifying requirements and automatically generating functional test cases for over 15 automotive and medical systems of various OEMs and tier-I developers.
  • Loop Abstraction for Bounded Model Checking: LABMC implements a unique loop abstraction technique to scale bounded model checking. Our analysis around the application of LABMC in different industrial applications, detected that 70 percent of the warnings generated by static analyzers were actually false positives. LABMC  also verifies properties on academic benchmarks and industrial applications that no other tools or techniques can analyze.

Access Recent Papers and Publications 

Become a part of  The Verification and Validation (V&V) group at TCS. 

  • Sabbatical: We welcome faculty members interested in verification and validation of safety- and business-critical systems. As visiting researchers, you can gain access to TCS-developed research tools. You will also be able to explore diverse real-world codes as well as engage in research to address major challenges in the field of verification and validation.

Write to us at  with the subject line – ‘Sabbatical - Visiting Researcher – V&V’

  • Internships: The V&V group accepts internship applications from students with a strong inclination for research and development. The internship duration is between two months and one year. If you are excited about this field, mail your resume clearly indicating your interest, past experience, and  preference for the internship duration.

Write to us at  with the subject line – ‘Internship – V&V’

The lab is headed by R. Venkatesh.

Back to Research Area-Software




TCS Embedded Code Analyzer (TCS ECA) is designed to detect all occurrences of certain categories of errors early in the software development cycle and offer complete coverage-based testing, resulting in fewer product defects and, hence, better product quality.

Press Releases

TCS Introduces New Software Assurance Solution Co-Developed with Nissan

TCS ECA has been developed by TCS in collaboration with Nissan Motor Co., Ltd (Nissan) in Japan and is available from distribution partner Yokogawa Digital Computer Corporation. TCS ECA has been designed to combine TCS’ leadership in engineering software solutions and services with Nissan’s expertise in automotive software.