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 email@example.com 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 firstname.lastname@example.org with the subject line – ‘Internship – V&V’
The lab is headed by R. Venkatesh
Back to Research Area-Software