We introduce an interleaving operational semantics for describing the client-observable behaviour of atomic transactions on distributed key-value stores. Our semantics builds on abstract states comprising centralised, global key-value stores and partial client views. We provide operational definitions of consistency models for our abstract states which we show to be equivalent to the well known declarative definitions of consistency model on abstract executions. We explore two applications, verifying that the COPS replicated database and the Clock-SI partitioned database satisfy their consistency models using trace refinement, and proving invariant properties of client programs.