A modelling framework I've actually tried using is Leslie Lamport's system of temporal logic, known as TLA. It has a web page accessible here. To me, it made good sense on the whole. The key idea is that specifications are certain sets of infinite state sequences. These sets are closed under finite repetition of states, or stuttering, `skip' steps. (And deletion of such steps.) This is a view of systems evolving discretely in time. It is as if we are interested in systems which can be completely "filmed", where the shutter speed is fast enough to take a picture at least as often as the system changes state.
The specifications (stutter-closed sets of state-sequences) are written using formulas of a temporal logic of a designedly weak form. This form is incapable of expressing predicates which are sensitive to stuttering steps. The formulas are conjunctions of a safety property, and a fairness property. The safety property tells you what you can rely on not happening: topologically it is a closed property -- the paradigm example is freedom from deadlock. The fairness property tells you what you can rely on happening; topologically it is a dense property -- an example is infinitely many "up"-steps in a well-ordering.
The restricted form of specifications in TLA short-circuits senseless `psychologistic' or mataphysical distinctions between systems which don't differ in any way an implementer or user could care about.
The distinction between what you can rely on happening and what you can rely on not happening is comparable to the distinction between sins of omission and sins of comission. Thinking of the 10 commandments, there is "Remember the Sabbath", to sin against which is a sin of o-mission; and there are the various "Thou shalt nots", to sin against which would be a sin of co-mission. The 10 commandments are of course a very famous behavioural specification.
In Lamport's framework, a design step (from a high level abstract statement, to a more concrete and implementation oriented statement) is verified by proving an implication between temporal formulas of a particular circumscribed form. The proof of that implication is the solid content of the design step.
To prove such an implication, you can often just define a function (called a refinement mapping) from states of the low-level system to the states of the high level system. This function is, so to speak `static'. However, you may need to add special auxiliary variables to the concrete state, to account for the `dynamics' of the abstract system. Lamport and Abadi in SRC report 29, The Existence of Refinement Mappings (from 1988) divide these auxiliaries into history variables (that record the history of the concrete system), stuttering variables (that control its present internal activity), and prophecy variables (that oracularly predict its future). They are `there' so that the simulation relation can be single valued: hidden variables.
It is not clear to me what the implications are of restricting refinement relations to be functions, i.e. single valued. This seems to involve the idea of equality between states, and not just state variables. As I understand it, a refinement mapping is just a particularly well-behaved kind of simulation relation, where the concrete state is rich enough to uniquely determine the abstract state.
A noteworthy plank in Lamport's philosophy is the idea that `one state-space does for all'. As it were, you should think about states of the universe, not about states of any particular part of it. Seemingly, this has solid implications in terms of combining and comparing specifications. He also distinguishes clearly between `closed system' and `open system' specifications; the latter involve a system communicating with an environment using an interface.
There is a particularly entertaining TLA paper about refinement and auxiliary variables among Lamport's writings here. It features a acid-casualty mathematician and a 60's style bed-side radio. (There is one by my own bed.) The story revolves around the clock's jumping from 10:59 via 11:59 or 10:00 to 11:00.