The importance of starting in a good place

Formal arguments for CPS certification depend on modeling the CPS and formally verifying the CPS. The correctness properties that we are interested in formally verifying are typically quite diverse (e.g., prove correct timing, prove that no message is lost, prove that assertions in source code are true). Consequently, it is typically not possible to state a single model of the system and state all correctness properties in a single language and then perform the verification. Instead, it is typically necessary to create different verification models for different correctness properties, and then for each verification model invoke a formal verification tool that proves the correctness properties related to this verification model. When doing so, however, there may be dependencies between different formal verification methods/tools; thus, the guarantee provided by one formal verification method/tool may be an assumption for another formal verification method/tool. Thus, there may be dependencies between analyses. Such dependencies may be circular. In this paper, we show that for such formal verification with circular dependencies, the outcome may depend on initial assumptions, hence illustrating the importance of starting in a good place.