Stefan Huster

Jonas Ströbele

Jürgen Ruf

Thomas Kropf

Wolfgang Rosenstiel

Using Robustness Testing to Handle Incomplete Verification Results when Combining Verification and Testing Techniques

Keywords: Software verification, Robustness Testing, Test Vector Generation 1

Modular verification and dynamic testing techniques are often combined to validate complex software systems. Formal verification is used to cover all input spaces and program paths. However, due to the high complexity of modern software systems, they might not achieve complete verification results. Dynamic testing techniques can easily be applied to any type of software. Current approaches use them to handle incomplete verification results by validating unverified sections. This way of combining verification and testing ignores the fact that tests can only be used to show the presence of errors, but not their absence. Undiscovered errors pose the risk to trigger further errors in vulnerable code sections. Vulnerable sections are modularly verified, but depend on the guarantees of the tested code. We include robustness testing to analyse the influence of undiscovered errors. The generated robustness tests simulate failed guarantees within the tested code. The triggered response to those simulated errors helps the developer in adding additional error handling code. This makes the system more robust against undiscovered errors and guards it against uncontrolled crashes and unexpected behaviour in case of software failures. In the second part of this paper, we introduce a reference-architecture to generate and apply robustness tests. This architecture has been applied to multiple case studies and helped to identify potential errors yet undiscovered by generated test cases.

Introduction

Modular verification and dynamic testing techniques are often combined to validate complex software systems. Verification techniques are used to guarantee that an implementation matches its formal specification. For object oriented programs (OOPs), the specification is often defined as a set of conditions such as pre-and post-conditions and invariants. Modular verification techniques [START_REF] Müller | Modular specification and verification of object-oriented programs[END_REF] analyse this type of specification based on a generated set of proof obligations (also known as verification goals). A proof obligation (POG) is similar to a Hoare-Triple P S Q [START_REF] Hoare | An axiomatic basis for computer programming[END_REF]. The POG contains a program segment (Hoare: S), a set of assumptions (Hoare: P ), and a guarantee (Hoare: Q) [START_REF] Beckert | Verification of object-oriented software: The KeY approach[END_REF]. While considering all assumptions, the verification framework has to verify whether each possible execution of the embedded program section fulfils the defined guarantee. Assumptions made by one proof obligation must be ensured by another one. Only the validity of all proof obligations implies the correctness of the entire software system. Especially OOP concepts such as inheritance and (recursive) aggregation cause an infinite number of feasible control flows and thereby a high level of complexity. Due to this complexity, formal verification techniques are rarely capable of achieving complete verification results. We use Listing 1.1 as running example to introduce our methodology. The listed method cannot be verified using the verification framework Microsoft Code Contracts 1 . It is part of a program to solve the Cutting Stock problem [START_REF] Amor | Cutting stock problems[END_REF]. This problem is about cutting standard-sized pieces of material into pieces of specified sizes. The listed method is used to add new cutting lengths (Cut) to the current cutting layout (Bar). It checks whether the available material length is long enough to add the given piece length. It analyses the summarised lengths of all added cuts plus the required minimum space between two cuts (line 14). The value of usedLength must always be smaller than the total material length. This is required by the invariant in line 7. Figure 1 shows how Code Contracts claims that this invariant is not guaranteed on exit. This illustrates how specifications remain unverified. In such cases, where some proof obligations remain unverified, current approaches ensure the correctness of those proof obligations by exhaustive testing. This use of testing can be shown to have residual risks. As Dijkstra put it, program testing can only be used to show the presence of bugs, but not their absence. Program sections which require the correctness of tested guarantees remain vulnerable, Let's come back to our running example. The unverified method in Listing 1.1 can be tested using the unit test listed in 1.2, achieving full branch, path and condition coverage. In view of testing, this test case covers all major coverage rates and the method can be seen as validated. However, we achieve the same testing results when replacing line 14 by if ((Length -usedSpace)< cutLength). This would be a major bug, because this line ignores the used material length. This bug allows to add more cuts to the bar than available material space. This could be tested when executing line 4 of our test case multiple times in a row. This simple example illustrates how testing can achieve good coverage rates while missing important defects. This paper introduces a new approach that uses robustness testing to analyse the influence of such undiscovered errors. We initialise invalid program states to simulate failed guarantees and inspect the corresponding behaviour of vulnerable program sections. Our goal is to support the developer in adding additional error handling code on critical locations in order to secure vulnerable sections against potential failures. The remainder of this paper is structured as follows: Section 2 describes related work and current tools. Section 3 describes how we use robustness testing to analyse the influence of undiscovered errors. Section 4 defines one reference implementation to generate the defined type of robustness tests. Section 5 presents our results in comparison to current tools. Section 6 concludes the paper and presents future work.

Related Work

Several methodologies and tools already exist which combine formal verification and dynamic testing. Christakis et al. [START_REF] Christakis | Collaborative verification and testing with explicit assumptions[END_REF][START_REF] Christakis | Guiding dynamic symbolic execution toward unverified program executions[END_REF][START_REF] Christakis | Narrowing the gap between verification and systematic testing[END_REF] present a methodology that combines verification and semantic testing. Different static verification models are used together to verify the software under test in a sound way. Assumptions made by one prover, e.g. regarding numerical overflows, are ensured by another. Unverified assumptions are subsequently tested. The symbolic testing is guided to cover specifically those properties that could not been verified. Czech et al. [START_REF] Czech | Just test what you cannot verify![END_REF] present a method to create residual programs based on failed proof obligations. They reduce the number of required test cases, by testing only those control flows that have not been verified. Kanig et al. [START_REF] Kanig | Explicit assumptions-a prenup for marrying static and dynamic program verification[END_REF] present an approach that uses explicit assumptions to verify ADA programs. Unverified assumptions are tested by generated test suites. Code Contracts [START_REF] Fähndrich | In: Static Verification for Code Contracts[END_REF], Pex [START_REF] Xie | Advances in unit testing: theory and practice[END_REF] and Moles [START_REF] De Halleux | In: Moles: Tool-Assisted Environment Isolation with Closures[END_REF] is the current Microsoft tool chain for software verification and symbolic test case execution. Code Contracts can be used to verify C# programs and supports contracts such as pre-and postconditions. Pex and Moles have been integrated into Visual Studio 2015 under the names IntelliTest and Fakes. Moles/Fakes is used to isolate test cases and can replace any method with a delegate. Pex iteratively applies symbolic execution to create test vectors in order to cover all branches of the method under test. The Microsoft tool chain does not provide any standard methodology to combine both tools. In summary, all mentioned approaches try to reduce the number of required test cases by testing only unverified control flows. They try to handle incomplete verification results by achieving high test coverage on the unverified software components. No mentioned approach handled the residual risk of tested source code on vulnerable code sections. Therefore, they mark code sections as formally correct, even when those sections may contain serious errors caused by failed guarantees in tested code.

Methodology

The presented methodology integrates into existing workflows combining formal verification and dynamic testing techniques. Figure 2 shows an abstract illus-Fig. 2: Abstract workflow to combine formal verification and testing techniques tration on how current approaches combine verification and testing. The input to those workflows is the program source code and its specification. The proofobligation-generator analyses the source code and the specification to generate a set of proof obligations. In the second step, those proof obligations are verified by the verification backend. This step divides the set of proof obligations into a verified and unverified subset. In step 3, unverified proof obligations are further analysed by a test case generation framework. Those frameworks use symbolic execution (also known as concolic testing) to automatically create test cases and test vectors to explicitly cover control flows of unverified proof obligations. The presented methodology adds two new steps to existing workflows. In step 2B, the POG inspector analyses the dependencies between verified and unverified proof obligations in order to identify vulnerable code sections. Step 3B generates robustness tests for those vulnerable POGs. These tests simulate errors within the tested code and uncover locations where additional error handling and sanity checks are required. This section starts by defining proof obligations, then describes how to identify vulnerable code sections, illustrates their risks and finally explains how to generate corresponding robustness tests.

Proof Obligations

We start by defining the input to our methodology and corresponding symbols to refer to the different components of object oriented programs. The input to the proof obligation inspector is a set of verified and unverified proof obligations Definition 2 (Proof Obligation). The set of all generated proof obligations is Π. A proof obligation π Ω, S, φ is a triple, combining a set of assumptions (Ω), a control flow ( S), and a verification goal (φ). We refer to the method which contains the control flow S by m π . Assumptions and goals are represented as boolean predicates. A proof obligation is verified iff one can show that each execution of S validates φ while assuming Ω. The predicate Ψ π is true iff π can be verified. A proof obligation is always generated based on a specification γ b Γ , we write Πγ π.

Let's apply this to our running example. Here we can extract two work flows and POGs: s1 s 12 , s 13 , s 14 , s 15 e and s2 s 12 , s 13 , s 14 , s 17 , s 18 , s 19 e. The indexes s i mark the global line number of the corresponding statement. The unverified invariant φ 1 U sedLength d Length is covered by two proof obligations:

