If you’re testing with timers then you’ll want to add the timers to the model itself. After all time is part of your state at that point. You can treat timer calls as a command to generate. This allows you to deterministically control your tests and consequently run them much faster. It also allows you to induce weird failures that you wouldn’t normally see (like firing timers in incorrect orders for instance). I typically do this by shimming the timer module. My SUT uses the shim. In production it’ll use the real timer module. In my tests they’re just dummy calls.

Is that a standard cache?
I am not sure I would use PBT for such case. It makes sense where there is an explosion of different states. In case of cache, there are two: the data is there, or it isn’t.
Other argument for not testing it this way is that usually after deleting the session, you fetch it from the DB or somewhere else. It doesn’t affect how your system behaves to the outside world. It is an implementation detail that can you should leave out of model.
If there is other stuff depending on it, and you want to test it with PBT, you can pass current time to the functions as an argument. That makes it easier to test in general - not only for PBT

That’s not what I had in mind, but those are good points.

Oh that makes sense–thanks.

The example requirement was intended as an explicit feature of the server API. Although clients can’t be sure data isn’t retained longer without being able to audit the running code, they can at least know the server behave as if they have a clean slate after waiting >70s. The PBT would help in case this guarantee ever needed to be audited and help maintain the guarantee as the implementation evolves.

Another potential reason for the requirement is avoiding per connection session data becoming a memory leak.