·Table of Contents
·Reliability and Validation 1
Preparing Testing by Proving Critical SystemsD. Rouillard, R. Castanet, P.Castéran, P. Félix
Labri, UMR 5800, Université Bordeaux 1,
33405 Talence Cedex, France
* This development is a part of the project Calife of the RNRT.
Let us consider some proof assistants based on higher order logic, such as Coq, HOL, or various "logics object"of Isabelle([9, 10]). Their main feature is a great expressive power, which includes a wide range of mathematics. As a result, there is no problem to use them in order to define formally various classes of transitions systems (including Büchi Automata, Petri nets, Turing machines, ... ), their semantics, and specification of their behavior (including various kinds
of temporal logic,m-calculus, ...). It is therefore possible to compute within the same framework, two implementations of the same specification e.g. one with Büchi Automata, the other by Petrinets.
Moreover, such systems are often provided with rewriting facilities, making possible to mix proof and computations. For instance, we can simulate a transition system by computing some of its executions or even looking for some executions having a given property.
Reading the explanation above, one can believe that proof assistant are enough to do all the verification/test activities. This would not take into account the need for efficiency and automation.
When the property we want to prove deals with a finite system (given by enumeration), it is often better to call an automatic process which may be a function in the meta-language of the assistant or an external tool like MEC. In the last case, we must have enough confidence in the correctness of tool to accept its "oracles" as axioms for our proof assistant.
The main advantages of the approach we describe are following :
In the last case, a constructive proof compute the execution x ; it's shows that simulation/test is highly compatible with proof activity.
We present in the next session the tools CClair, a prototype which implements the most of the features of this approach.
Isabelle is a generic proof assistant that supports a collection of logics among them First Order Logic, Zermelo-Fränkel set theory. For our work, we only use the High Order Logic (HOL in short) distributed within Isabelle too. The core of the system consists of a small and clear set of rules from which all proofs are derived. The consequent confidence in the soundness of the tool makes Isabelle a reliable proof checker.
The interpreter ML in which Isabelle is written allows facilities to write functions in order to resolve some kinds of statement like classical reasoning and linear arithmetic inequalities. In addition, Isabelle provides a powerful rewriting mechanism and several tools to automate proof.
3.2 Architecture of CClair
The main goal of the project CClair is to provide a framework for reasoning about automata, especially labeled transitions systems. It is comprised of several Isabelle theories each composed of a collection of definitions and proved lemmas. As a whole, they constructed the hierarchical structure depicted in Fig 1.
|Fig 1: Actual/Planned CClair Theory structure|
We claim that our architecture may be easily extended with another models, simply by providing definitions of the automata and expressing its operational semantic part in term of transition systems. Thus, we plan to add into CClair the Büchi automata model as well as Petri nets. The great benefits of this generic architecture is the possibility to compare object, mainly executions and traces, which are issued from various formalisms. It's because the behavior of all the build-in models are internally translated in terms of transition systems.
|Fig 2: a simple transition system:the Digicode|
4.1 Tactics and rewriting
Verification activity in a proof assistant consists of successive raffinements of the statement to prove by applying tactics. A tactic is a function that splits the current goal into several new subgoals according to a logical deduction rule. The proof is complete when there are no longer any subgoals to prove. One of the central Isabelle built-in tactic, used below, is resolve_tac which encapsulates resolution of the goal with a given list of inference rules.
All the interactions with the system are done via tactics but we must precise here that it is not necessary to give during the proof, all the basic step of deduction. Some large part of a proof is automatically achieved by rewriting. For example, the following rule :
is able to solve without any outer help,the following statement which means that a given trace contains the action keyC(in the figure 2,describing a digicodeusing only three keys :A,B,C):
However, tactics make it possible for the user to call external decision procedures. We have experimented this last feature in the context of finite transitions systems.
4.2 Finite verification
The theory SmallTS provides a collection of automatic tools in case we have to deal with a system given by enumeration. Indeed, it is here easy to compute, for example, the set of states reachable from a distinct state or to search an execution between two given states.
Actually theses computations are done by functions written in SML, the meta-language of Isabelle, but we plan in the next version of CClair to use more powerfull tools such as model- checker to achieve this task.
As an illustration of the convenience of this approach, we prove that we can found an infinite execution from the state q1 in the digicode :
The statement is introduced by the Isabelle function Goal :
First, we remove the existencial quantifier by applying its introduction rules exI.
by (resolve_tac [exI] 1);
Level 1 (1 subgoal)
We now apply on subgoal 1,the lemma omega_is_Exec from our library of proven lemma,which means that in order to obtain an infinite execution,it is enough to find a cycle and repeate it using the "w" operator.
by (resolve_tac [omega_is_Exec] 1);
Level 2 (1 subgoal)
A adequate cycle is then computed by an automatic procedure via the tactic F_Exec_tac.
by (F_Exec_tac 1);
This short example shows what a usual session looks like :
a sequence of alternating steps of reasoning and computation.
The connection of this methodology with the test generation is presented in the next section.
4.3 Unknown variables
Isabelle provides prolog-like variables, called unknowns. These variables may be introduced in any statement and will be instantiated by unification during the proof. We have thus the possibility to build statement like :
In the same way,the unknowns allow us to build objects like traces and executions using the technique of prolog-like answer extraction and then to synthesize some test cases.
4.4 Test purpose and test cases
A test is a sequence of actions which is carried out the industrial product to verify whether it reacts in conformity with a design specification. A particularly active research area in computer science [3, 6, 4, 7, 11, 5] consists of the development of automatic tools which generate tests from the executions of the formal model of the real-life system. What we call a test may be simply an execution crossing a given transition, an execution where all actions of the system appear or an execution which contains a subsequence of actions which occurs at some fixed time.
Notice that in all cases, the goal is to build an execution which satisfies a property, what is naturally translated in CClair specification language by the following statement :
Where P is the specification of the expected property and ?w an unknown variable which represents a behaviour of the system S.
The development activity is now a mix of techniques like :
For example, let us build an execution in the digicode automaton with the following test purpose : the system must perform the action keyC. We start with the following statement :
Applying the introduction rule of splits our statement into two new subgoals.
by (resolve_tac [conjI] 1);
Level 1 (2 subgoal)
As made above,we are looking for an execution in Digicode between states q1 and q4,using the tactic F_XTraces which calls an automatic procedure. Then the second subgoal is simplified.
If the execution returned by F_XTraces does not permit to conclude, the system backtracks and computes another execution.
by (SOLVE (F_XTraces_tac 1) THEN (Simpl_tac 1);
If we now look at the proven lemma, we can see that the variable ?x has been instanciated with an execution the trace of which (keyC,keyA,keyB,keyA) satisfies the desired test purpose. Therefore, this execution provides a case test. Notice that backtracking allows us to obtain possibly several other test cases.
In this example, we have dealt with a small enumerated system for which a dedicated tool is provided to compute execution but it is not always the case in more complicated models such as p-automata. If so, the simplest way to generate an execution is to simulate the model. To achieve this task, the user have to specify, with the help of adequate tactics, the list of actions the system must perform. Each step is done under control of CClair. Indeed, simulation tactics involve rewriting mechanisms which simplify constraints on transition like guards, and invariants in order to detect tautologies and redundancy hypothesis. In these cases, the unsolved assumptions are delivered to the user's judgment. This allows the user to build a so-called symbolic execution i.e. an execution of the underlying control graph together with a set of constraints (mostly on abstract data) from which a solver can generate several test cases with a given degree of exhaustiveness.
|© AIPnD , created by NDT.net|||Home| |Top||