Ω 1 cutLength e 0, CutLength! null in π 1 Ω 1 , s1 , φ 1 and π 2 Ω 1 , s2 , φ 1 .

Identifying Vulnerable Proof Obligations

The verification framework (Step 2 in Fig. 2) divides the set of POGs Π into a set of verified POGs Π π b ΠΨ π and a set of unverified POGs Π π b Π2Ψ π. Modular verification techniques build their correctness proof upon dependencies between different POGs. Those dependencies must be considered when testing unverified POGs. In step 3B of Fig. 2, we identify POGs depending on unverified code. We call them vulnerable proof obligations.

Definition 3 (Vulnerable Proof Obligations). One proof obligation π i Ω i , si , φ i depends on a different proof obligation π j Ω j , sj , φ j iff the assumption list Ω i contains the verification goal φ j :

π i Ø π j § ω b Ω i ω ¡ φ j (1) One proof obligation π i is vulnerable iff π i Ø π j D 2Ψ π j .
The set of all vulnerable proof obligations is defined as

Π ? π i π i Ø π j D 2Ψ π j .
public L i s t <Bar> C r e a t e B a r s ( L i s t <double> cutLengths , D i c t i o n a r y <double , int> m a t e r i a l s ) { L i s t <Bar> c u t t i n g L a y o u t s = new L i s t <Bar >() ; To conserve space, we list this example without its specification. This method creates different cutting layouts using the AddCut method. The above defined POG π 2 Ω 1 , s2 , φ 1 of AddCut requires a valid precondition. Therefore, this POG depends on all POGs covering this precondition. One of those POGs is generated based on the following control flow s3 s 2 , s 3 , s 4 , s 5 , s 6 , . . . e for the CreateBars method π 3 Ω 3 , s3 , CLen e 0. This control flow must guarantee that the used cut length is greater than zero before calling AddCut. We call this an explicit dependency. There exists another kind of dependency for all control flows calling AddCut. These code sections depend on the invariants of Bar, such as π 2 , even if these invariants are not explicitly addressed. This is the case because every method requires valid object states when calling their methods. We call this an implicit dependency. Such dependencies are expressed as assumptions and are handled during the POG generation. However, we remember that the POG π 2 could not be verified. Therefore, all POGs calling AddCut in their control flow are considered as vulnerable.

Spreading Errors -The Risk of Vulnerable Proof Obligations

The main risk is the spreading of undiscovered errors in tested code into seemingly unrelated or previously verified code sections. In such cases, errors might be difficult to find, because the error source might be hidden in the method call stack. This is illustrated in Figure 3. The method call graph shows two methods, m 1 and m 3 , both calling method m 2 . The precondition γ 3 of method m 2 must be respected by both calling methods m 1 and m 3 . Therefore, the precondition is covered by two POGs: π 3a for the control flow in that the POG π 3a can not be verified. This makes π 4 vulnerable because it now depends on an unverified POG. Errors in m 1 may cause a failed precondition γ 3 , which produces errors in m 2 even though m 2 has been modularly verified. The result might be an invalid return value of m 2 , which in turn may affect the code section in m 1 handling this return value. Thereby, even the postcondition γ 2 of method m 1 may fail.

The goal of our approach is to identify such risks by testing the method m 2 assuming that γ 3 has failed. This allows us to add additional checks to prevent such an error propagation.

Generating Robustness Tests

In general, robustness tests are used to analyse the behaviour of a program under hostile circumstances. This can be done in different ways. In some cases, it is sufficient to call a method with invalid parameter values. In other cases it is required to modify the tested code in order to simulate failures. In such a scenario, we speak of "Mocked Test Cases". Definition 4 (Mocked Test Case). A test case t b T with test vector Ñ t executes the control flow s: t s. A mocked test case t η @ ή¥ s replaces in s the symbol η by ή before executing s.

Definition 5 (Robustness Tests). A robustness tests t b T ? is used to simulate failed guarantees by injecting invalid symbol values. We use following syntax to express the requirements on a symbol's value: fγq v . When evaluating γ using value v, γ must evaluate to false. Additional test oracles are defined using following syntax: ftq φ The evaluation of test case t must fulfil the boolean condition φ. Invalid symbols must be set during the test case execution and the only location to define them is within the robustness test parameter vector. Therefore it must be possible to back trace those values to the test vector. We use the right arrow syntax to express this trace, e.g. Ñ t Ñ m F. This syntax expresses that the original test vector Ñ t is used to fill the method parameter list Ñ m. These parameter values Ñ m are used to set the class field values F.

We create one robustness test for each POG π i depending on an unverified POG:

T ? ¦ i π i Ω i , Si , φ i b Π ? ¢ t Si (2)
We use the verification goals of all proof obligations covering the tested control flow as additional test oracles:

¦ i t i Si b T ? ¦ j π j Ω j , Sj , φ j b Π ¢ ft i q φ j Si Sj (3)
The way failed guarantees are simulated depends on the POG's origin: If the unverified POG π i was generated to cover the precondition γ pre i of method ṁ, we must create a robustness test which calls ṁ with parameter values Ñ t violating γ pre i :

¦ j π j Ø π i 2Ψ π i ¢ t Sj , Ñ t fγ pre i q Ñ t (4)
If the unverified POG π i was generated to cover the postcondition γ post i of method ṁ, we must inject a return value of ṁ violating γ post i . To inject the simulated return value, we must create a mocked version m of ṁ. The mocked version uses an extended parameter list Ñ m, which allows us to directly set the return value based on Ñ t. We refer to the return value of m by f mq.

¦ j π j Ø π i 2Ψ π i ¢ t ṁ @ m¥ Sj , Ñ t Ñ m f mq fγ pos i q B mG (5)
If the unverified POG π i was generated to cover an invariant γ inv i of class c i , we must inject an invalid object instance. Therefore we must distinguish between two further cases: (1) The POG was generated based on a constructor ċtor.

(2) The POG was generated based on a method ṁ. In the first case, the invalid object instance can be created by a mocked constructor method ctor. The mocked constructor uses an extended parameter list Ñ ctor, which allows us to directly set all class fields F based on Ñ t. In the second case, the invalid instance must be simulated by a mocked copy m of ṁ. The mocked method must set all referenced class fields F of c i based on its own extended parameter list Ñ m.

¦ j π j Ø π i 2Ψ π i ¢ t ċtor @ ctor¥ Sj , Ñ t Ñ ctor F¥ fγ inv i q F (
¦ j π j Ø π i 2Ψ π i ¢ t ċtor @ ctor¥ Sj , Ñ t Ñ m F fγ inv i q F (7)
In our running example, the failed POG was generated to cover an invariant during the execution of AddBar. Therefore, we need to inject the simulated error through a mocked method, which is listed in 1.4. We have added the additional parameters useLength and length to the original parameter list. These values are used in line 6 and 7 to set the invalid object state. Now, we only need to replace calls to AddBar by calls to AddBarMocked when testing CreateBars. We can simulate the invalid object state of Bar by calling AddBarMocked, e.g. with usedLength=7000 and length=5000. The results of the robustness test will show that the created cutting layouts are invalid. Now we know that we need to add extra sanity checks to validate the correctness of cuttingLayouts before return them. This prevents undiscovered errors in AddBar from spreading into code sections where the origin of invalid cutting layouts may be difficult to find.

Reference-Implementation

Applying robustness tests and injecting simulated errors requires more effort than regular testing. Especially creating all required mocks is very labour intense when doing it manually. Therefore, we have implemented our methodology into a new mocking framework to face three major challenges: First, we need to ensure that every tested method is visible and accessible within the test suite. Second, we need to initialise object instances with deliberate states hosting the tested methods. Third, we must create the possibility to inject simulated errors to apply robustness testing. We meet those challenges by creating three different layers of mocked code: The first layer mocks the original source code to provide access to all class fields and methods. The second layer contains the mocked test methods to validate unverified POGs and vulnerable code sections. All steps in both layers can be applied automatically and do not require manual work. The Layer 1 contains a mocked version Prog of Prog to make the complete code base testable. We need to consider that we do not want to test complete methods but explicit control flows of unverified POGs. Those control flows might be extracted from private or abstract methods. In Prog we set the visibility of each class field and tested method to public. We have chosen this way, because it is language independent. other solutions for accessing private symbols require language specific runtime flags or reflection APIs. We remove the abstract attribute from each tested class and method. Instead, we add an empty default implementation and a corresponding default return value to each pure abstract method so our program can be compiled. To be able to initialise every object type, we add a default constructor and a static initialisation method to each user-defined type. To create those initialisation methods, we use the recursive Algorithm 1 to inspect aggregated object types c b C. The algorithm extracts a list with parameters representing the aggregated primitive values. To that end, we also create items to fill used collection types, such as Lists, Arrays or Dictionaries. The number of items are added is set with the constant CollectionSize. Recursively analysing the key and value types, we merge the resulting parameter lists. To prevent endless recursion steps, we track the recursion depth with the map RecursionDepthc N) until the maximum recursion depth M axRecursion has been reached. Layer 2 contains the mocked methods and constructors to inject invalid return types and object states. Invalid return values and object states are injected by setting corresponding class fields or by creating corresponding return values, instead of computing them. We use Algorithm 1 to extract the list of required primitive types in order to manipulate or initialise the aggregated object. These extracted primitive types are added to the parameter list of the mocked method. Thereby, we can use the parameter list to explicitly control return values and object states. An example is given in Listing 1.7, in line 6 and 7. Layer 3 contains the actual robustness tests calling the mocked test methods in layer 2. The parameter lists of test cases in this layer combine the extended parameter lists of called mocked methods. Errors can be injected by assigning corresponding parameter values. This might require additional manual work, if the list of parameters is to long and cannot be automatically covered by a symbolic execution tool like Pex.

Case Studies

The real world case study 'Settings Manager' (SM) is extracted from an industrial machine control software. The case study 'Cutting Stock' (CS) is the program hosting our running example. The program creates a list of cutting layouts based on the lengths and quantities of material and pieces. The case study 'Lending Library' (LL) is a small code example to manage the rental and return of items. All three studies are implemented in C# and use Code Contracts as specification language. Table 1 summarises the main properties. We compare our methodology with results of current verification and testing techniques. We apply Microsoft Code Contracts as formal verification framework and IntelliTest as automatic test case generation framework. To get detailed POG information, we have implemented our own POG generator based on [START_REF] Beckert | Verification of object-oriented software: The KeY approach[END_REF] and [START_REF] Huster | More flexible object invariants with less specification overhead[END_REF]. The results are summarised in Table 2. To benchmark the achieved benefits, we analyse the results of the generated robustness tests, and analyse whether they triggered an error within the vulnerable code. The resulting table lists those errors as "Robustness Errors". This table also lists the automatically achieved test coverage by regular test cases on unverified proof obligations. C o n t r a c t . R e q u i r e s ( t a r g e t V a l u e s . ContainsKey ( targetName ) ) ;

C o n t r a c t . R e q u i r e s ( t a r g e t S c o p e s . ContainsKey ( targetName ) ) ;

C o n t r a c t . E ns u re s ( C o n t r a c t . R e s u l t <System . Object >() != null ) ;

if ( ! t a r g e t V a l u e s . ContainsKey ( targetName ) )

{

Conclusion and Future Work

Our case studies have shown that automatic test frameworks already achieve high coverage rates on unverified code sections. This poses the risk that such test suites might never be checked manually by the corresponding developer to identify insufficient test cases, as shown in Listing 1.2. That makes the inspection of code sections that rely on the correctness of the tested code particularly important. Even tested methods, entirely covered, may still contain errors. Therefore, only testing unverified code sections is insufficient when combining formal verification and dynamic testing techniques. Undiscovered errors in tested code my spread into other code sections, even those sections that have been previously verified. Such errors may be hard to debug, as they might be camouflaged after having been propagated through different methods. This was demonstrated in our running example extracted from the Cutting Stock case study. These risks are not handled by current approaches.

To reduce this residual risk, we have presented a new methodology to use robustness testing to handle incomplete verification results. We extract the guarantees of unverified proof obligations and use them to create and inject simulated errors. Those errors test the behaviour of vulnerable code sections in situations when those guarantees fail. The presented reference-architecture demonstrates how robustness tests can be generated and how simulated errors can be injected. By injecting simulated errors, the developer can analyse the consequences of failed guarantees. They can add further exception handling and sanity checks to prevent the propagation of previously undiscovered errors into other methods. The software can then handle errors in a controlled way rather than defaulting to unpredictable behaviour. It could be argued that developers can always add more exception handling and state checking. But this would be very labour intense when applied for every return value and argument. Furthermore, these sanity checks must be tested as well, requiring many robustness tests to cover the corresponding program paths. The presented methodology helps the developer to localise precisely those code sections, where additional error handling is required.

Finally, one major issue regarding formal verification needs to be addressed in future work. There is still no proper way to tell whether the defined specifications are sufficient and cover all necessary requirements. When the specification is insufficient, the number of generated POGs may be too small to properly analyse dependencies between them in order to identify vulnerable sections. Future work must find more sophisticated coverage rates for specifications.

Fig. 1 :

 1 Fig. 1: Code Contracts marks unverified invariant

Listing 1 . 1 :Listing 1 . 2 :

 1112 public class Bar { public double Length , UsedLength , MinSpace ; public L i s t <Double> Cuts ; [ C o n t r a c t I n v a r i a n t M e t h o d ] private void O b j e c t I n v a r i a n t ( ) { C o n t r a c t . I n v a r i a n t ( UsedLength >= 0 ) ; C o n t r a c t . I n v a r i a n t ( UsedLength <= Length ) ; C o n t r a c t . I n v a r i a n t ( Cuts != null ) ; } public Bar ( double l e n g t h , double minSpace ) { [ . . . ] } public bool AddCut ( double cutLength ) { C o n t r a c t . R e q u i r e s ( cutLength > 0 ) ; double usedSpace = Cuts . Count * MinSpace ; if ( ( Length UsedLength usedSpace ) < cutLength ) { return false ; } UsedLength += cutLength ; Cuts . Add( cutLength ) ; return true ; } } Code Contracts: Unverified Invariant public void TestAddCut ( ) { Bar bar = new Bar ( 5 0 0 0 , 5 ) ; bool couldAdd = bar . AddCut ( 1 5 0 0 ) ; A s s e r t . I s T r u e ( couldAdd && bar . UsedLength == 1 5 0 0 ) ; couldAdd = bar . AddCut ( 5 5 0 0 ) ; A s s e r t . I s T r u e ( ! couldAdd && bar . UsedLength == 1 5 0 0 ) ; } Testing unverified method because undiscovered errors regarding failed guarantees produce further failures.

  (POG). The POGs are generated based on the source code of an object-oriented program Prog and its specification set Γ Prog . This program contains classes c b C Prog . Each class can contain methods m b M c and fields f b F c . A method consists of an ordered set of statements s b Se m . The list of method parameters is Ñ m. The specification can contain preconditions Γ pre m , postconditions Γ post m , and object invariants Γ inv c . The proof of the overall correctness is divided into a generated set of proof obligations. Each proof obligation covers one control flow: Definition 1 (Control Flow). A control flow S s 0 , . . . , s n e is a set of statements s i b S m , m b M c . Between each pair of statements s i and s i1 exists one unique transition.

  foreach ( double cLen in c u t L e n g t h s ) { bool couldAdd = false ; foreach ( Bar bar in c u t t i n g L a y o u t s ) { if ( bar . AddCut ( cLen ) ) { couldAdd = true ; break ; } } if ( ! couldAdd ) { double bfLength = Double . MaxValue ; foreach ( double matLength in m a t e r i a l s . Keys ) { double o f f c u t = matLength cLen ; if ( o f f c u t > 0 && o f f c u t < bfLength cLen && m a t e r i a l s [ matLength ] > 0 ) { bfLength = matLength ; } } if ( bfLength < Double . MaxValue ) { Bar newBar = new Bar ( bfLength , 5 ) ; newBar . AddCut ( cLen ) ; c u t t i n g L a y o u t s . Add( newBar ) ; m a t e r i a l s [ bfLength ] = 1 ; } } return c u t t i n g L a y o u t s ; } Listing 1.3: Implicit depending code Let's have a look what dependencies and vulnerable code section we can identify in our running example. Listing 1.3 shows another code section of the Cutting Stock program.

Fig. 3 :

 3 Fig. 3: Method call graph (Top) and possible POG dependency graph (Bottom)

  Algorithm to generate initialisation parameter lists third layer contains the actual test cases.

	Algorithm: InitList(c)
	Globals: RecursionDepth, M axRecursion, CollectionSize
	begin
	if RecursionDepth c¥ e M axRecursion then return c IP ¢ g
	RecursionDepth c¥ foreach f b Fc do if IsSimpleT ypef then IP IP 8 T ypef
	else if IsCollectionf then
	for i 0 CollectionSize do
	if HasKeyT ypef then IP IP 8 InitListKeyT ypef IP IP 8 InitListV alueT ypef
	end
	else IP IP 8 InitListT ypef
	end
	RecursionDepth c¥
	return IP ;
	end
	Algorithm 1:

Table 1 :

 1 Overview case studies

		Settings	Cutting Stock	Lending
		Manager (SM)	(CS)	Library (LL)
	LOC	1277	634	432
	Preconditions	46	32	12
	Postconditions	22	19	13
	Invariants	21	13	15
	Proof Obligations	187	115	52
	5.1 Case Study: Settings Manager
	We have created 187 POGs to cover all 89 single specifications. The verifica-
	tion framework left 4 POGs unverified, covering different preconditions. The

public object GetValue ( string targetName ) { [ . . . ]

  Listing 1.5 shows one of those unsecured code sections. The precondition in line 3 could not be verified for each caller. To handle this incomplete verification result, related approaches create test cases to validate the unverified caller. In addition, we use robustness tests to analyse the consequences of a failing precondition. The robustness tests created by our approach call this method with a value for target-Name which explicitly invalidates the precondition in line 2, while respecting all other assumptions. Thereby, we discovered the potential KeyNotFound-Exception in line 8, which would cause a software crash. This distinguishes a robustness test from a regular test. Regular test coverage could be achieved by testing this method while respecting both preconditions, but such tests would not trigger the error in line 8. This method was programmed based on the assumption that both containers (targetScopes and targedNames) share the same keys. Therefore the programmer checked the key only for one container. After discovering this risk, the developer could add additional exception handling similar to the one in lines 5-6. One of them was already discussed above and used as the running example. Another unverified POG covers the postcondition of GetFreeClamp in Listing 1.6. This method is called by a different method AssignClamps, which of course depends on the validity of that postcondition. AssignClamps calculates the required Clamp positions for the cutting machine, which is used to produce the generated cutting-layouts. Wrong clamp positions may cause damage to the machine, e.g. when the saw hits a wrongly positioned clamp. Therefore, we want to test the behaviour of AssignClamps when this postcondition fails, in order to private Clamp GetFreeClampMocked ( double minPos 1 , double maxPos 2 , bool f r e e 3 , double minPos 4 , double maxPos 5 ) { GetFreeClamp into AssignClamps. Our framework generates the mocked copy GetFreeClampMocked in Listing 1.7. In AssignClamps, all method calls to the original methods are replaced in order to call the mocked copy. As described in Section 4, the mocked method uses an extended parameter list to initialise the returned object: free 3, minPos 4, maxPos 5. These parameters map to the basic field values of class Clamp. Thereby it is possible to return a Clamp instance which is not null and which does not meet the defined postcondition. The analysis of this robustness test shows that the simulated error caused an invalid return value for AssignClamps. An invalid return value would cause invalid cutting layouts, leading to faulty production in the real world. What makes this bug particular dangerous is the absence of easily detectable errors such as exceptions or a crash. The problem would not have been detected until someone tried to produce the erroneously calculated cutting layouts. Analysing the robustness test, the developer can add an additional sanity check within AssignClamps and make sure that the results meet all requirements. RentalItem is actually rented and not returned. This state is encoded as an boolean class field. The related precondition could not be verified. However, this flag is already checked in line 2 and the robustness test could not trigger any new error.

	public bool ReturnItem ( RentalItem item ) {
	if ( ! item . Rented ) { return false ; }
	Clamp clamp = new Clamp ( ) ; [ . . . ] }
	clamp . I n i t ( f r e e 3 , minPos 4 , maxPos 5 ) ; return clamp ; } Listing 1.8: Existing checks also handle simulated errors
	throw new UnkownTargetException ( " [...] " ) ; } // Exception when targetName is no key [...] } Listing 1.7: Mocked method to inject invalid return values method requires that the given
	S e t t i n g S c o p e t a r g e t S o p e = t a r g e t S c o p e s [ targetName ] ;
	guarantee safe error handling. The corresponding robustness test must inject an Listing 1.5: Vulnerable code section which can causes a software crash automatically generated test suite achieved 92% branch coverage on those 4 un-verified control flows. Analysing those 4 unverified POGs, we could identify 18 vulnerable proof obligations. Two of them were not sufficiently secured against undiscovered errors. invalid return value for { return clamp ; } 5.2 Case Study: Cutting Stock }
	return null ; } This case study is comprised of 64 specifications, which are covered by 115 POGs. The verification framework left 7 POGs unverified (4 invariants, 2 preconditions, Listing 1.6: Code section with an unverified postcondition
	1 postcondition). The automatically generated test suite achieved 94% branch coverage on those 7 unverified control flows. We could identify 23 vulnerable 5.3 Case Study: Lending Library
	proof obligations. The smallest case study, 'Lending Library' was specified using 30 conditions,
	which were covered by 54 generated POGs. The verification step left 6 proof
	obligations unverified (3 invariants, 2 postconditions, 1 precondition). Based on
	those 6 unverified POGs, we could identify 12 vulnerable code sections. The cor-
	responding robustness tests discovered 3 critical code sections where additional
	sanity checks were required. Now someone could wonder about the vulnerable
	sections where no robustness error was found. The answer is very simple. The
	other 9 vulnerable code sections already contained error handling code, so no
	additional code needed to be added. An example is given in Listing 1.8. This

