Properties are implicitly global: G (...); make sure to use the outer "G"!
Implications: the left-hand side may be too strong → this makes your property more specific and weaker! Extreme case: "antecedent failure": left-hand side is never true, property always holds! Example: G(false → everything is fine)
Timing: The model can be "infinitely fast" but a real system may not be able to react in one "time step" (zenoness) → This requires careful inspection.
Timing: adding more feature may introduce additional transition steps and can break safety properties or liveness properties using "X". This may require changes in the properties to use auxiliary variables or allow something to happen in multiple time steps instead of one step.
False assumptions: Do not assume that physical components are initialized in a specific way, or requests can only be made at certain times.
Requirements Changed
3.4c Safety and security standards for next-generation systems Part 3, Theory