Floating point example – an exotic investment

To illustrate the usefulness of floats inside our model checker, we will define a non-trivial investment game, formalize it in an extension of HLL (the input language of PSL), and check some properties of the investment using PSL. The rules of the investment are as follows:

1. The initial investment is 100.0 of our favorite currency (let’s call it “satcoins”).
2. A year of normal return, our investment grows with 5 %.
3. A good year, which happens at least once every 5 years, the investment grows with 20 % plus an extra bonus of 0 to 100 satcoins.
4. A bad year, which also happens at least once every 5 years, the investment is halved.
5. An excellent year, which happens at least once every 7 years, the invested amount is squared (multiplied by itself).
6. Finally, a disastrous year, which happens at least once every 8 years, cancels the result of an excellent year: the new amount is the quotient of the current amount and that of the previous year.
7. The first year is a normal year.
8. An excellent or disastrous year is always followed by a bad year.
9. The calculations shall be performed according to the international floating point standard IEEE 754 using 32-bit binary floats (known as the type “float” in the C programming language).

This informal specification of the investment rules can be straightforwardly translated into extended HLL. We will omit some of the details. However, the part relating to the actual floating point calculations could be formalized into the following code:

@ include FP_8_23
Namespaces:
FP_8_23 {
 Types:
  enum {normal, good, bad, excellent, disastrous} Year;
 Declarations:
  Year year;
  int [0, 100] bonus;
  float amount;
 Definitions:
  rne := Rounding::rne;     // Round to nearest tie to even
  I(amount) := 100.0;
  X(amount) := (year
               |normal     => mul(rne, amount, 1.05)
               |good       => add(rne, mul(rne, amount, 1.2),
                                       of_int(rne, bonus))
	       |bad        => div(rne, amount, 2.0)
	       |excellent  => mul(rne, amount, amount)
	       |disastrous => div(rne, amount, pre(amount)));
}

Checking properties of our investment

The kind of properties of floating point calculations that we are interested in checking using our model checker, is typically properties such as “the calculation does not overflow our 32-bit representation (no infinities)” and “divisions by zero does not happen (no NaN values appear)”. Indeed, PSL is able to prove the absence of overflow and NaN for the first 80 years of our investment over night. Note that properties such as “the expected average return on investment” is outside of the realm of model checking, and so will not be considered here. Instead, we will ask PSL if our investment can generate (if we’re lucky) at least a billion satcoins. We do this, as usual, by trying to prove that the amount on our account is always less than a billion. If the tool disproves (or falsifies) this property, then it will provide a counterexample to the proof as a solution:

Proof Obligations:
 lt(amount, 1.0e9);

In a matter of minutes, in single thread on an average laptop, PSL tells us that after at least 13 years, there exists a scenario in which we become satcoin billionaires. (In this time, PSL has also proved that there are no scenarios shorter than 13 years.) Below is one out of many scenarios found by PSL. The table should be read by combining the “year”, “bonus” and “amount” on the same line to determine the “amount” on the next line. As usual when dealing with automatic provers, the scenario may surprise at first, but is nevertheless valid and easily verified.

Summary

We have shown how a non-trivial floating point calculation, in the guise of an investment game, can be successfully checked by PSL 4.0. It should be noted, however, that automatic verification of floating point arithmetic is notoriously hard, and there are numerous pitfalls, so it is important to have realistic expectations. PSL uses underlying techniques known as bitblasting and SAT-solving, which are extremely precise (down to the last bit), but of course come with an attached cost. For example, if we double the precision from 32-bit to 64-bit floats in our investment game, runtimes approximately quadruple. Fortunately, PSL provides very efficient support for parallel computing, which means that such effects on runtime can be compensated by the use of more processor cores.

We conclude by observing that for complex safety-critical reactive systems with a little bit of floating point arithmetic, automatic reasoning tools such as PSL can be very useful, especially for finding unexpected scenarios such as the generation of NaN, infinities and other values out of the expected range.

Inlägget Floating point model checking dök först upp på Prover - Engineering a Safer World.

