In terms of formal models: Douglas Hofstadter' strange loop concept in "GEB" and "I am a Strange Loop", and Self-Representational theories of consciousness in general, provide a formal model for introspection based on self-reference.
Put simply an information processing system need have a set of input symbols for representing different objects, and a set of internal states, one of which is observing(object X) or processing(object X). All it needs to perform introspection is to have a representation of itself.
We can have a computer program that analyses computer programs. We simply have to feed the code of that program to itself and it is performing introspection. Turing proved that there is no general solution to the Halting problem by using this tactic.
A team in Switzerland has put this concept to practice, proposing what they call "Gödel Machines", although it is yet to be seen how much attention or success they will achieve.