The origin of the term "model checking" and the idea itself
is succinctly described in the Q&A with Clarke, Emerson, and Sifakis
in the July 2008 CACM. 

     If a program can be specified in temporal logic, then
     it can be realized as a finite state program --- a program
     with just a finite number of different configurations.
     This suggested the idea of model checking --- to check whether
     a finite state graph is a model of a temporal logic specifications.

This Q&A was based on a preliminary interview with a journalist,
followed by many rounds of polishing and revising by the three Turing Award
winners and the editor until we were all satisfied.

In other words, model checking derives from the Finite Model Property
used in my program synthesis work. A more detailed explanation is
given in [Emerson, "The Beginning of Model Checking", 25MC].