Declarations:
 int partialGrid[9][9];
Definitions:
 partialGrid := ;

Declarations:
 int [1,9] unknown[9][9];
 int [1,9] grid[9][9];
Definitions:
 grid[i][j] := if partialGrid[i][j] == 0 then unknown[i][j] 
                                         else partialGrid[i][j];

Definitions:
 objective := ALL digit:[1,9] (
    ALL row:[0,8] SOME col:[0,8] (grid[row][col] == digit)
  & ALL col:[0,8] SOME row:[0,8] (grid[row][col] == digit)
  & ALL subgridRow:[0,2], subgridCol:[0,2]
      SOME sRow:[0,2], sCol:[0,2]
    (grid[subgridRow * 3 + sRow]
         [subgridCol * 3 + sCol] == digit));

Proof Obligations:
 ~objective;

$1*: grid[0][0] is [1]
$2: grid[0][1] is [7]
$3: grid[0][2] is [6]
$4: grid[0][3] is [4]
$5: grid[0][4] is [5]
$6: grid[0][5] is [3]
$7: grid[0][6] is [8]
$8: grid[0][7] is [9]
$9: grid[0][8] is [2]
    ...
$80: grid[8][7] is [2]
$81: grid[8][8] is [9]

Declarations:
 int [0,8] counter;
 int [1,9] rows[9];
Definitions:
 grid[i][j] := if partialGrid[i][j] == 0 then unknown[i][j] 
                                         else partialGrid[i][j],
               grid[i][j]; // Keep value in next time step
 counter := 0, (counter + 1) % 9;
 rows[i] := grid[i][counter];

$1*: rows[0] is 1 7 6 4 5 3 8 9 [2]
$2: rows[1] is 9 4 2 7 8 1 3 6 [5]
$3: rows[2] is 5 8 3 6 2 9 7 4 [1]
$4: rows[3] is 3 9 1 5 4 6 2 8 [7]
$5: rows[4] is 6 2 7 9 1 8 5 3 [4]
$6: rows[5] is 4 5 8 2 3 7 9 1 [6]
$7: rows[6] is 2 1 4 8 9 5 6 7 [3]
$8: rows[7] is 7 3 9 1 6 2 4 5 [8]
$9: rows[8] is 8 6 5 3 7 4 1 2 [9]

How safe and efficient are your rail control systems? Let’s find out!

Inlägget Using HLL to solve Sudoku puzzles dök först upp på Prover - Engineering a Safer World.

The history of HLL

The language has its roots in the proof engine technologies developed by Prover in the 1980s (Stålmarck’s method), 1990s (temporal induction) and early 2000s (higher level theories) and its development was prompted by a need for trusted (or certifiable) formal verification.

HLL is a declarative language with a broad panel of types and operators and is suitable for modelling discrete-time sequential behaviors and expressing properties of these behaviors.

Or to put it differently: if you have a reactive system (such as an interlocking or a CBTC subsystem) with some inputs, outputs and internal state (memory), and you want to formally prove that some present or future conditions on the outputs shall follow from some past or present conditions on the inputs, then HLL may be the right language for you. The language, with its associated tools, can be used for applications such as invariant checking, sequential equivalence checking, test case generation or static code analysis (detection of runtime errors such as overflows or divisions by zero).

Version 1.0 of HLL was released in 2008 and the language is being continually developed. The latest version includes, in addition to the basic core of Boolean logic and integer arithmetic, features such as enums, arrays, tuples, structs, recursive functions, quantifiers, polymorphism, namespaces and blocks. The imperative dialect of HLL also supports statements such as assignments, if-then-else, loops and procedures.

The HLL formal language success

The success of HLL can possibly be attributed to its ease of use (flexible and intuitive) coupled with the support by formal verification tools that both scale up in practice for a wide variety of systems, and provide certifiable results based on diversification and proof logging/checking.

Find out more about HLL here.
You can also check out our HLL Forum – The community for those who use HLL

Inlägget HLL formal language celebrates 10 years dök först upp på Prover - Engineering a Safer World.