Whence formulae?
	• Jaffe, Leveson et al. developed criteria that specifications of embedded real-time systems should satisfy, including: – All information from sensors should be used – Behavior before startup, after shutdown and during off- line processing should be specified – Every state must have a transition defined for every possible input (including timeouts) • Predicates on the transitions must yield deterministic behavior • Essentially a check-list, but a very useful one