The questions you ask are actually quite different.
However, I am not sure to what extent this applies to real-world program likes operating systems. Do these types of programs need the full strength of Turing completeness?
It takes extremely little for a model of computation to be Turing complete. For example, various models with counters can simulate Turing machines. If you believe your software requires more than two counters that you can manipulate arbitrarily, you are using a Turing complete language. Though machine integers are apriori bounded, heap-allocated data structures usually are not. If your software needs lists, trees, and other dynamically allocated data, you are using a Turing complete language.
Are there simpler models of computation (such as PR) in which these applications could be written? If so, to what extent does this allow decidability of program correctness?
It is important to recognise that we do not want to check arbitrary properties of our software. Checking very specific, narrow properties (no buffer overflows, no null-pointer dereferences, no infinite loops, etc.) immensely improves the quality and usability of software. In theory, such problems are still undecidable. In practice, focusing on specific properties allows us to discover structure in our programs that we can often exploit to solve the problem.
In particular, you can modify your original question to
Is there an abstraction of my software that I can analyse efficiently in a non-Turing complete model?
An abstraction is a model that includes the behaviour of the original software and possibly many additional behaviours. There are models such as one-counter machines or pushdown systems that are not Turing complete and that we can analyse. The standard approach in program verification with automated tools is to construct an abstraction in such a model and check it algorithmically.
There are applications where people care about sophisticated properties of their hardware or software. Hardware companies want their chips to correctly implement arithmetic algorithms, automotive and avionic companies want certifiably correct software. If it's that important, you are better of using a (trained) human being.