Property checking
	• Domain independent properties – Deterministic state transitions – Function consistency • Domain dependent – Output agreement – Safety properties • We used SMV to investigate some of these properties on TCAS’ Own_Aircraft module