How to define the Atomic Propositions in Model Checking

Question

The atomic propositions in Symbolic Model Checking form the state in the state-transition graph (the model $\mathcal{M}$ in Model Checking). The other part of Model Checking is the specification, which is usually some sort of temporal logic formula over the atomic propositions in the model.

My question is about the atomic propositions themselves. I have only seen a few rudimentary examples of them, such as $x = 20$ or $printer is busy$. These atomic propositions (I think) are stating a fact about the state of the program at that point in the system. You then use a temporal logic formula to see if the model holds under it. I am confused by how the atomic propositions are both defined and used.

First, how they are defined. I haven't seen anywhere a description on how you define these atomic propositions. That is my first question. I don't understand how stating $x > 100$ in a state in the model $\mathcal{M}$ means anything. I didn't have to prove it or anything. It was just stated as fact. Then the temporal logic formula comes along and is checked against it, but there's some disconnect there for me. The value was never proven correct in the first place. It's as if, in my program, I make an HTTP request and during the waiting period before a response, my atomic proposition is that $\mathtt{the\ sky\ is\ blue}$. Wondering why was it put there, how do I know that it is true. A better atomic proposition would be $\mathtt{the\ request\ was\ sent}$. But again, I don't see how the program/model/checker "knows" this. I don't see what is doing the verification that that statement is true.

So my question is basically, how you define atomic propositions in Symbolic Model Checking. What goes into them. How you are allowed to make such statements that seemingly aren't verified. I don't see how I can say anything about the state of the program without something else "checking" that yes $\mathtt{the\ request\ was\ actually\ sent}$. I understand that after we define this model, we have our specification formulas and check them against the model. But we never checked the model itself for accuracy, is what I'm trying to get at.

I feel like, after writing down, in a specific state, an atomic proposition, I would then need to write a unit test to verify that it was true for some input. Not sure what I'm missing.