I suspect the following isn't what you wanted, but it does fit the wording in the question: "an explicit procedure that constructs a model of ZFC from any model of S." Let S be Peano arithmetic (PA) plus the axiom "ZFC is consistent" (Con(ZFC)). The proof of G"odel's completeness theorem can be formalized in PA. Under the additional hypothesis of Con(ZFC), it produces $\Delta^0_2$ formulas $U(x)$ and $E(x,y)$ that interpret ZFC. (This means that, in PA + Con(ZFC), one has proofs of all the formulas obtained from ZFC axioms by replacing $x\in y$ by $E(x,y)$ and restricting all quantifiers to range only over things that satisfy $U$.) Thus, given any model M of PA + Con(ZFC), one obtains a model M* of ZFC by taking as its underlying set the set of elements that satisfy $U$ in M and by taking as its membership relation the set of pairs that satisfy $E$ in M. The formulas $U$ and $E$ could in principle be written out explicitly just by following the usual (Henkin) proof of the completeness theorem (but I do not volunteer to do this explicit writing). So these formulas give an explicit procedure for converting models M of PA + Con(ZFC) into models M* of ZFC.
A few additional comments: (1) There's nothing special about ZFC here. The same works for any arithmetically definable theory T, except that the formulas $U$ and $E$ will not be $\Delta^0_2$ but merely $\Delta^0_2$ in T. (2) In general, the definition of "interpretation" should also require provability of $\exists x\,U(x)$; I left it out because, in the case of ZFC, it follows from the interpretation of the axiom of infinity. (3) I suspect that the intention of the question was not something like this but rather that S should be a set theory and that the given and constructed models should agree as to the membership relation. Nevertheless, given that the question allowed other sorts of examples, it seemed worthwhile to point this one out. Note that, if you merely want S to be a set theory but don't care whether the membership relations agree, then what I wrote above still works with the theory of finite sets (ZF with the axiom of infinity replaced by its negation) in place of PA; the two are essentially equivalent.