Automated behavior modeling for verifying safety-relevant modules
Vladislav Nenchev · 2021
Despite employing state-of-the-art safety mechanisms, the intractable variety of possible dynamical behaviors requires automating verification in safety-relevant domains like automated driving. This paper proposes an automatic modeling approach for safety-relevant modules amenable to verification of formal requirements. A logical predicate abstraction is imposed over the module’s inputs and outputs. By stimulating the module with possible finite input sequences, an approximate behavior model is obtained. The approximation accuracy can be improved by increasing the trace length. Then, the satisfaction of the specification is evaluated by model checking in an iterative manner, as shown for the implementation of an automated driving system supervisor.