Broadly speaking, in order to have a "simulation", we must first have a physical computer of some kind... How can we rigorously (mathematically) describe the relationship between the physical computer and the formal system being simulated?
If you are talking about a formal simulation on a computer, then you are talking about a computer simulation. An excellent example of how computers practically apply simulations is by emulating other software and hardware machines and are known as virtual machines. Formalizations of computer hardware and software are a topic of discussion in subjects like formal languages and their correspondence to automata, formal systems, and computability theory. There are more formalisms than a full-time academic can wrap her mind around.
Computation and the Digital Computer
There are several definitions of computation.
See Philosophy of information question on the nature of computation
However, if you are invoking the modern concept of digital computers such as those built to the von Neumann architecture and Harvard architecture and those that align with Turing-equivalent models of computation, then you are dealing not with computer models, but computer simulations. From WP:
Computer simulation is the process of mathematical modelling, performed on a computer, which is designed to predict the behaviour of or the outcome of a real-world or physical system. Since they allow to check the reliability of chosen mathematical models, computer simulations have become a useful tool for the mathematical modeling of many natural systems in physics (computational physics), astrophysics, climatology, chemistry, biology and manufacturing, as well as human systems in economics, psychology, social science, health care and engineering. Simulation of a system is represented as the running of the system's model. It can be used to explore and gain new insights into new technology and to estimate the performance of systems too complex for analytical solutions.1
That is, a simulation is software which is generally seen as a combination of data or state and instructions or process that allows a computing platform to predict physical systems which philosophically implies the belief in physicalism. That is to say, the sciences which often use proof-theoretic interpretations of physical laws, can be done by using encoding established scientific theories to attempt to conduct experiments about natural phenomena which might not be amenable to laboratory practice. This is of great utility in many disciplines, particularly when examining permutations of deterministic systems, such as distributed computations of protein folding such as Stanford's Folding@home project.
The Core of the CPU
As to the formal nature of these systems, what needs to be understood is what is at the core of the CPU, which from the perspective of software instructions, is the ALU. Ultimately, from a software engineer's perspective (as opposed to a computer engineer who has access to microcode), every platform consists of a series of layers of data and instructions that ultimately start with op codes:
In computing, an opcode1 ... is the portion of a machine language instruction that specifies the operation to be performed. Beside [sic] the opcode itself, most instructions also specify the data they will process, in the form of operands. In addition to opcodes used in the instruction set architectures of various CPUs, which are hardware devices, they can also be used in abstract computing machines as part of their byte code specifications.
Opcodes or machine instructions are the processing primitives of the system which largely consist of arithmetic and logical operations performed on data in registers inside the CPU. Because opcodes are mind-bogglingly small operations in an obtuse binary format, generally no programmer works with anything less than assembly language. But often, coders write in tools as sophisticated as fourth-generation langauges such as Java or C#.
Computers and Formalisms
Since the von Neumann architecture is an example of a general purpose computer, there is no one formalism. In fact, for simulations and computers, there are a dizzy array of formalisms. Formalisms for hardware design. Formalisms for OS design. Formalisms for programming languages and compilers. Formalisms for software design. Formalisms for logical and arithmetic systems. Formalisms for describing physical data.
To give a few examples, a computer language might be described abstractly by BNF, which is an artificial language specification. For instance:
<syntax> ::= <rule> | <rule> <syntax>
<rule> ::= <opt-whitespace> "<" <rule-name> ">" <opt-whitespace> "::=" <opt-whitespace> <expression> <line-end>
<opt-whitespace> ::= " " <opt-whitespace> | ""
Then a compiler is built that converts instructions in a programming language into opcodes.
But, perhaps the program itself is designed in UML and written in Java according to object-oriented design principles. And on top of those formalisms, it implements numerical analysis, SQL storage, and a physics engine. Each and every one of those will involve formalisms, including the last which implements the formalisms of physical laws. That's a lot of formalisms.
Philosophy of Computation
There are very important philosophical implications regarding simulations and computation, and perhaps one of the most important is the Curry-Howard correspondence which shows equivalencies between mathematical and computational formalisms:
In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relationship between computer programs and mathematical proofs.
See Logic and Computation: a philosophical viewpoint on Curry-Howard isomorphism
Another important aspect of simulation are questions it raises about the relationship between physical and mental ontologies, such as Cartesian duality. One of the most famous philosophical problems in the philosophy of mind is the Chinese Room argument by Searle. See How does human intelligence differ from Searle's chinese room?
Lastly, computers are now being used not just to simulate physical systems such as molecules and weather systems, but aspects of epistemology and intentionality itself. In fact, a number of philosophers are collaborating with other cognitive scientists to build computers to simulate aspects of consciousness. See Computers, Artificial Intelligence, and Epistemology