I'm interested in software verification and therefore only interested in algorithms which always terminate in predictable amount of time and can determine whether the final result is expected or not, hence I think the computable functions are a good place to start as as I understand it these are functions which can be defined using a decidable procedure, i.e. an algorithm which always terminates.
I'm a little familiar with the Chomsky hierarchy, I imagine I would be looking for a language or an abstract machine that is as far up the hierarchy as possible, but does not suffer from the halting problem. However I don't think Linear-bounded Turing machine's are what's needed as these seem to just cut of resources i.e. they are just computers which stop simply because they run out of resources. I think I need something which limits the number of computation steps using logical expressions which can be reasoned with effectively, so by the time the computation finishes we are able to describe something about the final state. I need to be able to reason about cycles too. Could this be pushdown automaton? Are there any other suitable models I've missed?