Hey.

In the post Tests that test tests, I described my view on program verification through duplicating their logic as a separate model and then comparing with it. Unit tests were a special case.

This time, based on the ideas presented, I will try to formulate a general approach to assessing the level of software verification.

Introduction

When developing software, we, in fact, are engaged in the formalization of a certain subject area, the result of which is the appearance of a model describing it.
')
You can check the accuracy of the model implementation only by comparing it with the sample external to the model:

• original subject area - running the software for operation;
• another model developed for the same subject area.

Of course, when comparing models, it is not so much their verification, as “synchronization”, since when differences are found, it is impossible to say for sure in which of the two models there is an error.

Why duplicate logic works

Let be:

• when developing model 1, the probability to make a mistake is p1;
• when developing model 2, the probability of making the same error is p2;

Then:

• the probability of making this error simultaneously in two models is equal to p1 * p2 (for the sake of abbreviation of the text, we assume that these are independent events);
• this is usually significantly less than the initial probabilities.

^{This graph shows the change in the probability of the occurrence of the same error in the two models and is intended to add weight to the article.}

From these considerations it follows that it is desirable to choose models that are organized on different principles, so that the probabilities of assuming similar errors differ. Otherwise, the verification will skip a whole class of errors, the probabilities of which for this type of model are committed to 1.

In the case when the test model closes only part of the functionality of the original model, it is reasonable to consider it component-wise: so that the test model either closes the entire component or not.

Popular verification methods

Let's look at the most popular methods of improving the quality of software and demonstrate that each of them is based on the formation of a separate domain model and comparing it with the main one.

To do this, we define properties that may differ methods:

• method of implementation - how the duplicate model is implemented;
• verification method - how models are compared;

Tests (automatic, semi-automatic, manual)

method of implementation: a code (or an algorithm of human actions) that implements the creation of an environment and verifies the result of the target model;
verification method: calling the program code with tests or manual testing by the tester;

Static analysis

method of implementation: the model is defined by the rules inside the checking software, for example: compiler, pylint, PVS-Studio. In particular cases, there may be an additional specification, for example: description of types, extended specification of algorithms (example: habrahabr.ru/post/251751 );
verification method: call an external verifier to analyze the code of the target model;

Pair programming and code review

implementation method: the model is located in the partner’s head;
verification method: comparing your model with what you write;

Full system duplication

implementation method: a complete analogue of the target model developed by another team;
verification method: comparing the states of two models and the results of their functioning;

A couple of words about typing

In my opinion, it cannot be considered a separate verification method, but rather correctly attributed to:

• static analysis, if it is static;
• to test if it is dynamic.

Accordingly, typing has all the features of the corresponding methods.

How can these considerations be used?

We can strengthen our argument in organizing the testing process and obtain several plausible metrics of the project’s “verification”.

Metrics

The simplest metric that comes to mind is the level of coverage by duplicating the target system. In other words: how many verification models repeat each piece of functionality of the original system.

• minimum coverage - the minimum number of models per piece of the functionality of the original model;
• average coverage - the average number of models per piece of functionality; You can calculate, for example, by breaking the original system into components, calculating the coverage of each component and taking the average.

Organization of the testing process

Knowing the features of the project and the team, we can choose the types of quality control in a convenient way for us.

We can, for example, establish that we want to have a minimum coverage of 1 - i.e. at least one duplicate model per piece of functionality.

Based on this requirement, we direct all the resources of the testing department to a 100% UI check, and for the internal components we allocate the developer for writing unit tests.

An alternative would be to smear the efforts of the testing department throughout the project and get coverage in 0.5 models (expert assessment), but save the efforts of the developers by sending an extra person to do pair programming of a particularly critical component (the coverage of which will be 1.5).

Summary

In this article, of course, there are no claims for any discovery. But there is an attempt to add more formality and validity to the organization of software development.