In formal verification, what is the formal specification, what formally means there?

Question

I have been reading a lot about formal verification of software and apparantly you need to formalize the behaviour of the program to create an equivalent model of it (if I get it right). But nowhere can I find what "formalizing" actually means. Describing mathematically? That is a bit vague. Describing in a way that its semantics can be interpret mathematically?

I am not a math guy and trust me, I have tried reading anything I could google. But all say the same - "produce formal model".. I would be extremely grateful for an explanation taking into account my very limited background in math.

Answer 1

See Formal system.

We can agree that the aim of formalization is to "describe mathematically" a theory or problem in order to aply mathematical techniques to "handle" it.

For example, in computer science, formal specifications:

are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools. These specifications are formal in the sense that [the syntax and semantics of the system are mathematically (i.e. exactly) described].

---

Consider for example Propositional calculus: it is a formal system with a syntax specified by formal rules and with a very simple (truth-functional) semantics.

We use it as a "toy system" useful to study the basic properties of inference; thus, we can say that is a (very very simplified) formal model of human reasoning.

Answer 2

Formal description means that the system is described in a language derived from mathematic logic, the syntax and semantics (and vocabulary) are formally defined and allow you to apply mathematic operation on the result of your description.

Answer 3

Basically, the word "formal" in most mathematical contexts means that everything relevant is governed by syntax rules, which are rules about what strings of symbols (from some fixed alphabet) you can derive given initial or previously derived strings. Informal mathematics on the other hand proceeds by appealing to the intuition, such as whenever we write or say "Clearly, ...".

Formal systems

A formal system is intended to give a foundation for all the mathematics that can be translated into its language and derived according to its rules, because whoever accepts the meaningfulness of the formal system, meaning just the meaningfulness of the initial strings and the rules, must also accept the meaningfulness of all the derivable strings, which are called theorems.

The most common formal systems for mathematics are based on first-order logic, which can be expressed via many deductive systems. All these deductive systems have only a handful of rules each, and essentially everyone would accept that these rules are sound, meaning that they only allow us to derive true statements if we start with only true statements (each statement is nothing more than a string). So the only concern we would have is what initial statements we include in the formal system, which are called axioms. These formal systems based on first-order logic are called first-order theories.

One first-order theory is Peano Arithmetic, which captures as much as possible of what we believe about natural numbers in first-order logic. Another first-order theory is Zermelo-Fraenkel set theory plus Choice, which almost all modern mathematics can be translated into. This last point is an important one, because it means that whoever accepts that the axioms of ZFC are somehow meaningful, they also must accept all the theorems of ZFC as meaningful.

Note that the formal system is separate from how people interpret the meaning of the theorems and how they evaluate meaningfulness. In other words, people may accept the same formal system but hold different interpretations of what the theorems mean to them. This point must be clearly understood, since it is impossible to capture all meaning in symbols; after all every symbol of any kind is merely a symbol, namely a physical entity that refers to or reflects something else, be it an object or a notion.

The purpose of a formal system therefore is to isolate the notions of meaning in mathematics to the 'smallest possible core'. If any two people can somehow agree on how to interpret statements in first-order logic, and agree that the axioms of a first-order theory are true under that interpretation, then they would certainly agree on all theorems derived in that theory. This is the main goal of formalization of mathematics, and in some sense it is successful because nearly everyone intuitively understands and interprets first-order sentences in the same way.

Other kinds of "formal"

As an aside, we also see "formal" in other areas of mathematics, with the same kind of connotations as I hinted at in my first paragraph. For example, a formal power series is simply the power series viewed as an infinite sequence of coefficients instead of as a function of some sort. Whenever we talk about ordinary power series we have to specify and prove its domain as convergence is not guaranteed for arbitrary sequences of coefficients. But a formal power series can be defined and manipulated (syntactically) without concern for convergence simply because we never attempt to evaluate it by substituting a (formal) variable with some value. This feature can be very useful such as for generating functions in combinatorics.

Similarly formal differentiation concerns syntactically differentiating an expression (which is a string) with respect to some variable (which is a symbol) by following syntactic rules. When the original expression corresponds to an actual function, formal differentiation gives an expression corresponding to its derivative. This is exactly how computer algebra systems compute the derivative of a function from the string representation that you provide. On the other hand, formal differentiation is very useful for some instances when ordinary differentiation is meaningless, such as differentiating generating functions or differentiating polynomials over a field of prime characteristic. In the latter case, for example, we can prove that a polynomial has a repeated roots in a splitting field if and only if it and its formal derivative have a non-constant factor.

Answer 4

While the other questions are not wrong, none of them address what a model is in the specific context of formal verification, so let me address that. Verification and model checking is a technique for constructing a model of some process which has a specific behaviour, for example a software program, a factory workflow, or a communication network, and then verifying that some kind of property holds for this model, for example that the model never stops, or never enters a bad state.

In order to make a model that can be verified in this way, we need a formal, mathematical way of describing these models. The formalism that is usually used is some variety of automaton. There are many many different automaton formalisms, such as labeled transition systems, timed automata, markov chains, Büchi automata, Petri nets, etc. depending on what aspects of the process you are interested in modeling (for example whether time is important). Here is a simple example of a labeled transition system, taken from Joost-Pieter Katoen's slides: This automaton describes the behaviour of a simple (and odd) vending machine. It starts in the state $pay$ where the only action that can be taken is to insert a coin. Then it goes to the state $select$, where the vending machine nondeterministically and internally chooses whether to give a beer or a sprite. Then the customer can get the sprite or beer and the machine is back in the $pay$ state.

Now we can ask whether some of these states satisfy a given property or not. Such properties are expressed in a formal logic, of which there also exist many different kinds, such as Hennessy-Milner logic, $\mu$-calculus, second-order monadic logic, and many other modal and temporal logics. For this example, let us use Hennessy-Milner logic. The formula $\langle insert\_coin \rangle \langle \tau \rangle \langle get\_beer \rangle tt$ says that it is true that we can insert a coin, and then there exists some internal choice such that we can then get a beer. On the other hand, the formula $\langle insert\_coin \rangle [\tau]\langle get\_beer \rangle tt$ says that we can insert a coin, and then no matter what internal choice the vending machine makes, we can then get a beer. Clearly, the first one is true for the state $pay$ and the second one false for the state $pay$.