Suggestion for formally Verification of partially specified safety-critical Automotive Systems

Abstract:
Automotive Systems are expanding more and more to huge, complex, modular, adaptive and diverse supersystems (hybrids) executing synchronous and asynchronous operations in multi-mode using lots of processors. They are composed of components (subsystems) with certain topological properties themselves being composed to hybrids. In doing so, particularly for safety systems, the warranty of consistency, reliability and reproducibility for process run of the hybrid and all of its subsystems has a high priority. One famous common technique for handling such complex systems is the divide-and-conquer approach. In this paper we show a road map for successively dividing a system component based on its given structural properties into its substructures, and provide several intuitive and formal approaches to recompose the component behavior again from its substructures. Each dividing granularity and connectivity provides specific information about safety, stability and reliability of the component structure under operation. We classify and discuss behavioral model and stability criteria on bases of a use-case, present results to formally extract structure-weaknesses and discuss the safety aspects also involving the analog properties of the structure like multivalued information flow, propagation time and superpositions leading to information corruptness.