The other thing you can do is composition of individually-verified parts. In your example, you make tests that really exercise the shutdown function. Also, note

The other thing you can do is composition of individually-verified parts. In your example, you make tests that really exercise the shutdown function. Also, note any preconditions these functions need to meet so the application calling it can be consistent with specs. From there, just assume shutdown works if used within the tested spec. This method also encourages reusing working specs, code, and tests. We see that in DO-178C with the RTOS’s, etc.