Rigorous model-based design & verification flow for in-vehicle software

The development of in-vehicle software, often controlling safety-critical functions related to braking, steering and transmission systems, requires rigorous techniques to ensure high-integrity and reliability requirements. Formal models of requirements and design artifacts based on state-transition systems and other formalisms serve as a means to apply rigorous analysis and verification techniques at every stage in the development process. We present here one such formal analysis and verification flow, developed at General Motors R&D, provide an overview of methods for automatic test generation based on mathematical modeling and discuss the future directions for research.