** Thomas Arts **

Computer Science Laboratory, Ericsson Telecom AB,

thomas@cslab.ericsson.se

** Dilian Gurov, Mads Dam, Lars-åke Fredlund **

Swedish Institute of Computer Science,

{dilian, mfd, fred}@sics.se

First of all, we may obtain trust in a program's correctness by examining the way the program is written, and by the experience of its programmer/designer. However, the more complex the programs get, the easier it is to overlook a flaw in the program. Therefore, secondly, a program is tested as exaustively as possible. Testing a program means that you take a certain configuration of the program and its environment and that for this configuration you run the program and see what happens. The more configurations you try, the more you believe that you have covered the program behaviour in general. Since most programs have infinitely many configurations to start with, testing implies that you might have overlooked that configuration that is causing your program to fail.

If we are able to formulate the property that we want the program to meet in a very precise, mathematical way, then we can use verification
techniques to actually *prove* that the property holds for *all*
possible configurations.

Before one can prove anything about a program, one has first to make clear what to prove, which then should be formalised. This specification process involving "deep thinking" turns out to be probably half as effective as the actual verification. By explaining yourself, or better, a colleague what you did and why it should work correctly, many serious mistakes and pitfalls show up.

After that it has become clear which property of the program should be verified, one can consider using our verification technique. For using this technique we have designed:

- a formal language, based on a temporal logic called the modal mu-calculus, in which to state the properties,
- a proof system, consisting of a set of proof rules, for reasoning about program correctness, and
- a tool that assists and partially automates the latter reasoning.

In the formal language, we directly address the Erlang primitives and the Erlang processes. Additional logical connectives and quantifiers enable us to express properties like:

- Given a list
`X`, the evaluation of the term`length(X)`terminates and results in an integer. - The process P1 can only send messages to process P2 and P3.
- Given processes P1 ... P5 in a ring, if process P1 continuously sends 0 to process P2, then eventually P5 sends 0 to P1.

The difficulty is of course to reduce the goal into subgoals, such that in the end we end up with something trivial. We developed a set of approximately 50 proof rules that, depending on the form of the goal, can be used to devide a goal into subgoals. Often several of these proof rules are applicable to a certain goal and the hard part is to choose the right one.

The tool we have built enables to apply the proof rules to a
certain goal,
where the user has to choose the proof rule that should be applied.
In order to partly automate this, and in order to obtain a higher level
of abstract reasoning,
several heuristics have been developed that help
the user in the hard task of choosing the right rules.
For keeping an overview of what is proved and which subgoals are still open, the proof can be visualized by the daVinci graph manipulation tool, developed at the university of Bremen.

The billing agent asks the user for a

The user is clearly taking a risk by exposing the account number and so is the resource owner by giving away the resource before any money has been payed. The software written for performing these tasks should be trusted. Both the user as the resource owner, and probably even the bank want to be sure that the software meets certain security criteria. Typical properties that have been verified for this example are: (a) the number of transfers from the user account does not exceed the number of requests to use the resource; and (b) the billing agent does not communicate the user-account key to any other party than the bank.

Typical properties to verify here are those concerning the termination of the search, and the guarantee that all data that should be found eventually arrives.