·Home ·Table of Contents ·Reliability and Validation 1

Preparing Testing by Proving Critical Systems D. Rouillard, R. Castanet, P.Castéran, P. Félix Labri, UMR 5800, Université Bordeaux 1, 33405 Talence Cedex, France Contact

Abstract

This paper presents a framework to specify and validate critical systems. It is based upon the proof assistant Isabelle and provides a formalization of transitions systems model on top of which various other models may be developped. Verification alternates interactive steps of reasoning and computations with the possibility to build test cases using a prolog-like approach.

* This development is a part of the project Calife of the RNRT.

1 Introduction

The three main categories of verification techniques are testing, model-checking and theorem- proving. Testing cannot provide the necessary confidence to validate safety-critical reactive systems. This is due to the fact that it cannot perform an exhaustive verification of the final product. Nevertheless, testing is essential at the end of the development life cycle to detect errors of implementation in real-life system but it must be preceded by an intensive study of a formal representation of the system.
Model-checking computes automatically wether a system satisfies a property expressed under the form of a logical formula, or not. This consists of the exhaustive exploration of the reachable state space in order to find a state where some properties hold. But in some cases, and especially in the context of real-time systems, the state-space is too large to be entirely explored.
Moreover, some interesting systems have an infinite numbers of states or are defined in a symbolic way. In these cases, proof assistant may help to verify a system, building a proof by composition of logical deductions. The main drawback of this method is to require a high degree of ingenuity and interaction.
It is now well admitted these three approaches are complementary and therefore the ideal verification tool should combine them. We argue that proof assistants are suitable to be the base of such a tool because they generally provide a meta-language (mostly some version of ML) which permits to manipulate the results once proven.
The remainder of the paper is structured as follow : Section 2 presents the practical benefits of using a proof assistant. Our tool CClair[2], supporting some of the expected concepts, is described in Sect. 3. Proof activity and test generation as an consequence of our verification approach is presented in Sect. 4. Finally, section 5 concludes the paper.

2 A proof assistant as entry point

Let us consider some proof assistants based on higher order logic, such as Coq[8], HOL[13], 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 :

• A unique formalism for describing a transitions system or its specification : a transition system is defined in term of its set of transitions, which may be either finite (and a possible entry point for automatic tools) or infinite and described in a comprehensive way.
• The same format for all kinds of results one wants to get, which is the mathematical language, able to express such statement as :
  • all states of S are reachable"
    
  • state q is a deadlock"
    
  • there exists an infinite execution x starting from q₀ and satisfying the property P"

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.

3 The CClair environment

3.1 Isabelle
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 concentrate our effort on the theory TS which implements the transition systems model. Owing to its simplicity, this model is the underlying representation of many tools. Furthermore, the operational semantic of more elaborate models could easily be expressed in term of transition systems.
A transition system with action type a and state type s is defined by the type constructor (a,s) ts which is synonymous to the type of set of transitions.
This polymorphic declaration allows us to formalize not only small systems with a finite enumerated set of transitions, but also infinite systems or a family of systems indexed by some parameters.
The behaviour (i.e. executions and traces) of a transition system is formalized with the help of the theory of lazy list by Paulson[10]. The main advantage of this theory is to accommodate both finite and infinite list in a single representation. Furthermore usual functions on list, including filtering are provided. In CClair, executions are therefore declared as possibly infinite lists of transitions and several predicats about it have been introduced, using the mechanism of inductive or coinductive definitions. We present here some them :
Since temporal logics have proven to be suitable to express a great variety of properties, we provide a collection of usual temporal operators such as "Always"(), "Eventually" (à), "next"(O), "infinitely often" (à), ... With the help of these operators, we can express the most of formal statements about desired system properties and verify them.
On the top of TS, it is possible to formalize some more complex models of automata : actually, the distribution of CClair contains two examples of such models (the theory SmallTS only distincts some kind of transition systems) :
• an extended transition system model named GU (for Guards and Updates) where transitions are guarded by constraints on variables.
  
• the timed model of p-automata[1] which differs from classic timed automata in that they consider a single universal clock but possibly several variables.

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 The verification activity

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 digicode[12]using 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 q₁ 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);
No subgoals!

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 :

(1)

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 :

• application of tactics (basic or complex).
  
• computation by rewriting tactics or call to external tools.
  
• Prolog-like backtracking to control the various instantiation made during the previous activity.

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 q₁ and q₄,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);
No subgoals!

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.

5 Conclusion

The main thesis of this paper is that current proof assistants like Isabelle, Coq, HOL can be used as an entry point for the veri"cation of critical systems. To substantiate this claim, we have developed the tool CClair. Its overall architecture is based upon a natural formalization of the transitions systems model from which more complex models may be implemented. Moreover, we have demonstrated that it is possible to accommodate complex scheme of proof, computations by rewriting or call to external process, and tests generation in the same tools.
CClair has been used to formally specify and prove correctness for the Available Bit Rate (ABR) conformance protocol used in ATM networks and our experiments with transitions systems show that is possible to generate test cases for this protocol, using our proof-basis approach. Another planned goal is to connect CClair with external decision procedures in order to provide a possible guide for developping future tools in the context of the RNRT project Calife.

References

1. Berard Béatrice and Laurent Fribourg. Automated verification of a parametric real-time program: The ABR conformance protocol.Lecture Notes in Computer Science, 1633:96-107, 1999.
2. Pierre Cast ran and Davy Rouillard. Introduction to CClair (draft). Rapport technique, LaBRI, December 1999. www.dept-info.labri.u-bordeaux.fr/~casteran/CClair/Tutorial.ps.
3. A. Cavalli and All. Engendrer des tests pour un vrai protocole, grâce à des techniques éprouvées de vérification. CFIP'96, 1996.
4. M. Clatin, R. Groz, M. Phalippou, and R. Thummel. Two approaches linking a test generation tool with verification techniques. Protocol Test systems, VIII, 1995.
5. M. Dubuc, G. Bochmann, and R. Dssouli. TESTL : An environment for incremental test suite design based on fsm. 4 th IWPTS,Leidschendam, 1991.
6. J.C. Fernandez, C. Jard, T. Jéron, and G. Viho. Using on-the-fly verification techniques for the generation of test suites. CAV'96, July 1996.
7. J. Grabowski. Test case generation and test case specification with MSC. PhD thesis, University of Bern, 1994.
8. Christine Paulin-Mohring. The coq project, 1999. http://coq.inria.fr.
9. Lawrence C. Paulson. The Isabelle reference manual. Technical Report 283, University of Cambridge, Computer Laboratory, 1993.
10. Lawrence C. Paulson. Isabelle's object-logics. Technical Report 286, University of Cambridge, Computer Laboratory, 1993.
11. R.Castanet, C.Chevrier, O.Koné , and B. Le Saec. An adaptative test sequence generation method for the users needs.Protocol Test Systems VIII, 1995.
12. Philippe Schnoebelen et al. Vérification de logiciels, Techniques et outils du model-checking. Vuibert (France), 1999.
13. Daryl Stewart. The hol system, 1998.http://www.cl.cam.ac.uk/Research/HVG/HOL.

© AIPnD , created by NDT.net

|Home|    |Top|