private Clamp GetFreeClamp ( double minPos , double maxPos ) { C o n t r a c t . E ns u re s ( C o n t r a c t . R e s u l t <Clamp>() == null | | ( C o n t r a c t . R e s u l t <Clamp>() . f r e e && C o n t r a c t . R e s u l t <Clamp>() . minPos <= minPos ) ) ; foreach ( Clamp clamp in clamps ) { if ( clamp == null ) continue ; if ( clamp . minPos <= minPos && clamp . maxPos >= maxPos )

Table 2 :

 2 Comparsion between both approaches

		SM	CS	LL
	Unverified Proof Obligations	4	7	6
	Autom. achieved code coverage	92%	94%	98%
	Identified Vulnerable Code Sections	18	23	12
	Discovered Robustness Errors	2	5	3


Nassim Benharrat

Christophe Gaston

Robert M Hierons
email: rob.hierons@brunel.ac.uk

Arnault Lapitre

Pascale Le Gall

Constraint-based oracles for timed distributed systems

Keywords: Model-based testing, Distributed testing, Timed Input Output Transition Systems, Off-line testing, Constraint-based testing

This paper studies the situation in which the system under test and the system model are distributed and have the same structure; they have corresponding remote components that communicate asynchronously. In testing, a component with interface Ci has its own local tester that interacts with Ci and this local tester observes a local trace consisting of inputs, outputs and durations as perceived by Ci. An observation made in testing is thus a multi-trace: a tuple of (timed) local traces, one for each Ci. The conformance relation for such distributed systems combines a classical unitary conformance relation for localised components and the requirement that the communication policy was satisfied. By expressing the communication policy as a constraint satisfaction problem, we were able to implement the computation of test verdicts by orchestrating localised off-line testing algorithms and the verification of constraints defined by message passing between components. Lastly, we illustrate our approach on a telecommunications system.

Introduction

Distributed systems can be seen as collections of physically remote reactive systems communicating through communication media. The classical approach to testing such systems involves placing a local tester at each localised interface, with each local tester only observing the events at its interface. If testers do not exchange synchronisation messages and there is no global clock, this corresponds to the ISO standardised distributed test architecture [11]. The result of test execution can be modelled as a collection of logs (local traces); each is a sequence of messages involving a given localised system.

Model-Based Testing (MBT) [START_REF] Grieskamp | Model-based quality assurance of protocol documentation: tools and methodology[END_REF][START_REF] Petrenko | Testing from Partial Deterministic FSM Specifications[END_REF][START_REF] Tretmans | Formal methods and testing. chapter Model Based Testing with Labelled Transition Systems[END_REF] aims to automate three central processes in testing, namely: the test generation process whose purpose is to extract test cases from a behavioural model of the System Under Test (SUT), the test execution process whose purpose is to orchestrate the stimulation of the SUT with input test data and the collection of the SUT's reactions and finally, the verdict (oracle) computation phase whose purpose is to analyse the results of test case executions, given as execution traces, in order to identify faults by checking traces against the model 4 . This comparison is based on a conformance relation that relates traces of SUTs and traces of their associated models.

MBT was first explored in a centralised context but extensions to distributed SUTs have been defined, initially motivated by protocol conformance testing [START_REF] Sarikaya | Synchronization and specification issues in protocol testing[END_REF]. This includes work that uses Input Output Transition System (IOTS) as the modelling formalism [START_REF] Brinksma | Factorized test generation for multiinput/output transition systems[END_REF][START_REF] Hierons | Implementation Relations for the Distributed Test Architecture[END_REF][START_REF] Hierons | Using Time to Add Order to Distributed Testing[END_REF]. In the context of distributed testing from Timed IOTS (TIOTS), in [START_REF] Gaston | An implementation relation and test framework for timed distributed systems[END_REF], we extended the tioco conformance relation [START_REF] Krichen | Black-box conformance testing for real-time systems[END_REF][START_REF] Krichen | Conformance testing for real-time systems[END_REF][START_REF] Schmaltz | On Conformance Testing for Timed Systems[END_REF] to define a conformance relation dtioco for timed distributed testing. The model of a distributed SUT is given as a tuple of TIOTSs, each modelling one of the localised subsystems of the SUT. The result of test case execution is a tuple of timed traces (a timed trace is a trace in which delays between consecutive interactions of the tester with the localised SUT are recorded). Under the hypothesis that localised systems communicate in a multi-cast mode, we have shown that the verdict computation process can be conducted by combining centralised MBT techniques for each localised system, using the tioco conformance relation, and a step-by-step algorithm whose purpose is to check that the tuple of timed traces is consistent with the underlying communication hypothesis [START_REF] Gaston | An implementation relation and test framework for timed distributed systems[END_REF].

The goal of this paper is twofold. First, we propose an improvement of the algorithm presented in [START_REF] Gaston | An implementation relation and test framework for timed distributed systems[END_REF] by formulating the oracle problem as a constraint solving problem. While the previous algorithm analyses a multi-trace by mimicking step by step emissions and receptions of messages, as well as the passage of time, in this article, we reformulate the verification of message passing as a set of inequality constraints that can be supported by a constraint solver. Compared to the one introduced in [START_REF] Gaston | An implementation relation and test framework for timed distributed systems[END_REF], the new algorithm treats durations between communication actions as real numbers. In [START_REF] Gaston | An implementation relation and test framework for timed distributed systems[END_REF] those durations had to be representable as multiples of a basic time unit, which only allowed us to consider durations in a set isomorphic to the set of natural numbers. The previous approach also included backtracking. In the new algorithm, durations may be any real number that falls in the theory addressed by the considered solver. Second, we present the tool that solves the oracle problem using both a localised verdict computation approach for tioco (presented in [START_REF] Bannour | Off-line test case generation for timed symbolic model-based conformance testing[END_REF]) and the verification of constraints to check internal communications between localised systems. We consider a case study modelling a telecommunication system, named PhoneX [START_REF]Ericsson Int. report. Investigation on how to integrate Diversity (MBT tool) and Titan (TTCN-3 executor) to provide an open source MBT tool chain[END_REF] specified as a collection of Timed Input Output Symbolic Transition Systems (TIOSTS), which are symbolic representations of TIOTS.

Section 2 introduces the types of models used and Section 3 presents the PhoneX case study. Section 4 recalls the testing framework and introduces the verification of message passing using constraints. Section 5 describes a scalability study, based on the PhoneX example, that applied mutation techniques to generate correct and faulty trace tuples. Section 6 discusses related works and Section 7 gives concluding remarks.

Modelling framework

TIOSTS

Timed Input Output Symbolic Transition Systems (TIOSTS) are symbolic automata built over a signature Σ = (Ω, A, T, C) where Ω = (S, F ) is an equational logic signature with S a set of types and F a set of functions provided with an arity. The functions are interpreted in a model M as usual. A is a set of data variables used to store input values, to denote system state evolutions and to define guards. T is a set of clocks, which are variables whose values are elements of a set D isomorphic to non-negative real numbers and that are used to denote durations. D + will denote D \ {0}. M is supposed to contain D. Variables in A ∪ T are assigned values by interpretations of the form ν : A ∪ T → M ; M A∪T is the set of all interpretations. Finally, C is a set of channels partitioned as C in C out where elements of C in (resp. C out ) are input (resp. output) channels. The set of terms T Ω (A) over Ω and A is inductively defined as usual and variable interpretations are canonically extended to terms. The set of symbolic actions Act(Σ) is

I(Σ) ∪ O(Σ) with I(Σ) = {c?x|x ∈ A, c ∈ C in } and O(Σ) = {c!t|t ∈ T Ω (A), c ∈ C out }.
In order to simplify the exposition, at the level of our modelling framework, we consider messages that contain only a single piece of data. However, at the tooling level, without adding any particular difficulties, messages contain 0 (signals c! or c?), 1 or n data (c!(t 1 , . . . , t n ) or c?(x 1 , . . . , x n ), the x i being different variables of A).

A TIOSTS is a triple G = (Q, q 0 , T r) where Q is a set of states, q 0 is a distinguished element of Q called the initial state, and T r is a set of labeled transitions. A transition is defined by a tuple (q, φ, ψ, T, act, ρ, q ) where q (resp. q ) is the source (resp. target) state of the transition, φ is a formula, called time guard, of the form z ≤ Cst or z ≥ Cst where z ∈ T and Cst is a constant interpreted in D (φ constrains the delay at which the action act occurs), ψ is an equational logic formula, called data guard (ψ is a firing condition on attribute variables), T ⊆ T is a set of time variables (to be reset to 0 when the transition is executed), act is a communication action and ρ assigns terms of T Ω (A) to variables in A in order to represent state evolutions. In the sequel, we use M |= ν ϕ to say that ϕ holds for interpretation ν. The set of paths of G contains the empty sequence ε and all sequences tr 1 . • • • .tr n of transitions of T r such that source(tr 1 ) = q 0 and for all i < n, target(tr i ) = source(tr i+1 ).

Concrete actions are values exchanged through channels. The set of concrete actions over C is thus Act

(C) = I(C) ∪ O(C) where I(C) = {c?v | c ∈ C in , v ∈ M } are inputs and O(C) = {c!v | c ∈ C out , v ∈ M }
are outputs. Given act ∈ Act(C) of the form c∆v with ∆ ∈ {!, ?}, chan(act) refers to c, act refers to its mirror action, c∆v with ! =? and ? =!. Variable interpretations are canonically extended to symbolic actions (ν(c?x) = c?(ν(x)) and ν(c!t) = c!ν(t)).

A concrete action is generally observed after a delay has occurred since the previous occurrence of a concrete action. This is captured by the notion of events. Definition 1 (Events). The set of (resp. initialised) events over C is defined as

Evt(C) = (D + ∪{ })×(Act(C)∪{δ}) (resp. IEvt(C) = D + ×(Act(C)∪{δ})).
Pair (d, a) represents the observation of concrete action a after delay d. Following [START_REF] Tretmans | Formal methods and testing. chapter Model Based Testing with Labelled Transition Systems[END_REF], symbol 'δ' is used to denote the absence of observation of a concrete action (i.e. quiescence). Let us point out that usually, in a pure timed framework, δ may be useless (e.g. [START_REF] Gaston | An implementation relation and test framework for timed distributed systems[END_REF][START_REF] Krichen | A formal framework for black-box conformance testing of distributed real-time systems[END_REF][START_REF] Krichen | Black-box conformance testing for real-time systems[END_REF]). Here, the use of δ is a side effect of considering atomic actions as events. Indeed, expressing that a system is quiescent after a duration d has to be representable as an event, and thus, we need a symbol to represent these quiescent situations as a couple (d, δ). Symbol ' ' is introduced to denote the absence of the observation of a delay (i.e ( , a)). We require this so that the first action of a localised trace need not be stamped with a duration. In addition, between two consecutive concrete actions on one location, we require that the delay is greater than zero so that two events do not occur simultaneously. Given ev ∈ Evt(C), we let act(ev) = a and delay(ev Any event of an initialised trace contains a duration and a concrete action. For the first event, this duration represents a delay between some distinguished moment (e.g. since the time at which a tester started to measure the duration) and the first observed action. Uninitialised traces are timed traces for which no initial instant is identified. Finally, note that quiescence is only observed at the end of traces, when no communication action follows it. Indeed when a communication action a occurs after a period of time where an implementation remains silent, this period of time is captured by the delay of the event introducing a.

) = d if ev = (d,
For σ ∈ T T races(C), dur(σ) denotes the duration of σ, which is 0 if σ is ε, and otherwise is the sum of all delays of events in σ. P ref (σ) denotes the set of prefixes of σ defined as {ε} if σ is ε and P ref (σ ) ∪ {σ} if σ is of the form σ .ev. Moreover, for an action a in Act(C), |σ| a denotes the number of occurrences of a in σ. pref (σ, a, n) stands for the smallest prefix of σ that contains n occurrences of a when this prefix exists. Finally, using the pref operation, we introduce an operation that measures the elapsed time at the nth occurrence of an event a from the beginning of the trace. By convention, if a trace contains strictly fewer than n occurrences of a, then the associated duration is that of the entire trace.

dur occ(σ, a, n) = dur(pref (σ, a, n)) if pref (σ, a, n) exists dur(σ) else
We now define runs of transitions of TIOSTS:

Definition 3 (Runs of transitions). Let G = (Q, q 0 , T r) be a T IOST S over Σ. The set Snp M (G) of snapshots of G is the set Q × M A∪T . For tr = (q, φ, ψ, T, act, ρ, q ) ∈ T r, the set of runs of tr is the set Run(tr) ⊆ Snp M (G) × Evt(C) × Snp M (G) s.t. ((q, ν), ev, (q , ν )) ∈ Run(tr) iff there exist d ∈ D and ξ : A ∪ T → M satisfying: -for all w ∈ T , ξ(w) = ν(w) + d, -if act = c!t then for all x ∈ A, ξ(x) = ν(x), else (act = c?x) for all y ∈ A \ {x}, ξ(y) = ν(y),
and such that we have either ev = (d, ξ(act))

or ev = ( , ξ(act)), ∀x ∈ A, ν (x) = ξ(ρ(x)), ∀w ∈ T, ν (w) = 0, ∀w ∈ (T \ T), ν (w) = ξ(w), M |= ξ φ and M |= ξ ψ.
In Definition 3, ξ is an intermediate interpretation whose purpose is to let time pass from ν for all clocks (ξ(w) = ν(w)+d) and take into account a potential input value (denoted by ξ(x) if act = c?x). Guards of the transition should be satisfied by ξ and if it is the case then the transition can be fired resulting on a new interpretation ν updating data variables according to ρ and resetting clocks occurring in T.

For a path p of G, the set of timed traces of p, denoted T T races(p) is {ε} if p = ε and if p is of the form tr 1 . • • • .tr n , T T race(p) contains all sequences of events ev 1 • • • ev n such that there exists a sequence of runs r 1 • • • r n satisfying: for all i ≤ n, r i is a run of tr i of the form (snp i , ev i , snp i+1 ) and for all j < n we have snp j = snp j+1 and such that all events are initialised except for i = 1, i.e. ev 1 is of form ( , a 1 ) and for all i > 1, ev i is of form (d i , a i ).

By taking into account the particular action δ, the set of timed traces of G, denoted T T races(G), is defined as:

-For all p ∈ P ath(G) we have T T races(p) ⊆ T T races(G), -For all σ ∈ T T races(G) such that there exists no path p and no event ev with act(ev

) ∈ O(C) satisfying σ.ev ∈ T T races(p), we have σ.(d, δ) ∈ T T races(G) if σ = ε and ( , δ) ∈ T T races(G) if σ = ε.

Communication and systems

We now define a distributed interface as a collection of localised interfaces.

Definition 4 (Distributed interface). A distributed interface is a tuple Λ = (C 1 , • • • , C n ), with n ≥ 1,
where for all i ≤ n, C i is a set of channels such that for any i = j we have

C out i ∩ C out j = ∅. C(Λ), which is equal to i≤n C i , is the set of channels of Λ with C(Λ) in = i≤n C in i and C(Λ) out = i≤n C out i . C out i ∩ C out j = ∅
ensures that for a channel c, messages emitted through c can only be emitted from one sender. This is a simplification hypothesis that makes the later formalisation lighter. In a distributed architecture, for a given localised interface

C i of Λ = (C 1 , • • • , C n ), C int i (resp. C ext i ), defined as {C i ∩ C j |j ≤ n ∧ j = i} (resp. C i \C int i )
, denotes the set of internal channels (resp. external channels) that can be used to exchange messages with other localised subsystems (resp. exchange messages with the system environment). We let

C int (Λ) denote i≤n C int i , C ext (Λ) denote i≤n C ext i , and Act(Λ) de- note I(Λ) ∪ O(Λ) with I(Λ) = i≤n I(C i ) and O(Λ) = i≤n O(C i ). I int (Λ) (resp. O int (Λ)) is the subset of I(Λ) (resp. O(Λ)) whose elements are inputs (resp. outputs) through internal channels. For any c!v ∈ O(Λ), Sender(Λ, c!v) stands for the index j such that c ∈ C out j . We let Act int (Λ) = I int (Λ) ∪ O int (Λ), Evt(Λ) = Evt(C(Λ))
, and Evt int in (Λ) be the set of events whose action is an internal input. We define T up(Λ) to be T T races

(C 1 ) × • • • × T T races(C n ). In the sequel, a distributed interface Λ = (C 1 , • • • , C n ) is
given. An observation made in a system will be a tuple of timed traces where each timed trace represents a local observation. We first introduce the notion of a multi-trace, which is a tuple of timed traces characterising compatible communications between a collection of localised subsystems. The set U M T races(Λ) (resp. M T races(Λ)) of uninitialised multi-traces (resp. of multi-traces

) of Λ is {(u(σ 1 ), • • • , u(σ n ))|(σ 1 , • • • , σ n ) ∈ IM T races(Λ)} (resp. U M T races(Λ) ∪ IM T races(Λ)).
Initialised multi-traces denote tuples of traces, each trace of the tuple being a partial centralised vision of a common distributed execution. The nature of communication considered is multicast, as captured by the property that an internal message can be received at some C i only if C i has consumed fewer occurrences of this message than the number of the corresponding output occurrences. Each trace occurring in an initialised multi-trace starts with an event introducing a duration. All those durations are supposed to start at a common initial instant. Of course, in the context of distributed executions it is generally not possible to observe such a common initial instant. Therefore, we defined uninitialised multitraces in which the initial durations are not observable. Similar rules have been proposed in [START_REF] Nguyen | A framework for distributed testing of timed composite systems[END_REF] to express component composition in a distributed setting.

In distributed testing, we assume that there is a separate tester at each localised interface and there is no global clock for globally ordering distributed events. Hence, we cannot make any assumption on the different moments at which the different local testers stop observing their associated interfaces. To capture this, we accept as valid observations, tuples made of multi-trace prefixes.

Definition 6 (Observable multi-traces). The set of initialised observable multi-traces of Λ, denoted IOT races(Λ), is the smallest set containing IM T races(Λ) and such that for any (σ

1 , • • • , σ i .ev, • • • , σ n ) ∈ IOT races(Λ) we have (σ 1 , • • • , σ n ) ∈ IOT races(Λ).
The set of uninitialised observable multi-traces of Λ, denoted U OT races(Λ),

is the set {(u(σ 1 ), • • • , u(σ n ))|(σ 1 , • • • , σ n ) ∈ IOT races(Λ)}.
Initialised observable multi-traces characterise observations starting at a common initial instant but ending at different instants depending on the considered component of the interface. Of course, since there is a common initial instant it is possible to order the moments at which the observations of the different traces of the tuple occur (σ i ends before σ j if dur(σ i ) < dur(σ j )). However, in general such an initial instant cannot be identified in testing. Therefore, real observations of system executions should be defined by tuples containing only uninitialised traces, which is captured by uninitialised observable multi-traces.

Definition 7. Let Λ = (C 1 , • • • , C n ) be a distributed interface. A system over Λ is a tuple Sys = (G 1 , • • • G n ) such that for all i ≤ n we have G i is a TIOSTS over a signature of the form (Ω i , A i , T i , C i ). The semantics of Sys, denoted T T races(Sys) is defined as (T T races(G 1 )ו • •×T T races(G n ))∩U OT races(Λ).

The PhoneX case study

PhoneX [START_REF]Ericsson Int. report. Investigation on how to integrate Diversity (MBT tool) and Titan (TTCN-3 executor) to provide an open source MBT tool chain[END_REF] is a central telecommunication system model describing a protocol to establish sessions between phones. It was initially used as a reference to investigate the test case generation capacities of the platform Diversity6 by the Ericsson company. In our context, PhoneX is interesting since it allows the number of communicating actors to be parameterised, even though there is only one time constraint in the subsystem models. Fig. 1 Then it joins PhoneX central by sending to it src and dest (caller reaches Initiating state). Caller returns to Idle state when it receives an error code from PhoneX (PhoneX cannot establish a call due to violated condition of call establishment) or a signal to terminate the call from the active session (due to a call rejection by called client). At Initiating, src may reach Established if a call is established by active session or state T erminating if a no-answer (from called client) is observed during a waiting delay. When a call is established (at Established), src may return to Idle by receiving a terminating signal from the active session (due to an ending call by called client) or receive a signal from the environment (a caller) to end the call in progress (caller reaches U serEndingCall). At U serEndingCall, the caller notifies the active session for terminating the call (caller reaches T erminating). At T erminating, src returns to Idle by receiving a terminating signal from the active session.

Called client behaviour (Fig 3(b)

). This role is symmetric (on the called client side) to the one described in Fig 3

Testing

In [START_REF] Gaston | An implementation relation and test framework for timed distributed systems[END_REF], we modelled timed distributed systems as tuples (LS 1 , . . . , LS n ) where each LS i denotes a black box localised system under test. Then we defined a conformance relation dtioco to test such a distributed system with respect to a system model (G 1 , . . . , G n ). We showed that solving the oracle problem for an observable multi-trace (σ 1 , • • • , σ n ) reduces to: (a) solve the oracle problem of each σ i with respect to tioco [START_REF] Krichen | Conformance testing for real-time systems[END_REF] and with G i as reference model (unitary testing, see Section 4.1) and, (b) check whether (σ 1 , • • • , σ n ) is an observable (uninitialised) multi-trace. In Section 4.1 we briefly recall the principles of a simplified7 version of the unitary testing algorithm defined in [START_REF] Bannour | Off-line test case generation for timed symbolic model-based conformance testing[END_REF]. Then in Section Fig. 4: TIOSTSs G X and G S of PhoneX Central and Active Session 4.2, we introduce the new algorithm based on constraint solving to decide if a tuple is an observational multi-trace. As compared to [START_REF] Bannour | Off-line test case generation for timed symbolic model-based conformance testing[END_REF] and [START_REF] Gaston | An implementation relation and test framework for timed distributed systems[END_REF], we have slightly adapted our definitions of timed traces in order to deal with events instead of atomic observations such as inputs, outputs or durations; this adaptation has no impact on the results in [START_REF] Bannour | Off-line test case generation for timed symbolic model-based conformance testing[END_REF] and [START_REF] Gaston | An implementation relation and test framework for timed distributed systems[END_REF].

Unitary testing

A Localised subsystem Under Test (LUT) is defined over a set of channels C as a non-empty subset LS of U OT races(C) such that:

-Input completeness: for any σ in LS of the form σ .ev , for any ev ∈ Evt(C) such that act(ev) ∈ I(C) and delay(ev) ≤ delay(ev ), we have σ .ev ∈ LS. -Quiescence: for all σ ∈ LS we have:

∀ev ∈ Evt(C).(act(ev) ∈ O(C) ⇒ σ.ev / ∈ LS) ⇔ (σ = ε ⇒ (∀d ∈ D + , σ.(d, δ) ∈ LS)) ∧ (σ = ε ⇒ ( , δ) ∈ LS)
Moreover for any σ in LS of the form σ .ev with act(ev ) = δ, for any ev ∈ Evt(C) with act(ev) ∈ O(C) we have σ.ev / ∈ LS. -Reaction prefix: for any σ in LS, we have P ref (σ) ⊆ LS.

Input completeness is required so that an LUT cannot refuse an input from the environment. Quiescence corresponds to situations where the LUT will not react anymore until it receives a new stimulation. Reaction prefix is a realistic property stating that a prefix of an observation is an observation.

The local verdict computation algorithm is based on a symbolic structure SE(G) δ computed from the reference model G obtained by classical symbolic execution techniques. It is a tree-like structure whose nodes are symbolic states used to capture information related to the possible executions of G. A path p is a sequence of consecutive edges relating symbolic states and labelled by symbolic events. The set of executions (uninitialised timed traces) associated to p is characterised by the sequence ev 1 • • • ev n of symbolic events labelling the consecutive edges and by the final symbolic state η. Each symbolic event of the sequence is of the form (d i , act i ) (except ev 1 which is of the form ( , act 1 )). Each d i is a new fresh variable (i.e. not used in the definition of G) used to represent durations (they are typed as clocks) and each act i is of the form c?z i or c!t i where z i is a new fresh variable and t i is a term built over the same equational logic signature Ω as terms in G but on a set of new fresh variables. η is of the form (q, π d , π t , ) where q is the state reached in G, π d is a constraint on new fresh data variables (let F d be the set of those variables), π t is a constraint on the set of variables of the form d i and : A → T Ω (F d ) associates symbolic values to variables of G. An uninitialised timed trace ev 1 • • • ev n belongs to p iff for all i ≤ n:

-ev i is of the form ( , act i ) (resp. (d i , act i )) if ev i is of the form ( , act i ) (resp. (d i , act i )) and act i is of the form c?z i (resp. c!t i ) if act i is of the form c?z i (resp. c!t i ). -Let x i (resp. x i ) stand for the variable z i (resp. z i ) if act i (resp. act i ) is
an input and for the term t i (resp. t i ) if act i (resp. act i ) is an output. The formula ( i≤n

x i = x i ) ∧ π d ∧ π t is satisfiable.
The verdict computation algorithm analyses successively all events of σ = ev 1 • • • ev n and at each steps it computes the set of paths to which the already analysed prefix of σ belongs. As soon as possible a verdict is emitted8 :

-F ail if act(ev i ) is an output or δ and the set of path becomes empty, or else act(ev i ) is an input (d i , act i ) and there exists an event ev i = (d i , act i ) where act i is an output (not δ)

satisfying d i < d i and ev 1 • • • ev i-1 .ev i belongs to some path of SE(G) δ . -Inconc if act(ev i ) is an input (d i , act i )
, the set of path becomes empty, and for all events ev i = (d i , act i ) where act i is an output (not δ), d i < d i we have ev 1 • • • ev i-1 .ev i does not belong to any path of SE(G) δ . -P ass if σ is fully analysed without generating any of the previous verdicts.

Communication testing

An SUT over Λ is a tuple S = (LS 1 , . . . , LS n ) where LS i is an LUT defined over C i (all i ≤ n). The semantics of S, denoted Obs(S) ⊆ LS 1 × • • • × LS n , contains all observations that can be made when executing S. The goal of Algorithm 1 is to check whether those observations reveal communication errors by checking whether they are in U OT races(Λ). It is based on the property that an uninitialised observable multi-trace µ = (σ 1 , • • • , σ n ) is such that each σ i is either empty or of the form ( , a i ).σ i , but in the latter case µ has been obtained from an initialised observable multi-trace of the form µ = (σ 1 , • • • , σ n ) where σ i is ε for σ i = ε and of the form (d i , a i ).σ i for σ i of the form ( , a i ).σ i . Thus, (σ

1 , • • • , σ i .ev, • • • σ n ) ∈ U OT races(Λ) iff there exist durations d 1 , • • • , d n where µ = (σ 1 , • • • , σ i , • • • σ n ) ∈ IOT races(Λ).
We check whether such durations exist by considering them as n variables d 1 , • • • , d n (of type D); we construct constraints on these variables characterising the properties of observable traces. By definition, only the occurrence of an internal input might break the property. There are two reasons for allowing an initialised observable multitrace to be extended by an internal input. The first is that a sufficient number of corresponding internal outputs have previously been emitted. The second is that at the time when the extension is performed, the trace emitting the corresponding internal output is no longer observed. If σ i is the trace extended by internal input a, ρ = σ i .a and σ j is the trace at the interface that sends a, the first case correspond to situation in which pref (σ j , a, |ρ| a ) exists and C: d i +dur(ρ) > d j +dur occ(σ j , a, |ρ| a ) holds. The latter case corresponds to situations in which pref (σ j , a, |ρ| a ) does not exist and C : d i + dur(ρ) > d j + dur(σ j ) holds. However, by definition of dur occ, when pref (σ j , a, |ρ| a ) does not exist we have that dur occ(σ j , a, |ρ| a ) = dur(σ j ), which means that the constraints C and C are equivalent. Therefore both cases can be treated in the same way by requiring that C holds, as is done in Algorithm 1. Every new constraint to be considered is added to the set E (line 10). Sat is a function on sets of constraints such that Sat(E) returns T rue if all constraints in E are simultaneously satisfiable and F alse otherwise.

Experiments

We implemented the approach by separating the verification of local traces (Section 4.1) and the verification of the tuple of traces against the definition of observable multi-traces (Definition 6 and Section 4.2). If there are n subsystems, the global verdict V erdict g has n + 1 verdicts (V erdict 1 , . . . , V erdict n , V erdict com ) where for l in [1 . . . n], V erdict l is the local verdict in {P ass l , F ail l , Inconc l } associated to the lth component and where V erdict com ∈ {P ass com , F ail com } is the verdict relating to the verification of the communication policy.

In order to assess the scalability of the framework, we adopted a mutationbased approach. We first generated multi-traces that are correct by construction with respect to local analyses and communication rules. For this purpose, a global model of the system is built by simulating internal communications using one timed queue per component. Since the reception of a message can be delayed, the model specifies asynchronous communications. Then, we use the symbolic execution platform Diversity9 to build long traces, focusing on the behaviours that complete communication scenarios as much as possible. Finally, the resulting multi-traces are directly constructed by considering a tuple made of all projections for each component. Generated multi-traces are then modified by applying some simple mutation schemas. Table 1 summaries mutation schemas we applied on a multi-trace µ to produce a set of mutated tuples of traces.

Mut. schema Description #1 Choose (randomly) a position in µ and insert an event ev #2

Choose randomly an event ev in µ and delete it #3

Choose randomly an event ev in µ and modify its data #4

Choose randomly an event ev in µ and modify its duration #5

Choose randomly a round-trip-commnunication (RTC) in µ and break it.

Table 1: Mutation schemas on multi-traces Mutation schemas #1 and #3 require that added or modified events respect syntactic requirements from the system signature and concerning channels and data types. Mutation schema #5 is designed to break the key property of multi-traces, that is that time is necessarily elapsing when messages are transmitted. Let us illustrate with the observable multi-trace µ = (σ 1 , σ 2 ) where

σ 1 = ( , c 1 ?v 1 ).(1, c 2 !v 2 ).(3, c 3 ?v 3 ) and σ 2 = ( , c 2 ?v 2 ).(1, c 3 !v 3
). Applying mutation schema #5 consists of breaking the so-called round-trip communication, abbreviated as the acronym RTC,

c 2 !v 2 → c 2 ?v 2 → c 3 !v 3 → c 3 ?v 3 ,
for which by construction, the delay between the emission and the reception on the first component has to be strictly greater than the delay between the reception and the emission on the second component. Mutation schema #5 modifies delays between these actions so that there is an internal reception occurring before its corresponding emission is sent. A possible mutation of µ using mutation schema #5 could be µ = (σ 1 , σ 2 ) with σ 1 = ( , c 1 ?v 1 ).(1, c 2 !v 2 ).(1, c 3 ?v 3 ) and σ 2 = ( , c 2 ?v 2 ).(2, c 3 !v 3 ). While the first 4 mutation schemas do not necessarily create faulty multi-traces, mutation schema #5 creates by construction at least a communication fault.

The size of the PhoneX system depends on the number of clients. We consider a system with 3 caller clients, 3 called clients, 3 active sessions and a PhoneX central. In Table 2, the third column (com. checking) give the time10 needed to solve the constraint associated to the verification of communications described in a multi-trace whose number of events is given in the first column and number of internal communications is given in the second column. The fourth column provides the time11 needed to analyse all local traces. For each multi-trace, we generate 1000 mutated tuples of traces and we count the ratio of multi-traces that are faulty with regards to communication policy (before last column). Finally, in the last column, we give the average time to check the communication constraint of the mutated tuples. Experiments have been performed on a 3.10Ghz Intel Xeon E5-2687W working station with 64 GB of RAM on Linux Ubuntu 14.04. Table 2: Experimental data for correct multitraces and their mutants Among classical solvers, we get best results with the Yices SMT solver [START_REF] Dutertre | Yices 2.2[END_REF]. The efficiency of Yices for solving constraints of the form d i + x > d j + y where x and y are concrete durations together with the fact that constructing the set of constraints from a tuple is linear explains that communication checking is more efficient than unit testing. Unit testing of subsystems is performed by the extension to unitary testing of the symbolic execution platform Diversity which is coupled with several solvers such as Yices, CVC4 or Z3. Regarding symbolic models without timed issues, functionalities (test case generation driven by test purposes, verdict computation) offered by the Diversity test extension are similar to those provided by the tool STG [START_REF] Clarke | STG : a symbolic test generation tool[END_REF].

Related work

Testing timed distributed systems from models gives rise to several recent works. In [START_REF] Nguyen | A framework for distributed testing of timed composite systems[END_REF], hypotheses are broadly the same as those adopted in this paper, namely a model for each local component, and a testing architecture constituted of independent local testers. [START_REF] Nguyen | A framework for distributed testing of timed composite systems[END_REF] mainly focuses on the generation of test cases from a global model built by composing local models and queues, similar to the one that we used in Section 5. The main difference is that the correction of the system can boil down to the local correction of each component, without any verification of internal communications. In [START_REF] Krichen | A formal framework for black-box conformance testing of distributed real-time systems[END_REF], testing of distributed real-time systems is based on the conformance relation tioco and considers timed automata as models. Testers can be local or global so that the testing architecture does not necessarily reflect the one of the system. The authors focus on the construction of analogue-clock and digital-clock test cases. The question of communications is supported by a compositionality result saying that correctness up to tioco is preserved by parallel composition of timed automata provided that they are input-enabled. Similarly, in [START_REF] Vain | Automatic distribution of local testers for testing distributed systems[END_REF], local testers that can exchange synchronisation messages are derived from a global timed automaton. Thus, all these works are rather interested in the issue of test case generation, assuming testing hypotheses on communications between components, while we leave aside this question to focus on the analysis of traces with almost no hypotheses on internal communications. Lastly, the use of constraint solvers is often advocated when dealing with software and system testing issues [START_REF] Gotlieb | Constraint-based testing: An emerging trend in software testing[END_REF]. As an example of usage for the verdict computation in MBT, [START_REF] Jourdan | Using a SAT solver to generate checking sequences[END_REF] uses SAT solvers for generating checking sequences from finite state machines.

Conclusion

We focus on the oracle problem for testing distributed systems against specifications. A system execution is a tuple of timed local traces, one for each location. An observation is correct iff each local trace is allowed by the corresponding specification component and the tuple of local traces defines a valid communication scenario. The oracle problem is reduced to several instances of the standard oracle problem for centralised testing plus a constraint satisfaction problem for communication. This is implemented as an orchestration coordinating several centralised verdict computations using the Diversity tool and calls to classical constraint solvers. We have carried out experiments with a central telecommunication system which have shown low computation time. Our algorithm is designed for active testing in which we run a test and then check the observation made. It would be interesting to extend it to deal with passive testing.

  a) with d ∈ D + , else delay(ev) = 0 (ev = ( , a)). In the sequel δEvt(C) denotes {ev ∈ Evt(C)\act(ev) = δ}. Definition 2 (Timed traces). The set IT races(C) of initialised traces over C is 5 (IEvt(C) \ δEvt(C)) * .(ε + δEvt(C)). The set U T races(C) of uninitialised traces over C is {u(σ) | σ ∈ IT races(C)} where u(σ) denotes ε if σ = ε and ( , a).σ if σ = (d, a).σ . The set T T races(C) of timed traces over C is U T races(C) ∪ IT races(C).

Definition 5 (

 5 Multi-traces). The set of multi-traces of Λ with initial instants, denoted IM T races(Λ), is the subset of IT races(C 1 ) × • • • × IT races(C n ) defined as follows: -Empty multi-trace: (ε, • • • , ε) ∈ IM T races(Λ), -multi-trace Extension: for any µ = (σ 1 , . . . , σ n ) ∈ IM T races(Λ), for ev ∈ IEvt(C i ) for i ≤ n, (σ 1 , . . . , σ i .ev, . . . , σ n ) ∈ IM T races(Λ) provided that: if act(ev) ∈ I(C i ) ∩ I int (Λ), we have |σ j | ev ≥ |σ i | act(ev) + 1 and dur occ(σ j , ev, |σ i | act(ev) + 1) < dur(σ i .ev) with j = Sender(Λ, act(ev)).

Fig. 2 Fig. 1 :Fig. 2 :

 212 Fig. 1: Interaction scenario of a successful call operation

Algorithm 1 : 2 E 4 ρ ← ε ; 5 foreach ev ∈ σi do 6 ρ 8 a

 124568 ObsM ult(µ, d, Λ)Data: µ = (σ1, • • • , σn) tuple of traces, d = (d1, • • • , dn) n variables, Λ system signature Result: a verdict stating whether or not µ is an observable multi-trace 1 begin ← ∅;3 for i ∈ [1 • • • n] do ← ρ.ev ; 7 if act(ev) ∈ I(C int (Λ)) then ← act(ev);

9 j← 10 E

 910 Sender(Λ, act(ev)); ← E ∪ {(di + dur(ρ) > dj + dur occ(σj , a, |ρ|a)}; 11 if ¬Sat(E) then 12 return F ailcom /* It's not an observable multi-trace */; 13 return P asscom;

  depicts a scenario of a successful session setup and call establishment between 2 phones. A caller with P hone 112 initiates a call (doCall(113)) to the user of P hone 113 . The PhoneX server, after receiving Calling(112, 113), checks if P hone 113 is registered, available, and then starts StartSession(112, 113) for communication management and remains available. Session 113 112 informs P hone 113 that P hone 112 tried to get in contact (CalledBy(112)). The user of P hone 113 can accept the call (doAcceptCall) and informs Session 113 112 using AcceptingCall which can establish communication (multicasting InitCall). Each user can end the call (the user of P hone 112 hangs up, doEndCall) and report it (EndingCall) to Session 113 112 that closes the connection by multicasting T ermCall and becomes available (EndSession(112, 113)) again.

  (a)). PhoneX central behaviour (Fig 4(a)). At the Idle state, PhoneX may receive a call and reach Calling or get notified of the ending of an already Fig.3: TIOSTSs G src and G dest of Caller and Called clients active session and return to Idle. At Calling, PhoneX may start a new session (src, dest) and return to Idle provided that dest is a registered and allowed-tocall number in the Client database and there is no active session with called client dest. Otherwise, PhoneX may also return to Idle when dest is not registered in Client database, or calling dest is not allowed, or called client dest is busy. Session behaviour (depicted in Fig 4(b)). When a new session is started, a Session TIOSTS is instantiated. At the Idle state, Session receives src and dest numbers, it then reaches Starting. It notifies dest with a call operation emitted by src and reaches Initiating. At Initiating, it may reach either Accepted when called client accepts the call during a waiting delay or T erminating if a noanswer is observed during a waiting delay or the call get rejected. At Accepted, active session initiates a call between src and dest and reaches state Established. Then, either caller or called client may end the call (session reaches T erminating state). At T erminating state session sends a terminating signal to both caller and called clients and reaches Ending. Finally, it returns to Idle by notifying PhoneX central of ending the active session.

				Caller TIOTS
													Called TIOTS
					Idle						Idle
	doCall ?	dest						Error ?	msg Code	CalledBy ?	src	TermCall	?
					Starting					Initiating
				! Calling	(	src	,	dest	)			doAcceptCa	ll	?	do	Re jectCall	?
	TermCall	?									Accepting
	TermCall	?		Initiating					TermCall	?	AcceptingC	! all
							InitCall	?		Accepted	Rejecting
				Established				InitCall	?
	? TermCall TermCall	?				doEndCall	?	NoAnswer	?	TermCall	?	doEndCall Established	?	Re	! l jectingCal
				UserEndingCall				UserEndingCall
							! EndingCall	TermCall	?	! EndingCall
				Terminating				Terminating
					(a)							(b)

E * is the set of finite sequences of elements in E with ε as neutral element for sequence concatenation.

https://projects.eclipse.org/proposals/eclipse-formal-modeling-project

Due to the lack of space.

In accordance with the tioco conformance relation

https://projects.eclipse.org/proposals/eclipse-formal-modeling-project

using the Yices SMT solver[START_REF] Dutertre | Yices 2.2[END_REF].

using the CVC4 solver[START_REF] Barrett | Cvc4[END_REF] embedded in the Diversity platform.