Looking for a book that derives and constructs a model checking application
John Harrison's book is an exception in going all the way from theory to practice and making all the source code available. I think you will find it difficult to find an equivalent book for model checking, but there are a few that achieve a close approximation.


Principles of Model Checking by Baier and Katoen contains a lot of examples and pretty detailed algorithmic description.
The SPIN Model Checker by Gerard Holzmann is a very different treatment from the author of one of the earliest model checkers. He has maintained the tool for about thirty years and has a "programmatic" approach.


A better bet may be to follow the course notes and lab assignments of some courses available online. At least you will find the theory, practice and examples, even though they are not organised in a book.


Edmund Clarke's course in CMU has a reading list which includes tutorials for a few different model checkers.
Joost-Pieter Katoen's software verification course and the followup on Practical Model Checking and Advanced Model Checking cover a lot of ground.


Finally, this is not entirely what you asked for, but since you have been studying logic and now model checking, you will invariably run into references to abstract interpretation, which is the basis of static program analysis and is intimately connected to model checking (though this connection is not always explicit in the model checking literature). 


Patrick Cousot's MIT Course is a tour de force covering everything from lattice theoretic foundations to the complete implementation of a static analyzer for a simple language. His course material includes all the code and exercises.