Home

The Fastest 1.3.6 User's Guide

1. might be useful to check whether values satisfy predicates or not Now let s see an example involving the optional parameter constant_declarations Say asctiTbl defined in figure 15 is used in some operation Then Fastest needs that the user sets a value for it so the tool can find abstract test cases for all the test classes generated for the opera tion In the same axiomatic definition have been defined some CHAR s but say the user wants to test the operation with a more realistic ASCII table Hence the user can issue a command like this one setaxdef ident charO chari char2 CHAR O Nmapsto null 1 Nmapsto char0 2 Nmapsto chari 3 Nmapsto char2 4 mapsto tab 5 mapsto space We will further subdivide this category to solve some issues automatically in future releases 34 In other words constant declarations allows the user to declare some constants of basic types that are used to define the constant value to be bound to the identifier Internally Fastest declare these identifiers in axiomatic definitions Although the user can chose any names in the declaration there are two things worth to mention 1 Avoid name clashes with other identifiers declared in axiomatic definitions and operations 2 Chose names that increase the likeness of Fastest finding abstract test cases by following the rules described in section 7 10 1 If constants of different types need to be declared the syntax is the same than
2. Integers n lt m m gt n n m m n n m m2 iln Type Subtype n gt m mn lt n xo Y XoY X o Y X gt Y seq Y Sets ANB BNA X Y X gt Y X gt Y seq Y AUB BUA Z Z N All types t y y 1 b Subtyping rules TAY yAHz a Equivalence rules Figure 16 Fastest applies by default these equivalence and subtyping rules Hdom R m m N R eval N gt 0 This sentence evaluates the parameter and if it is true and all of the other conjuncts of the theorem are found in the test class then the test class is pruned If the Boolean expression evaluates to false the test class is not pruned Equivalence Rules Fastest applies equivalence rules taken from the library to the elimination theorems whenever possible Besides it applies by default the rules listed in Table 16a This implies for instance that the engineer does not need to write the following theorem Elimination Theorem NotInEmptyDom Silly 1 X R X Y x dom R dom R because the library already contains the following one Elimination Theorem NotInEmptyDom x X R X Y x dom R R 4 and the equivalence rule R dom R Equivalence rules are lists of atomic predicates which should be equivalent to each other To add delete or modify equivalence rules edit the file INSTALLDIR 1ib conf rwRules tex with any text editor Subtyping Rules Fastest also applies some simple subtyping rules when it substitutes the formal parame
3. dom smaz smax s lt r KeepMazReading SP_1 smax SENSOR Z s SENSOR r Z s dom smaz Smart s lt r smar s lt 0 r lt 0 KeepMaxReading_SP_2 smart SENSOR Z s SENSOR r t Z s E dom smaz Smart s lt r smar s lt 0 r 0 KeepMaxReading_SP_3 smax SENSOR Z s SENSOR r Z s E dom smaz Smart s lt r smaz s lt 0 r gt 0 49 KeepMazReading SP 4 smat SENSOR Z s SENSOR Pos s dom smaz smat s lt r smar s 0 r gt 0 KeepMazReading_SP_5 smat SENSOR gt Z s SENSOR r Z s dom smaz smat s lt r smat s oO r gt 0 KeepMazReading DNF 2 smat SENSOR Z s SENSOR r Z s dom smar KeepMazReading_SP_6 smar SENSOR Z s SENSOR r Z s dom smaz smat s 0 PT U KeepMaxReading_SP_7 smat SENSOR Z s SENSOR r Z s Z dom smaz smat s 0 r 0 KeepMazReading SP 8 smax SENSOR Z s SENSOR r Z s dom smar smat s lt 0 r gt 0 KeepMazReading SP 12 smaz SENSOR Z s SENSOR r Z KeepMazReading SP 9 s dom smax r lt smar s smax s lt 0 r 0 smaz SENSOR Z s SENSOR r Z s dom smaz smaz s U r gt 0 KeepMazReading SP 13 smax SENSOR Z s SENS
4. In this case then the user can work directly with Aj Case A We suggest to write A as follows As EABAC where E is Decl Pred and then to derive test cases for B C and E and not for As If Decl Pred is not named Fastest will not recognize it as an operation thus making it impossible for the user to work with it Integration testing is not implemented yet 18 x is intended to be a natural number but N is not a type then we need an invari Naturals ant An equivalent schema would have been z Z Naturals z Z but the invariant would be hidden NaturalsInv Naturals Naturals x Z 0 lt z jag Decr Decr A Naturals A Naturals z gt 0 q g 1 Ea p 1 No proof is needed to verify that Decr preserves the state invariant because state variables are Theorem DecrVerifiesInvariant restricted to satisfy it NaturalsInv A Decr gt NaturalsInv a Classic style b Proof obligation style Figure 11 A simple example showing two styles of writing state invariants Fastest works better with the proof obligation style Case Ag As with the previous case we suggest to rewrite Ag as follows D ch Pred Ag EABAC where Decl might be different from Decl since it may be necessary to add some variables because E does not include B and C which may add some declarations If the operation is written in this way then derive test c
5. before modifying the library For a more academic presentation of the pruning method implemented by Fastest read CAR10 ATEX Elimination theorems are written in ETEX using the CZT package Theorem names Each elimination theorem must have a unique name Formal parameters Each elimination theorem has a set of formal parameters The parameters can be any Z legal declaration of variables plus the reserved word const before a parameter name If a parameter is preceded by const it means that Fastest will replace it only by constants of the corresponding type const applies only to parameters of type Z N or any enumerated type i e free types without recursion When an elimination theorem contains two or more constant parameters they are replaced only by different literals For instance the library contains the following elimination theorem Elimination Theorem ExcludedMiddleEq z const y const z X T Y T Z Fastest will call this elimination theorem always with y 4 z for example ExcludedMiddleEq n 11 34 but never something like ExcludedMiddleEq n 34 34 nor ExcludedMiddleEq n count 3 The parameters of an elimination theorem are formal in the sense that Fastest will try to replace them with the actual types of the terms appearing in the predicate of a test class Hence by using adequate parameters the theorem will serve to prune a lot of test classes See the paragraphs Rewrite rules Subtyping substitutions and Syntact
6. rangle where variable is the name of a numeric variable appearing in the operation and each element in the list must be separated by a comma and in increasing order The list must be non empty If the type of the variable is N Fastest checks that all the numbers in the list are naturals Important In this version Fastest will accept lists of numbers in any order but the behaviour of the tactic will be unpredictable 7 5 8 Mandatory Test Set Fastest s name MTS With this tactic the user can bind a set of constants v Un to an expression expr in such a way that when the tactic is applied it generates n 1 test classes characterized by the following predicates expr v for all in 1 n and expr u Un The command to apply this tactic is as follows addtactic op_name MTS expr set_extension where expr is an expression appearing in the operation and set_extension is a set extension written in TEX mark up whose members are constants Fastest checks whether the types of expr and set_extension are consistent In this version the constants in set_extension can be numbers elements of enumerated types identifiers declared in axiomatic definitions or constants assembled out of them for instance 2 gt ON where ON is an element of an enumerated type 7 5 9 Weak Existential Quantifier Fastest s name WEQ This tactic can be applied only when the precondition of the operation has one or more existential quan
7. 4 FIL Fie CL DEAD Pls Ce De LF tt ES SETEN GO Abas TA CBI T Standard partition for expressions of the form z A A 0 AAG Standard partition for expressions of the form z A A a Az iz teA Standard partition for expressions of the form A FA 0 A 1 A 1 51 C 2 Integers Standard partition for expressions of the form n lt m A lt 0 B lt 0 A lt 0 B 0 A lt 0 B gt 0 A 0 B gt 0 A gt 0 B gt 0 Standard partition for expressions of the form n lt m A lt 0 B lt 0 A lt B A lt 0 B lt 0 A B8B A lt 0 B 0 A lt 0 B gt 0 A 0 B 0 A 0 B gt 0 A gt 0 B gt 0 A lt B A gt 0 B gt 0 A4A B Standard partition for expressions of the form n gt m A lt 0 B lt 0 A lt U D Az 0 6 A gt 0 B 0 A gt 0 B gt 0 Standard partition for expressions of the form n gt m AO0 B 0 ASB A lt 0 B lt 0 A B8B A 0 B lt 0 A B 0 A gt 0 B lt 0 A gt 0 B 0 A gt 0 B gt 0 4 gt B ABI 4 8 Standard partition for expressions of the form n m A lt 0 B lt 0 A 0 8 0 A gt 0 B gt 0 Standard partition for expressions of the form n 4 m n lt 0 m lt 0 n lt 0 m 0 n lt 0 m gt 0 n 0 m lt 0 n 0 m gt 0 n gt 0 m lt 0 n gt 0 m 0 n gt 0 m gt 0 92 Standard partition for expressions of the form n m n lt O m lt O0 n lt m n lt 0 m lt 0 n m n lt 0 m lt 0 n gt m n lt 0m 0 n lt 0m gt 0 n 0 m lt 0 n 0 m 0 n 0 m gt 0 n gt 0 m gt 0 n lt m n gt 0 m gt 00 mm n gt 0 m gt 0 n gt m C 3 Relations Standard pa
8. 6 KeepMaxReading SP 7 P 8 9 T 2 3 4 KeepMaxReading SP E KeepMaxReading SP KeepMaxReading DNF 2 KeepMaxReading_SP_10 L KeepMaxReading DNF 83 KeepMaxReading NR 1 KeepMaxReading DNF 3 L KeepMaxReading NR 2 KeepMaxReading SP 11 L KeepMaxReading NR 3 KeepMaxReading SP 12 KeepMaxReading NR 4 KeepMaxReading SP 13 L KeepMaxReading NR 5 KeepMaxReading SP 14 KeepMaxReading_SP_15 genalltt addtactic KeepMaxReading_DNF_1 SP lt smax s lt r addtactic KeepMaxReading SP lt smax s lt r addtactic KeepMaxReading_DNF_3 NR r langle 10 1000 rangle genalltt genalltt c Applying DNF and SP to the entire testing d Applying DNF and then two different tactics to two different tree test classes Figure 14 In each figure we show the testing tree produced with the script shown below them scripts include only the relevant commands 28 where operator is the IX string of a Z operator and expression is a Z expression written in Tex It is assumed that operator appears in the expression and this in turn appears in the predicate of the selected operation Hence this tactic can be applied to different operators and different expressions of the same operation The application of the tactic divides each test class at a given level of the testing tree in as many test classes as conjunctions defines the partition Each conjunction is conjoined to the predicate of the test class being partitioned to form a new test
9. For instance consider the compound operations sketched in Figure 10 Let s assume in all cases that B C and D are primitive operations Besides say that fA1 fA2 fA3 fA4 fA5 fA6 fB fC and fD are the subroutines implementing the corresponding operations Then we suggest to work as follows in each case Cases A and A These cases are very easy to deal with Just derive test cases for B and C and not for A and A5 The point here as with some of the other cases is that the correctness of either fA1 or fA2 depends solely on the correctness of both fB and fC Then one should derive unit test cases for fB and fC only and then integrate them to test fA1 and fA2 Since Fastest now is only good for unit testing then trying to apply it to derive test cases for A and A might not be the best option Case A3 We have distinguished this case from the previous one because we want to emphasize that we think that B and D are two distinct operations and not two schemas of the same operation like the normal case and an erroneous one If this is the case then we think that the best course of action is to work as indicated in the previous paragraph Case A4 B and C do not have precondition since all of their variables are primed Hence their predicates will not have much influence in abstract test case derivation since test cases are generated from the input space of the operation For this reason Fastest will not unfold these schema references
10. If it finds that part of a test class matches on of the elimination theorems then it prunes that test class from the tree remember that the predicate of a test class is a conjunction of atomic predicates so if one or more of them are contradictory then the class is inconsistent Hence the more elimination theorems in the library the more test classes will be pruned by prunett without user intervention We suggest that users should add elimination theorems to the library every time Fastest fails in pruning an empty test class instead of pruning it manually due to two reasons 1 More test classes could be pruned automatically in the current or future projects and 36 2 It enables the chances to formally prove that the elimination theorem is actually a contradiction As the reader can see when executing prunett it displays either the name and parameters of the elimination theorem by means of which the test class was pruned or it says that Fastest cannot prune the test class which as we have seen does not mean that the test class cannot be pruned at all The library of elimination theorems is the text files INSTALLDIR 1ib conf elimTheorems tex and INSTALLDIR 1ib conf rwRules tex The user can add delete and modify elimination theorems by editing the first file with any text editor The syntax of the elimination theorems is rather easy an can be learned by reading the library here we just give some tips Please read all them carefully
11. The user can see the identifiers for which Fastest automatically bound a constant value by running command showaxdefvalues 7 6 3 Equalities If an identifier ident T where T is any type is declared in an axiomatic definition and there is exactly one equality of the form ident expr where expr is not a constant expression then 33 users should bind a value for each identifier in expr for which Fastest does not automatically bind a constant value and at the same time they cannot bind a value to ident Once this is done Fastest automatically reduces expr to a constant value which is bound to ident If this is not done then Fastest will not be able to find abstract test cases for all test classes For example users need to manually bind a value to audit in Figure 15 but they cannot bind a value to adm The user can bind values to identifiers with command setaxdef 7 6 5 7 6 4 All Other Declarations Identifiers declared in axiomatic definitions that do not meet the conditions described in the previous sections fall in this category For these identifiers the user should give constant values so Fastest has chances to find abstract test cases for all the test classes The user can bind values to identifiers with command setaxdef 7 6 5 7 6 5 Command setaxdef Fastest provides command setaxdef to bind values to identifiers declared in axiomatic definitions provided they can be bind at all Command syntax is as follows
12. VISo by following the edges from child to parent and let vi Ty Un Tn be n constant values satisfying Pi A A Pm Then an abstract test case of Co is the Z schema box defined by Cop ti v1 A A fn 0 4 Fastest Architecture in a Nutshell e Fastest architecture was guided by Performance because calculating thousands of test cases can be very time consuming Modificability because we don t know yet what features industry could need Documentability because to test must mean to document e Hence we combined two different architectural styles and we used open formats and tools in our interfaces Client Server so we distribute test case calculation Implicit Invocation so we can add modify and remove components as new and more sophisticated requirements arise Latex is used to read specifications and to generate testing trees test classes abstract test cases etc Fastest has been integrated with the Community Z Tools project CZT to avoid duplicate efforts in programming core modules e Fastest process structure is shown in Figure 5 Clients interact with the user and generate and prune testing trees All of the other functions are performed on the servers The knowledge base server stores testing tactics abstract test cases refinement functions etc so testers can use them for re testing within a given project and for testing in different projects Currently
13. Z schema box defined by zi Ti En Tal 3 1 2 Valid Input Space Let Op be a Z operation Let pre Op be the precondition of Op The Valid Input Space VIS of Op written VISop is the Z schema box defined by ISop pre Op 3 1 3 Test Class Informally test classes are sets of abstract test cases defined by comprehension hence each test class is identified by a predicate Test classes are also called test objectives ULOG test templates SC96 test targets and test specifications Let Op be a Z operation and let P be any predicate depending on one or more of the variables defined in V So Then the Z schema box VISo P is a test class of Op Note that this schema is equivalent to So pre Op A P This observation can be generalized by saying that if Co is a test class of Op then the Z schema box defined by Co P is also a test class of Op According to this definition the VIS is also a test class If Cop is a test class of Op then the predicate P in Co Cop P is said to be the characteristic predicate of Co or Co is characterized by P 3 1 4 Testing Tactic In the context of the TTF a testing tactic is a means of partitioning any test class of any operation However some of the testing tactics used in practice actually do not always generate a partition in the mathematical sense of some test classes For instance two testing tactics originally proposed for the TTF are the following e Disjunctive Norm
14. are operation schemas then showloadedops will print something like Q WUB However the user should select only A as an operation to be tested since B and C will be considered when DNF is applied Operation selection is explained in section 7 4 showtatics prints a brief description of all the available testing tactics A deeper explanation of them can be fund in section 7 5 and its subsections The remaining show commands display and save the specification testing trees test classes abstract test cases and values bound to identifiers declared in axiomatic definitions In any case command options must be entered in the order they are documented Some commands feature the o option that redirects the output to a file This is the only way so far to save the results generated by Fastest The output of most of these commands is BIFX mark up The following table summarizes these commands Command Description Options showaxdefs Displays the axiomatic definitions o lt file_name gt redirects the present in the specification in ETEX output to a file mark up showaxdefvalues Displays the values bound either au o file name Same as before tomatically or manually to identifiers declared in axiomatic definitions 45 Command Description Options showsch Displays a given schema it can be ei ther any of the specification schema test classes or abstract test cases TEX mark
15. basic and enumerated types and N and Z as follows e The default sets for basic types contain constants automatically generated by Fastest If the identifier of a basic type is XYZ then the constants for that type will be ryz0 ruz l ryz2 and all the identifiers of that type declared in axiomatic definitions Fastest assumes that all these values are distinct from each other For example if the specification declares type NAME and assuming there are no identifiers of this type declared in axiomatic definitions then the default finite set for it will be name0 namel name2 where it is assumed that name0 namel and name2 are declared in some axiomatic definition and since they have different names they are all distinct from each other e The default sets for enumerated types are the types themselves e The default sets for N and Z depend on the predicate being evaluated If some specific numbers appear in the predicate then the finite sets will contain all of them and the minimum minus one and the maximum plus one For instance if a predicate references 0 and 42 then the finite set for N will be 0 42 43 since 1 N then it cannot be included in the set and 1 0 42 43 for Z If there are no such constants then the sets are 0 1 2 and 1 0 1 for N and Z respectively e The finite sets for structured types like functions relations power sets etc are generated from the finite sets considered for the more basic t
16. be run by an operating system initialization script executing the same command The port number where each server will listen for connections is declared in the configu ration file 1ib conf server port conf by simply writing the number Note that this number and the port number declared in the clients must coincide Fastest s default configuration is to run a client and a sever in the same computer This is highly advisable since the client will be idle most of the time during a testing campaign In the default configuration client and server communicates through port 5001 while the IP address of the server must be 127 0 0 1 7 4 Loading a Specification and Selecting Schemas An specification is loaded by executing loadspec followed by a file name The full path to the file must be written if it is not located in the directory from which Fastest was started as in the following example Fastest gt loadspec doc sensors simp tex It is assumed that the file is a text file containing the full specification the current version does not support the BTFX directive input If the specification contains syntactic or type errors it will not be loaded and the errors will be informed It is possible to load only one specification at a time To load a new specification run the loadspec command again or reset the current session by running command reset in either case all the data generated so far will be lost It is possible to load specifications whe
17. before or after running genalltca but always after running genalltt Define finite models for KeepMaxReading_SP_1 and KeepMazxReading SP 5 as follows setfinitemodel KeepMaxReading_SP_1 fm num negate 1 negate 2 setfinitemodel KeepMaxReading_SP_5 fm num 1 upto 2 e Now run genalltca again so Fastest can find abstract test cases for those leaves for which there is no test case already e By running showtt you can see that there are test cases for all leaves e To see the abstract test cases run showsch tca Note that each abstract test case is a Z schema in which each state and input variable equals a constant value KeepMazReading_SP_1_TCASE KeepMaxReading_SP_1 r 1 smax sensor0 2 s sensor0 15 KeepMaxReading_SP_2_TCASE KeepMazxReading DNF 2 TCASE KeepMazReading_SP_2 KeepMaxzReading_DNF 7 r 0 r2 0 smax sensor0 1 smar s sensor0 s sensor0 KeepMaxReading_SP_3_ TCASE KeepMaxReading_SP_3 KeepMazxReading_SP_11_TCASE KeepMaxkReading_SP_11 r 1 smax sensor0 1 r 1 s sensor0 smar sensor0 1 s sensorO KeepMaxReading_SP_4_TCASE KeepMaxReading_SP_4 KeepMazxReading_SP_15_ TCASE Pwen i smax sensor0 0 KeepMazReading_SP_15 s sensor0 peT smar sensor0 1 KeepMazReading SP_5 TCASE s sensor KeepMaxReading_SP_5 pi 2 smax s
18. discretion Fastest provides commands prunefrom and prunebelow to erase a sub tree from some testing tree and command unprune to restore previously erased sub trees Their syntax and semantics are as follows e prunefrom class_name This command deletes the sub tree hanging from and including class name It is useful to erase leaves e prunebelow class name This command deletes the sub tree hanging from but not including class_name e unprune class name This command restores the sub tree hanging from and including class name Note that it is impossible to restore a sub tree hanging from a pruned test class It is important to remark that pruning test classes from a testing tree manually can reduce the quality of testing This happens when the tester prunes one or more classes that are not empty and thus Fastest will not generate abstract test cases for them 40 7 8 Generating Abstract Test Cases genalltca distributes evenly the task of finding abstract test cases for test classes across all the registered testing servers 7 3 Then the more testing servers the less the time needed to complete this task Important This process might take some hours The tool will remain useless until the whole process terminates If the process is interrupted it will have to be restarted from the very begining In that case all the abstract test cases generated so far will be lost This command can be run only after genalltt but it can be run a
19. e Oper modifies only x Including StateA EStateB makes a a A b hP redundant StateB Figure 12 State variables are grouped in state schemas Operations include A of the full state and of those part of the state that they do not modify IS Then the more variables in the IS the longer the abstract test cases Furthermore if some of the IS variables are not referenced in the operation s predicate then it means that these variables are irrelevant for the operation But they still need to be included in abstract test cases Hence it is possible that abstract test cases contain many variables such that only a fraction of them are meaningful to the tester It does not matter whether this irrelevant variables appear in predicates such us var var there still be an equality like var const in every abstract test case of the corresponding operation For instance it is a common style to divide the state variables in some state schemas that then are joined to define the whole state space of the system as shown in 12 In this way specifiers avoid to write many equalities for those variables that the operation does not modify However a better strategy if the specification is going to be loaded into Fastest would be to specify Oper as follows Oper AStateA m M P m x 1 Ay y Clearly this is possible only because Oper s predicate depends only on the state variables declared in StateA In the extreme case Oper ca
20. of sensors The Z formal specification for the function mentioned above is depicted in Figure 6 We did not write the state invariant in this example in order to simplify the presentation To run Fastest open a command window move to the directory where you installed Fastest and execute the following command java Xss8M Xms512m Xmx512m jar fastest jar Assuming the specification is stored in a file called sensors simp tex and if this file is stored in the doc directory under Fastest s root directory load the specification with loadspec doc sensors simp tex Generating the Testing Tree Before generating a testing tree you need to select one or more operations to test In our example we select KeepMazxReading selop KeepMaxReading The testing tree depends on the tactics you apply and the order they are applied In this case we will apply two testing tactics 2We assume the reader is familiar with the Z formal notation 3In this section we just give an overview of how to use Fastest Section 7 is a thorough user manual 11 SENSOR KeepMarReadingE2 MazxReadings MazReadings smax SENSOR Z s SENSOR r Z ted KeepMazxReading Ok e z po na A MazReadings s SENSOR r Z s dom SMAL KeepMazxReading smar s lt m KeepMazReadingOk smar smart s m r V KeepMazReadingE1 V KeepMazxReadingE2 KeepMazReadingEl EMazxReadings s SENSOR s Z dom
21. oracle The process is very automatic if we have the model The current version of Fastest only implements the generation phase of Figure Fastest is more suitable for unit testing The MBT methodology implemented by Fastest called Test Template Framework see next section uses Z formal specifications f Model comprobation generation comprobation Abstract Abstract test cases outputs test tase output refinament abstraction Concrete Program Concrete test cases outputs Figure 1 Model based testing methodology general view 3 The Test Template Framework Fastest implements the Test Template Framework TTF TTF is a MBT framework proposed by Phil Stocks and David Carrington in SC96 and Sto93 Although the TTF was meant to be notation independent the original presentation was made using the Z formal notation It is one of the few MBT frameworks approaching unit testing The TTF deals with the generation phase shown in Figure 1 In this framework each operation within the specification is analysed to derive or generate abstract test cases This analysis consists of the following steps roughly depicted in Figure 2 1 Define the input space IS of each operation 2 Derive the valid input space VIS from the IS of each operation 3 Apply one or more testing tactics starting from each VIS to build a testing tree for each operation Testing trees are populated with nodes called test classes 4 Prune each of th
22. smaz Figure 6 lt A Z specification of an operation that keeps the maximum values read from a set of sensors Disjunctive Normal Form DNF It s applied by default Standard Partitions SP We will apply it to the expression smaz s lt r present in schema KeepMazReadingOk Then you only need to issue one command to apply the last tactic addtactic KeepMaxReading SP lt smax s lt r e Once you have added all the tactics you want the testing tree is generated with genalltt e The resulting testing tree is the one shown in Figure 7 It can be printed with showtt e Each node in the testing tree i e a test class is also a Z schema describing the conditions for selecting a test case The content of those Z schema can be displayed with the following command showsch tcl You can take a look at these test classes in Appendix B 12 KeepMaxReading VIS 5 4 L KeepMaxReading DNF 1 KeepMaxReading SP 1 KeepMaxReading_SP_2 KeepMaxReading_SP_3 KeepMaxReading SP_4 KeepMaxReading_SP_5 KeepMaxReading DNF_2 KeepMaxReading_SP_6 KeepMaxReading_SP_7 KeepMaxReading SP_8 KeepMaxReading_SP_9 KeepMaxReading_SP_10 L KeepMaxReading DNF_3 KeepMaxReading_SP_11 KeepMaxReading SP_12 KeepMaxReading SP_13 KeepMaxReading_SP_14 KeepMaxReading_SP_15 Figure 7 Testing tree for KeepMarReading Pruning the Testing Tree It is important to prune from the testing tree
23. ta a lann e A Oe a eo da men ak Z Features Unsupported by Fastest B Test Classes Generated for KeepMaxkReading C Standard Partitions DISCS vwati Bete eBags Deore We eck ne wade Ble ee Ra een a eet hE Gl ok a arabe es E Re OCCT ey A td ce Da ae de Ta TR ee ee tae BF aes Bo ae e G32 RE A tons g di Bole as Dew SO le SO oe Ad be Se e he Eo tee Be e Elimination Theorems 48 49 51 51 52 53 55 1 What s New on This Version e Command loadelimtheorems has been added e In elimination theorems set extensions can be better expressed through the directive Nse e The general pruning algorithm was slightly changed see section 7 7 1 e The elimination theorem library delivered with this version is included in Appendix D e This version partially supports axiomatic definitions see section 7 6 e Commands setaxdef showaxdef and showaxdefvalues have been added e Limited support for four new testing tactics have been added Numeric Ranges NR Manda tory Test Set MTS Weak Existential Quantifier WEQ and Strong Existential Quantifier SEQ see sections 7 5 7 7 5 8 7 5 9 and 7 5 10 respectively e Testing tactics ISE PSSE and SSE have been fixed to support expressions at the left of C or C and not only variables e Section 6 was added to document some tips on how to write Z models more suitable to be loaded on Fastest e Appendix A lists some Z features still unsupported by Fastest e A configura
24. the bound variables The command to add this tactic is as follows addtactic Op_name WEQ quantification bindings P q g where quantification is the quantified predicate as appears in the operation and bindings is a comma separated sequence of bindings Each binding must have the following form var type set_extension where var is one of the quantified variables type is the type of one of the quantified variables and set extension is a set extension written in BTEX mark up whose members are constants Fastest checks that all the quantified variables are bound directly through their names or indirectly through their types to a set extension and that the types of the set extensions are consistent with respect to the quantified variables For instance the command corresponding to the example shown above is addtactic SomOp WEQ Nexists x Anat y seq num x gt w land y neq langle rangle implies head y gt x x N 4 6 y langle 4 rangle In this version the constants in any set_extension can be numbers elements of enumerated types identifiers declared in axiomatic definitions or constants assembled out of them for instance 29 ON where ON is an element of an enumerated type Important Fastest will not be able to automatically derive abstract test cases from test classes whose characteristic predicates include quantifications This tactic and SEQ help to reduce this limitation besides providing a s
25. the library these modifications will not have any effect until the library is loaded again To do this execute command loadelimtheorens 7 7 4 Semiautomatic Pruning Fastest provides two commands that can be used to prune empty test classes interactively e searchtheorems class_name searches the library for elimination theorems that might be used to prune test class class_name e apply theorem_name class_name parameter parameter applies the elimination theorem named theorem_name to the test class class_name to see if it is possible to prune the test class with that elimination theorem The user has to provide a list of parameters enclosed between double quotes If the list does not match either the number or the types of the formal pa rameters of the elimination theorem then the test class will not be pruned If the parameters provided by the user can be passed to the elimination theorem and the test class contains all the atomic predicates of it then the test class is pruned All the equivalence and subtyping rules are applied as with prunett For instance the following commands prune test classes SCAddCat_SP_1 and SCAddCat_SP_5 shown at the beginning of the section apply SingletonIsNotEmpty SCAddCat_SP_1 c apply NotSubsetOfSingleton SCAddCat_SP_5 categs c 7 7 5 Manual Pruning Test classes can be pruned not only because they are empty but also because they will not give meaningful test cases This is at the engineer
26. the second message shown above is printed This might be an indication that Fastest could have found an abstract test case for the test class if MAX EVAL would have been larger 7 10 Defining Finite Models Finding an abstract test case for a given test class means to find a vector of constants that when substituted by the free variables in the predicate they satisfy it This is an undecidable problem as the elimination of inconsistent test classes Hence Fastest may fail in finding an abstract test case due to three reasons 1 The test class is an empty set prunett failed because the problem it tries to solve is unde cidable too 2 Fastest is not smart enough to find one 3 The search space is so large that Fastest aborted before exhausting it If the test class is empty then proceed as indicated in section 7 7 1 If the test class is not empty then keep reading this section Fastest calculates abstract test cases by generating a finite model for each leaf test class This finite model is the Cartesian product between one finite set for each variable appearing in the VIS of the corresponding testing tree Clearly the bigger the finite model the more chances to find an abstract test case but the more time it will take Fastest automatically selects a finite model for each test class according to some heuristics The experiments we have run so far show that the default strategy applied by Fastest discovers in average 90 of th
27. 0 byte0 where represents 1021 elements e x byte0 A mem byte0 byte0 where represents 1022 elements e x byte0 A mem byte0 byte0 where represents 1023 elements It is very important to remark that although we have used to represent elements in each sequence in the real abstract test cases the elements must be written down Precisely the difficulty in writing down those test cases is the reason for which we suggest avoiding arbitrary numeric constants Fastest will automatically find the first two abstract test cases but it will need user assistance in order to find the remaining three However if the model is slightly rewritten Fastest will automatically derive all the abstract test cases but one and likely the implementation will be verified as thouroghusly as with the other model The only change is to avoid the constant by rewriting the axiomatic definition as follows memsSize N U lt memSize Then the user can derive the same test classes and later he or she binds a smaller constant to memSize 3 is an optimal choice In this way Fastest will automatically find the following test cases e x byte0 A mem byte0 e x byte0 A mem e x byte0 A mem byte0 byte0 e x byte0 A mem byte0 byte0 byte0 and the user will have to assist the tool to find the remaining one e x byte0 A mem byte0 byte0 byte0 byte0 If the implementation can
28. A e anything Elimination Theorem SetComprNotASeq4 s seq X n N n 0 s dom s domi 1 anything e i n 1 anything Elimination Theorem SetComprNotASeq5 s seq X n N n 0 s dom i 1 anything i n 1 gt anything C dom s Elimination Theorem NatRangeNotEmpty n const N const M N eval N lt M n N n M Elimination Theorem ExcludedMiddle z const y const z X T Y T Z Elimination Theorem NotinSetExtension z const y X x E setExtension y Cay Elimination Theorem SetComprisEmpty1 R X Y R anything dom R e anything 4 Elimination Theorem CapSubsetEmpty A B P X AFI ANB ACB Elimination Theorem CapEqEmpty 4 B P X 58 AF i ANB A B Elimination Theorem CapEmpty A B P X A AnB Elimination Theorem NatRangeNotEmpty2 const N const M N eval N lt M N M Elimination Theorem NatRangeNotEmpty3 n m const N const M N n mxN n ma M x N Elimination Theorem NatRangeNotSubset n m const N const M const P const Q N eval M N gt Q P N M Cn mxP n m Q P Elimination Theorem NatRangeNotEq n m const N const M const P const Q N eval M N gt Q P N M n mxP n m Q P Elimination Theorem NatRangeNotEmpty5 n m const P const Q N eval Q x P gt 0 n mx P n m Q P Elimination Theorem NatRangeNotEmpty4 n m N n n m E
29. AILED message might correspond to an empty test class that Fastest could not prune in this case the user should proceed as suggested in section 7 7 1 If the test class is not empty the the user should proceed as indicated in section 7 10 7 9 Controlling the Generation of Abstract Test Cases There are two configuration variables defined in the file INSTALLDIR lib conf fastest conf that can be used to fine tune the test case generation algorithm MAX_EVAL This is the maximum number of attempts to find one abstract test case for each test class that the algorithm will perform The larger this value the higher the chances to find an abstract test case for each test class but the longer it will take 41 DEE SIZE FINITE SET This is the maximum number of elements that will populate the finite sets bound to the most elemental types and variables As before the larger this value the higher the chances to find an abstract test case for each test class but the longer it will take A small increment in this value might produce a really huge model where abstract test cases are sought However MAX EVAL will limit the number of elements in this model that are tried out in order to find an abstract test case Every time these values are changed Fastest must be restarted Fastest is delivered with the best values according to our experience When the finite model for a given test class is inspected up to MAX EVAL elements but it has more then
30. Is Not Fully Supported saith Oe A E 6 2 Fastest Conforms to the Z ISO Standard Livia a a 6 3 Fastest Is Meant to be Used for Unit Testing 6 4 Be Careful in Testing Compound Operations o aoo a a a a 6 5 Do Not Include the State Invariant in the State Schema 6 6 Keep the State Schema Focused on a Set of Related Operations 6 7 Avoid Using Quantifiers A aa a 6 8 Replace Schema Types with Functions ooa a a a 00 eee eee ees 6 9 Avoid Axiomatic Definitions is ds ea a 6 10 Avoid Arbitrary Numeric Constants ell n TAL aA User s Manual 7 1 Installing and Executing Fastest ooa aaa a ee non 7 1 1 Running Fastest and Entering Commands 7 2 Steps of a Testing Campaign ai e hk a koe ee dl dg del da BR AAA HRA 7 3 Installing and Declaring Testing Servers 0002004 7 4 Loading a Specification and Selecting Schemas 7 5 Applying Testing Tactics and Generating Testing Trees Tal Disminctive Normal Porm n 4 YA se f AT aie Be ee 7 5 2 Standard Partition Fastest s name SP www aa aegis On do BA AAS Loe Free Type Fastest s name FT we kak A Be en see ge 7 5 4 In Set Extension Fastest s name ISE 7 5 5 Proper Subset of Set Extension Fastest s name PSSE 7 5 6 Subset of Set Extension Fastest s name SSE 7 5 7 Numeric Ranges Fastest
31. OR r Z KeepMaxReading_SP_10 smar SENSOR Z s SENSOR r Z s dom smar smat s gt 0 r gt 0 s dom smaz r lt smar s smar s lt 0 r gt 0 KeepMaxReading_DNF_3 smaz SENSOR Z s SENSOR r Z s dom smaz r lt smar s KeepMazReading SP 11 smax SENSOR Z s SENSOR r Z s dom smaz r lt smar s smaz s lt 0 r lt 0 KeepMaxReading_SP_14 smar SENSOR Z s SENSOR r Z s E dom smaz r lt smar s smar s 0 r gt 0 KeepMaxReading_SP_15 smaz SENSOR Z s SENSOR r Z s dom smaz r lt smar s smat s gt Q r gt 0 C Standard Partitions The following standard partitions are included by default in the file 1ib conf stdpartition spf The user can erase or modify these partitions and define new ones as well by simply editing the file Fastest needs to be restarted so it is notified of changes C 1 Sets Standard partition for expressions of the form SU T S T DHA ay SA T SAU TAGSAT SAL tl Fiabe CL SI Pale ies SAU TAG TH S SAIL TAIL EOL LR C T TE 8 T S Standard partition for expressions of the form SN T salpe Eres L A SA T 1 SATAN SAT O a Pate SL DEAL Fale Cs SAA eit 28 SALIA ON PA SET PES TAS Standard partition for expressions of the form SA T SERLE SIERO SA T SAU TAB SAT
32. SP_4 KeepMaxReading SP_5 KeepMaxReading DNF 2 L KeepMaxReading DNF_3 KeepMaxReading_SP_11 KeepMaxReading SP 15 Figure 8 Testing tree for KeepMarReading after running prunett prunefrom c prunes the sub tree starting at class c prunebelow c prunes the sub tree starting at class c including c itself unprune c restores class c See more about these commands in section 7 7 1 Finding Abstract Test Cases Now it is time to try to find one abstract test case in each leaf of the testing tree Fastest accomplishes this by generating a finite model over which it evaluates each leaf s pred icate If some element of the finite model satisfies a test class predicate then we have found an abstract test case in that class If no element in the finite model satisfies the predicate it can happen because The predicate is a contradiction or the test class is empty This can happen because Fastest is not smart enough to prune all the empty test classes although it can become smarter if the user teaches it see section 7 7 1 The finite model is not a appropriate The predicate is not a contradiction so there are other finite models that can satisfy it By running genalltca Fastest will try to find a test case for each leaf in the testing tree by applying default finite models After some time Fastest finds test cases for almost all the leaves as shown in Figure 9 this tree is displayed with sh
33. Set extensions se takes a Z UX string enclosed in brackets and separated by one blank from each bracket The string is intended to be an element of a set extension For instance the library contains the following elimination theorem Elimination Theorem SingletonNotSet A PX x X EA setExtension 1 A If se expr is found in an elimination theorem Fastest will try to match expr against any of the elements of a set extension present in the test class being processed expr cannot contain commas instead mapsto must be used If the members of the set extension present in the test class are set comprehensions se will not be useful i e the expression will not match against the set comprehensions Then if a test class contains any of the following conjuncts it will be pruned by SingletonNotSet Z mem xj mem 3g AUB 1 2 3 AUB R b gt 4 co 26 b 4ER but Fastest will fail in pruning a test class including the following conjuncts although it is a contra diction 1 3 AUB 1 3 2 17 AUB Evaluations eval takes a constant Boolean expression as a parameter separated by one blank from each bracket A constant Boolean expression is a Boolean expression referencing parameters preceded by const Z literals Z operators and the literals of enumerated types The following elimination theorem uses it Elimination Theorem DomsSizelsZero R X Y const N m N 38
34. The Fastest 1 3 6 User s Guide Automating Software Testing Maximiliano Cristi mcristia flowgate net Pablo Rodriguez Monetti Pablo Albertengo prodriguez flowgate net palbertengo flowgate net CIFASIS gen XL CONSULTING UNR UPCAM Flowgate Consulting Maip 778 Piso 1 Oficina 10 2000 Rosario Argentina Release date November 2010 Contents What s New on This Version Introduction to Model Based Testing The Test Template Framework ST Ey Concepts hues ew go kat tou A d re San SE ge G AZIL ABB Space ae ten ara sd e il aos Ri layo af AB ayo de ed Ba Z BAZ Vald an Spaces de T k kayo H ao tan te 2 k ede os ank ASYE ty dim eee AAS S Mesh Clase ks so a koni fin See fi aa ia OB dee E kep SE GAY A A y Bolte A ee a IAE Bie a8 i Re Use bit eg de de ghettos d vee e Ete eee lt 8 Dold Festina X a ent an to ae Bee at gh ee age ye ke ee eee a n o et ee es Cc wuld Pruning Testing Trees xls lila e fada d S dio lan ab SA TA AAS dap TA dh TR Aa 3 1 7 Abstract Lest Case erd vini yy da ie A peg Sete den teed Adee ALS Fastest Architecture in a Nutshell An Example 5 1 TheModel AZEpecifiCatioh e ese ee e are nn 5 2 Running Fastest and Loading the Specification 5 3 Generating the Testing Tree e ro ve kaa ee ano 5 4 Pruning the Testing Tree 5 5 Finding Abstract Test Cases xl da tan aa a a Tips on Writing Z Models for Fastest 6 1 The Z Notation
35. act test cases 7 8 9 If some leaves do not have an abstract test case then explore these leaves to determine the cause for that There are two possible causes e The leaf predicate is a contradiction but Fastest failed in pruning it In this case a Improve the elimination theorem library with as many elimination theorems as nec essary to prune all the contradicting leaves 7 7 2 b Reload the elimination theorem library c Prune the trees again 7 7 1 d Check whether all of the contradicting leaves have been pruned If not check the elimination theorems that were added and go to step 9a e The leaf predicate is not a contradiction but Fastest was not smart enough to find an abstract test case for it In this case a Help Fastest to generate finite models to find abstract test cases for these complex test classes 7 10 b Go to step 8 10 If all of the leaves have an abstract test case then save the results 7 11 and leave the program 7 19 Step 4 is perhaps the most relevant step of all since it will determine how revealing and leafy testing trees are going to be Along the same lines step 7 is highly recommended since it will severely reduce the time of most testing campaigns Steps 4 and 5 can be executed iteratively and in the specified order or the opposite one Test case design includes from step 2 to step 5 The remaining steps generate test data i e abstract test cases The following se
36. al Form DNF By applying this tactic the operation is written in Disjunctive Normal Form and the test class is divided in as many test classes as terms are in the resulting operation s predicate The predicate added to each new test class is the precondition of one of the terms in the operation s predicate e Standard Partitions SP This tactic uses a predefined partition of some mathematical operator Sto93 For example the partition shown in Figure 3 is a good partition for expressions of the form SAT where is one of U N and Cr ee Eee aa SY REM RO TC ONT Mey Let etre eee P P ETRE E TR a e yen T ka a eth P P O E NAE REEE EEE reir PAPEN Pi TET P a PLA P E A sd E E PA PI Figure 4 The predicate of a test class at some level is the conjunction of the predicate of its parent test class and its own predicate As can be noticed standard partitions might be changed according to how much testing the engineer wants to perform 3 1 5 Testing Tree The application of a testing tactic to the VIS generates some test classes If some of these test classes are further partitioned by applying one or more testing tactics a new set of test classes is obtained This process can continue by applying testing tactics to the test classes generated so far Evidently the result of this process can be drawn as a tree with the VIS as the root node the test classes generated by the first testing tactic as its children and so on In other wor
37. ases for B C and E and not for Ag as we suggested in the previous cases 6 5 Do Not Include the State Invariant in the State Schema It is the classic style within the Z community to include the state invariant inside the state schema as shows the simple example of Figure 11a However Fastest works better if the state invariant is not included in the state schema as shown in Figure 11b This is the style followed by specification languages such as B Abr96 and TLA Lamo02 Writing the state invariant outside the state schema makes it a proof obligation rather than a state restriction At the same time this style avoids implicit preconditions perhaps making the specification clearer to programmers because they do not need to calculate them But explicit preconditions are the key to input domain partition which is the fundamental concept behind the TTF Hence by writing the state invariant outside the state schema we avoid implicit preconditions thus enabling input domain partition 6 6 Keep the State Schema Focused on a Set of Related Operations As we have seen the input space IS of a Z operation is defined as the schema declaring all the input and state variables of the operation An abstract test case is an element belonging to the 19 StateA Oper RE AState y Y EStateB m M StateB P m 2 2 a A y y b B P m a x is a predicate depending only on m State x and z i
38. be configured to think that the available memory is 3 bytes then it is very likely that these test cases will uncover the same errors than the original ones and perhaps in less time It is important to remark that this will work if the implementation is configured and not modified In other words it will work if there is some symbolic constant that can be modified without changing a single line of code or if this value is returned by some external function 22 7 User s Manual Throughout of this manual remember that Fastest is still a prototype Then it is not as robust as it should be For an academic presentation of Fastest see CR09 and CAR10 7 1 Installing and Executing Fastest Fastest should work on any environment with Java SE Runtime Environment 1 6 or newer However it has been tested only on Linux and MS Windows boxes To install the tool just decompress and unarchive the file Fastest tar gz in any folder of your choice Fastest can run in one of two modes we call them application mode and distributed mode Roughly speaking in application mode all the processing is performed in the local computer while in dis tributed mode some tasks can be distributed across so called testing server In this section we explain how to run Fastest in application mode section 7 3 explains how to run it as a distributed system It should be noted that although application mode is the easiest way to use Fastest and it provides the same fun
39. c sub_tree tactic_name parameters where sub_tree is the name of either a selected schema or the name of a test class already generated tactic_name is the name of a tactic supported by Fastest and parameters is a list of parameters that depends on the tactic If sub_tree is the name of a schema the tactic is applied to all the existing leaves of the corresponding testing tree If sub_tree is the name of an existing test class the tactic is applied to all the leaves of the sub tree whose root node is that test class The examples shown in Figure 14 may clarify this behaviour Unless addtactic prints an error message the tactic has been successfully added This com mand produces no other effect than adding the tactic to an internal list until command genalltt is executed Command showtactics prints a brief description of the available tactics the following sections describe them in more detail 7 5 1 Disjunctive Normal Form This tactic is applied by default and it must not be selected with addtactic By applying this tactic the operation is written in Disjunctive Normal Form and the VIS is divided in as many test classes as terms are in the resulting operation s predicate The characteristic predicate of each class is the precondition of one of the terms in the operation s predicate 7 5 2 Standard Partition Fastest s name SP This tactic uses a predefined partition of some mathematical operator see Standard domains for Z operat
40. class 7 5 3 Free Type Fastest s name FT This tactic generates as many test classes as elements a free type enumerated has In other words if a model defines type COLOUR red blue green and some operation uses c of type COLOUR then by applying this tactic each test class will by divided into three new test classes one in which c equals red the other in which c equals blue and the third where c equals green The tactic is applied with the following command addtactic op_name FT variable where variable is the name of a variable whose type is a free type Currently Free Type works only if the free type is actually an enumerated type i e an inductive type defined only by constants 7 5 4 In Set Extension Fastest s name ISE It applies to operations including predicates of the form expr fexpri exprn In this case it generates n test classes such that expr expr for i in 1 n are their characteristic predicates The command to add this tactic is as follows addtactic op_name ISE predicate where predicate is an atomic predicate of the form shown above 7 5 5 Proper Subset of Set Extension Fastest s name PSSE This tactic uses the same concept of ISE but applied to set inclusions PSSE helps to test op erations including predicates like expr C fezpri ezpraj When PSSE is applied it generates 2 1 test classes whose characteristic predicates are expr A with 1 1 2 1 and A Plezpr
41. ctionality than in distributed mode Fastest achieves all of its efficiency in distributed mode 7 1 1 Running Fastest and Entering Commands To run Fastest in application mode open a command window and run one of the following commands where INSTALLDIR is the full path to the directory where Fastest was installed java jar INSTALLDIR fastest jar java Xss8M Xms512m Xmx512m jar INSTALLDIR fastest jar The first command will serve for most purposes but if large specifications will be used then the second command is a better option If the computer has at least 1 Gb of memory then the second option should be used The Xms and Xmx options indicate the minimum and maximum amounts of memory that the Java process will be able to use respectively Then if more memory is needed increase the maximum it must be a multiple of 1024 In this version of Fastest it is difficult to know if more memory is needed but one symptom is command genalltt section taking too long more than one minute to finish In either case Fastest prints the following prompt from which users can issue commands Fastest gt To enter a command just type in it along with its arguments and then press the return key There are three ways of learning which commands are available e Type help and press the return key e Press the TAB key and a list of commands will be printed e Type in the first letters of a command and then press the TAB key either a list of th
42. ctions explain in detail each of the steps of a testing campaign carried on with Fastest 7 3 Installing and Declaring Testing Servers We have mentioned earlier that Fastest by definition is a distributed system making it possible to parallelize testing tree pruning and the calculation of abstract test cases between all the available servers Hence a typical Fastest facility would consist of some clients used by test engineers to conduct the testing and many servers used by those clients to prune testing trees and calculate abstract test cases it is important to remark that servers need not to be powerful computers in fact we think of them being custom workstations which are usually underutilized If test engineers use Fastest wisely then they can take advantage of the servers during idle hours optimizing the computing power of the organization In this version testing servers need to be declared in each computer running a client The configuration file named lib conf cserversinfo conf is a text file that stores the list of available testing servers for that particular client The syntax is as follows name address port 25 where name is a descriptive name for the server it has no use in this version address is the IP address of the server and port is the port number at which the server is listening to On the other hand each server has to be started either manually with the command java jar fastest server jar or it can
43. ds test classes predicates obey the relationship depicted in Figure 4 A consequence of this relationship is that the deeper the tree the more accurate and discovering the test cases As was noted by Stocks and Carrington in SC96 the Z notation can be used to build the tree as follows Vis 15 P O VIS Pi E V C Cy Pi Cy ar an P 3 Gi VIS P C3 a C3 E 3 G T 1 G CP P C3 n Ci P 7 3 1 6 Pruning Testing Trees In general a test class predicate is a conjunction of two or more predicates It is likely then that some test classes are empty because their predicates are contradictions These test classes must be pruned from the testing tree because they represent impossible combinations of input values i e no abstract test case can be derived out of them In this way pruning the initial testing tree saves CPU time because it avoids searching abstract test cases in empty sets 3 1 7 Abstract Test Case An abstract test case is an element belonging to a test class The TTF prescribes that abstract test cases should be derived only from the leaves of the testing tree Abstract test cases can also be written as Z schema boxes Let Op be some operation let VISo be the VIS of Op let x Ti n Tn be all the variables declared in VISop let Cop be a leaf test class of the testing tree associated to Op let Pi Pm be the characteristic predicates of each test class from Co up to
44. e abstract test cases of non empty test classes for moderated size specifications In complex models however the computing time needed to hit these percentages use to be quite high and can even be higher if testing trees are not properly pruned Furthermore in some cases the size of the default finite models grows exponentially reaching thousands of millions of elements This could make Fastest to take years to find one abstract test case if the test class does not happen to be empty Hence an efficient and effective pruning method is as important as giving the user the chance to help Fastest to select the most promising and smallest finite model Fastest allows the user to define a finite model at the test class level in other words a different finite model for each test class can be defined If the user do not take any explicit action Fastest generates a default finite model that we believe is the best option in most situations Important The user defined strategy should be used only as an exception the default strategy works well in most models The user defined strategy should be used only when a test class predicate has many variables or some variables of complex types such as higher order partial functions relations between three or more sets partial functions whose domain is a Cartesian product and so on 42 7 10 1 Default Finite Models Finite models are constructed recursively from specific finite sets selected for all
45. e commands whose name starts with those letters will be printed or the complete command name if any will be printed For instance if after entering the a key the TAB key is pressed the following is printed TAB means pressing the TAB key 23 Fastest gt a TAB addtactic apply Fastest gt a And if the d key is pressed followed by the TAB key again the result is the whole addtactic command printed as follows Fastest gt ad TAB dtactic When the TAB key is pressed after command loadspec Fastest prints the contents of the working directory For example if Fastest is run from the installation directory the result is as follows Fastest gt loadspec TAB doc fastest server jar fastest jar lib Fastest gt showsch If the user types in the first letters of one these files or directories and then presses the TAB key again the name will be completed or a filtered list will be displayed as with command names If the letters correspond to a file name and it is completed a blank space is added at the end but if the letters correspond to a directory when the name is completed a or X character is added at the end If the user presses the TAB key again the content of this directory is displayed The TAB key can be further pressed as a means of exploring the contents of the inner directories The left and right arrow keys can be used to move the cursor along the line being edited to modify it by inserting or deleting any character T
46. e following categories treating each of them in a different way as is described below 7 6 1 Basic Types An identifier ident T where T is a basic type declared in an axiomatic definition is considered a constant For example null tab space and root in Figure 15 are considered to be constants of their respective types These constants are used when Fastest calculates abstract test cases 7 8 The user does not need to take any action for these identifiers 7 6 2 Symbolic Constants A identifier ident T where T can be any type but a basic one declared in an axiomatic definition is a symbolic constant if there is exactly one equality of the form ident cexpr where cexpr is a constant expression A constant expression is any valid expression verifying any of the following e The expression is a number or an element of an enumerated type e The expression includes only symbolic constants numbers elements of enumerated or basic types and Z symbols For example in Figure 15 Min Max and blank are symbolic constants Mid is not a symbolic constant because there is no equality defining a constant value for it and adm is not a symbolic constant neither because audit U root is not a constant expression Fastest automatically reduces any constant expression to its equivalent constant value thus bind ing the corresponding symbolic constant to this value In other words the user does not need to take any action for these identifiers
47. e resulting testing trees 5 Find one or more abstract test cases from each leaf in each testing tree Model VIS laelic _ Pruned constants Abstract test tree selection test cases tactic 1 pruning First level of test Test tree classes T tactic 2 Last level of test classes Second level of test classes tactic n tactic 3 Figure 2 The Test Template Framework process is a detailed view of the generation phase shown in Figure 1 One of the main advantages of the TTF is that all of these concepts are expressed in the same notation of the specification i e the Z notation Hence the engineer has to know only one notation to perform the analysis down to the generation of abstract test cases The concepts introduced above are explained in the next section How Fastest implements the TTF is explained by means of an example in Section 5 Stocks and Carrington use the term testing strategies in SC96 kiwo So Te a 5 SAD TEAD SCT 2 S T 6 SS T TCS 3 SAB T 7 SAB TAB T 8 T TABA SO bo TAO SOT Am ET FE B S ATF Figure 3 Standard partition for SUT SN Ty SAT 3 1 TTF Key Concepts In this section the main concepts defined by the T TF are described 3 1 1 Input Space Let Op be a Z operation Let 2 z be all the input and non primed state variables declared in Op or in its included schemas and T Ta their corresponding types The Input Space IS of Op written So is the
48. earing in the VIS of the test class and set_extension is one of a upto b This form can be used only for N and Z It restricts the finite set for the type or variable to the set a b where a and b must be constant values A set extension written in BTEX mark up whose members are constants It restricts the finite set for the indicated variable or type to the elements listed in the set extension Note that if for instance type is N NAME then each element belonging to the set extension must be a constant partial function of type N NAME written in IATEX mark up For instance the following is a possible value for this case 0 mapsto nameO 1 Nmapsto namel 2 Nmapsto name2 O Nmapsto name0 1 Nmapsto name0 2 mapsto nameO Note that the constants for type NAME i e name0 namel and name2 are consistent with the constants automatically generated by Fastest for the same type However this is not mandatory and the user can chose any names as long as they combined with those automatically generated by Fastest satisfy the predicate of the test class Given Seeds This form can be used only for N and Z but not for variables of those types In this case nsize will not be considered If this option is used the finite set for N or Z will be the set defined as follows Given If this option is chosen then Fastest will search for constants of type Z or N present in the test class depending on the indicated va
49. easily understood it will probably be implemented by one programmer The Z specification of such a design should then has one state schema per module and one operation schema for each subroutine exported by each module These are the primitive operations If you do not have a design or if you do not want to define one before understanding the requirements then at least write the specification as a set of primitive operations that are progressively integrated to provide some complex services In either case use Fastest to derive test cases for these primitive operations Note that full specifications can be given for these primitive operations In other words give schemas for both successful and erroneous conditions for each operation but keep them primitive 17 A BAC A Decl Pred AB A C A D U A3 BVD AC Ag As B Decl C Pred gt B Decl Pred gt Ge Pred Figure 10 Some compound operations Decl is a declaration and Pred and Pred are a predicates B C and D are primitive operations 6 4 Be Careful in Testing Compound Operations Although it is a matter of style specifiers might want to represent that some operation calls or uses the services of other operations This is some times achieved by specifying an operation as the conjunction A or the composition 3 of some other operations In particular conjunction can be written as schema inclusion We call these compound operations
50. ensor0 1 s sensor0 e This test cases as well as the testing tree and test classes can be saved to disk in TX format with the following commands showtt tcl o filename saves the testing tree showtt o filename saves the test classes showsch tca o filename saves the abstract test cases 16 6 Tips on Writing Z Models for Fastest Z is a very general language that can be used for several purposes and specifications can be written in a variety of styles Although Fastest can work with any kind of Z specifications provided they are written with the subset of Z currently supported Appendix A it works better if specifications follow some specific rules described in the following sections Important Working differently as we suggest might lead to performance penalties or even to Fastest being unable to derive abstract test cases If the specification or some of its operations are very complex then Fastest could crash when these operations have to be processed However if complex operations are treated correctly Fastest might provide very useful information regarding test case design and even abstract test cases 6 1 The Z Notation Is Not Fully Supported Before writing a Z specification for Fastest please read Appendix A to learn what parts of the Z notation are still unsupported by the tool The support for these features is being postponed since we consider that they are somewhat superfluous for Fastes
51. eristic predicates include quantifications This tactic and WEQ help to reduce this limitation besides providing a sound tool to increase the accuracy of testing at the presence of quantifications Important This tactic tends to produce more test classes for which Fastest would be unable to automatically find abstract test cases than WEQ 7 6 Dealing with Axiomatic Definitions According to the TTF and to the semantics of the Z notation identifiers declared in axiomatic defi nitions neither are state variables nor input variables However since they do appear in operations they are carried all the way down to test classes Hence when abstract test cases have to be derived from test classes it is necessary to bind a value for each identifier declared in an axiomatic definition because otherwise there is no way to find a tuple of values satisfying the test class predicate in this sense Fastest treats all these identifiers as model parameters Precisely if only test case design is needed then this step can be skipped 32 CHAR USER control blank P CHAR null tab space CHAR Maz Mid Min Z root USER adm audit P USER ascii Tbl N CHAR null control control N blank 4 Y Min 34 Maz 1000 Min blank tab space root adm adm audit U root Figure 15 Examples of identifiers declared in an axiomatic definition Fastest classifies identifiers declared in axiomatic definitions in th
52. f schema types are indeed needed there is a chance to replace them with functions as shown in Figure 13 6 9 Avoid Axiomatic Definitions Fastest supports axiomatic definitions as described in Section 7 6 However their presence decreases the level of automation of the tool so it is better to avoid them as much as possible Conceptually axiomatic definitions are parameters of the specification In other words the meaning of an speci fication depends on the particular value assumed for each axiomatic definition Since test cases are derived from the specification they are also parametrized by its axiomatic definitions Therefore the user first needs to set a constant value for each axiomatic definition and then Fastest derives test cases considering those values In this way the application is tested for only one of its possible meanings 6 10 Avoid Arbitrary Numeric Constants If memSize stands for the amount of available memory of some computer and the specification includes an axiomatic definition such as memSize N memSize 1024 and an operation like WriteMemOk A MemoryState x BYTE mem lt memSize mem mem x then possible test classes cases may be e mem 21 e mem 1 e mem memSize 1 e mem memSize e mem memsize 1 and possible corresponding abstract test cases may be e x bytel A mem e x byte0 A mem byte0 e x byte0 A mem byte
53. genalltt These steps can be repeated as many times as needed They can also be interleaved with any command to prune testing trees 7 7 what is highly advisable It is also possible to run these steps 26 even before genalltt is run to apply DNF in which case Fastest first applies DNF and then the tactics added by the user DNF is applied only once the first time genalltt is run Testing trees can be displayed with showtt 7 11 Important If genalltt takes more than a couple of minutes to finish it might be the case that the Java process run out of memory It usually happens when the DNF of an operation has thousands of disjuncts this in turn occurs when the operation is too complex considering full schema unfolding If this occurs the program will look like tiltt we hope to solve this in future versions The only thing the user can do is to kill the process from the operating system This problem might be solved by augmenting the memory available for the Java process 7 1 The command addtactic adds a testing tactic to the list of tactics to be applied to a particular previously selected operation Tactics are applied in the order they are entered by the user Initially the list of tactics of any operation includes only DNF which is the first to be applied The command syntax is rather complex because it depends on the tactic that is going to be applied see the following sections for more details The base syntax is addtacti
54. he up and down arrow keys move across the commands that have been issued during the session If one of these commands is recovered the user can modify it by using the left and right arrow keys and can run it again by pressing the return key Commands are executed when the return key is pressed regardless of where the cursor is Important Note that Ctrl C kills the program making all the data and commands to be lost Future versions will be more robust Important Fastest does not save anything by default The user has to use one of the commands described in section 7 11 to save the data generated during a session 7 2 Steps of a Testing Campaign Roughly speaking currently a typical testing campaign carried on with Fastest can be decomposed in the steps listed below Some of them are optional and some can be executed in a different order as is described in the referred sections between brackets Also at any time users can run commands to explore the specification and the testing trees and to save their results 7 11 1 Install and declare more testing servers i e run Fastest in distributed mode 7 3 2 Load the specification 7 4 3 Select the operations to be tested 7 4 Select a list of testing tactics to be applied to each operation 7 5 24 5 Generate testing trees one for each selected operation 6 Set a value for each axiomatic definition 7 6 5 7 Prune the trees 7 7 1 8 Calculate abstr
55. heorem SingletonNotSubsetDom R X Y 4 X y Y x Z dom R dom setExtension z gt y C dom R Elimination Theorem NrresEmptyRel R X 4 Y A PY x X x E dom R gt A R 56 Elimination Theorem NrresCap R X Y A PY a X z dom R amp A setExtension z N dom R Elimination Theorem CardDomEmptyRel R X Y const N n N eval N gt 0 R n N dom R mn Elimination Theorem CardRelSingleton R X Y const N n N r X x Y eval N gt 1 n N dom R n r R Elimination Theorem SingletonMappletNotEqualRell R X 6 Y 1 X y Y x E dom R setExtension z y R Elimination Theorem SingletonNotSubsetRel R X 6 Y 2 X y Y x E dom R setExtension 7 H y C R Elimination Theorem NotInEmptyRan R X Y y Y y ran R R 4 Elimination Theorem SingletonMappletNotEqualRel2 R X 5 Y x X const yl const y2 Y yl ran R r y2 R Elimination Theorem BasicSetContradiction A P X A AF Elimination Theorem ExcludedMiddleSingleton A PX const z const y X r A y A Elimination Theorem ExcludedMiddleSingletonSubl A PX const x const y X 2 A setExtension y C A 57 Elimination Theorem ExcludedMiddleSingletonSub2 A PX const x const y X zr A ACU Elimination Theorem RanNotSubsetOfSingleton R X e Y y Y RAN ran R C y Elimination Theorem SetComprNotEmpty1 const N Z A PX eval N lt 2 A 1 anything N
56. his case Though enumerated types are fully supported e Schema types All of the concepts related to schema types are unsupported including the 9 operator Spec ifications containing schema types will be loaded and test case design will work mostly but automatic pruning and abstract test case search will not work as usual Section 6 8 might give some light on how to deal with this limitation e The Z sectioning system Z sections are not recognized by Fastest e Generic definitions and generic schemas This features are not supported although the user can perform test case design with specifi cations using them Fastest will work as usual for those operation schemas that do not use generics e Schema composition and piping Schemas defined by these operators will not be recognized as operations by Fastest thus making it impossible for the user to test them Section 6 4 might give some light on how to deal with this limitation 48 B Test Classes Generated for KeepMaxkReading The following schema boxes represent the test classes generated for the operation KeepMazxReading In the framework developed in Sto93 each test class is described as a Z schema This is important because only one notation is necessary to describe the specification and the test results KeepMaxkReading_VIS smart SENSOR Z s SENSOR r Z KeepMaxrReading_DNF_1 smat SENSOR Z s SENSOR r Z s
57. i expr A exzpr exprn ezpri expr is excluded from Pfexpr expr L because expr is a proper subset of ezpri expr The command syntax is as follows addtactic op_name PSSE predicate where predicate is an atomic predicate of the form shown above 7 5 6 Subset of Set Extension Fastest s name SSE It is similar to PSSE but it applies to predicates of the form expr C ezxpri expr in which case it generates 2 by considering also ezpri expr The command syntax is as follows addtactic op_name SSE predicate where predicate is an atomic predicate of the form shown above 29 7 5 7 Numeric Ranges Fastest s name NR With this tactic the user can bind an ordered list of numbers ni n to a numeric variable var in such a way that when the tactic is applied it generates 2 k 1 test classes characterized by the following predicates var lt n var ni ni lt var lt Nb var Ni Ni lt VAT lt Nizi VAN Nini VAN lt nj var ny and Ny lt var Consider the following example Variable appearing in operation memPointer N List provided by the user 0 65535 Ti gt memPointer lt 0 T memPointer 0 Test classes generated by the tactic T 0 lt memPointer A memPointer lt 65535 Ti gt memPointer 65535 Ts 65535 lt memPointer The command to apply this tactic is as follows addtactic op_name NR variable langle list of numbers
58. ic substitutions below for other mechanisms that enable the generalization of elimination theorems The body of theorems The predicate of an elimination theorem must be a conjunction of atomic predicates The conjunction must be written only one conjunct by line ending each line with Since the predicate is a conjunction the order of the conjuncts is unimportant An atomic predicate in an elimination theorem can be any legal Z atomic predicate using the standard symbols of Z supported by Fastest the names of the formal parameters and the reserved words sw anything se and eval explained below Somewhere sw takes a Z TEX string enclosed in brackets and separated by one blank from each bracket For instance the library contains the following elimination theorem Elimination Theorem BasicUndefinition f X Y x X x E dom f somewhere f z 37 Nsw string is equivalent to the regular expression string When prunett finds such a directive it tries to match the regular expression in any of the atomic predicates of a test class predicate Anything anything takes no parameters For example the following elimination theorem uses this directive Elimination Theorem SetExtNotASeq s seq X n N n 0 s dom s dom i 1 anything i n 1 anything anything is equivalent to the regular expression that matches any string Two or more occurrences of this directive can match different strings
59. in Z i e setaxdef ident charO chari char2 CHAR user0 user7 USER The user can see the values bound to identifiers by running command showaxdefvalues Besides Fastest provides command showaxdefs so users can easily see all the axiomatic definitions used in the specification setaxdef can be executed right after loadspec but perhaps the best moment to do it is after genalltt Fastest will not be able to find abstract test cases for those test classes where an identifier declared in an axiomatic definition is referenced and there is no constant value bound to it Therefore if abstract test cases are needed for all the test classes setaxdef must be executed before genalltca However both commands can be executed one after another iteratively until there is an abstract test cases for each test class 7 7 Pruning Testing Trees It is very common that many leaves in a testing tree are indeed empty classes because their predicates are contradictions Finding an abstract test case for a given test class implies finding a vector of constants verifying the predicate of the test class Hence if the predicate is a contradiction it will be impossible to find an abstract test case for it Fastest provides two strategies to prune empty test classes from testing trees The following sections describe each of them 7 7 1 Automatic Pruning Fastest provides command prunett which goes through all the testing trees and prunes as many empty test classes a
60. limination Theorem NatRangeNotSubset2 n const N const M const P N eval M N gt P N M c n n P Elimination Theorem NatRangeNotEq2 n const N const M const P N eval M N gt P N M n n P Elimination Theorem NatRangeNotSubset3 n m p const N const M const P const Q N eval M N gt Q P m lt n Q P N M Cp nxP p m Elimination Theorem NatRangeNotEg3 n m p const N const M const P const Q N eval M N gt Q P m lt n Q P N M p nxP p m 59 References Abr96 J R Abrial The B book Assigning Programs to Meanings Cambridge University Press New York NY USA 1996 CAR10 Maximiliano Cristi Pablo Albertengo and Pablo Rodriguez Monetti Ipruning testing trees in the test template framework by detecting mathematical contradictions In SEFM 2010 CRO9 Maximiliano Cristi and Pablo Rodriguez Monetti Implementing and applying the Stocks Carrington framework for model based testing In Karin Breitman and Ana Cavalcanti ed itors ICFEM volume 5885 of Lecture Notes in Computer Science pages 167 185 Springer 2009 Dil90 Antoni Diller Z An Introduction to Formal Methods John Wiley Press 1990 GJM91 Carlo Ghezzi Mehdi Jazayeri and Dino Mandrioli Fundamentals of sofware engineering Prentice Hall Upper Saddle River New Jersey 1991 HP95 Hans Martin Horcher and Jan Peleska Using Formal Specifications to Support Software Testing Software Quali
61. n be specified with but this implies that abstract test cases derived by Fastest will not mention y This might be a problem if the unit implementing Oper needs some initial value for all of its variables but perhaps that is an indication of some poor implementation 6 7 Avoid Using Quantifiers Quantifiers always complicate software verification Then it is a good advice to avoid them as much as possible regardless whether Fastest will be used or not wisely use the rich mathematical operators provided by Z to avoid many quantifications Fastest will enter into troubles if it needs to find abstract test cases from test classes whose predicates include quantifiers However it will succeed in many cases 6 8 Replace Schema Types with Functions Maybe the most important Z feature currently not supported by Fastest are schema types Schema types are normally used along with operation promotion Operation promotion talks about compound 20 Schema Type State gi X zr A X J X gt Y fA X R Y h X HX State dom z dom f should be added as state invari g A SchemaType ant 6 5 h X X a With schema types b With functions Figure 13 Replacing schema types with functions a represents the original specification and b represents the alternative without schema types operations 6 4 which in turn refers to integration testing and Fastest is meant to be used for unit testing 6 3 I
62. onSubl and NotinSetExtension Elimination Theorem NatDef n N A0 lt n Elimination Theorem Reflexivity z const y X LAY T Y Elimination Theorem ExtensionalUndefinition f X Y z X x Z dom f somewhere f x Elimination Theorem ArithmIneq const N N n m Z nom m N n N Elimination Theorem Arithmlneq2 const N N n m Z n m m N n gt N Elimination Theorem ArithmIneg3 const N N n m Z n m m N n gt N Elimination Theorem SingletonNotSet A PX x X EA setExtension 1 A Elimination Theorem BasicMembershipContradiction A P X x X EA EA Elimination Theorem NotInEmptySet A PX z X TEA A AJ 59 Elimination Theorem SingletonIsNotEmpty x X setExtension z Elimination Theorem NotSubsetOfSingleton A PX x X A Ac x Elimination Theorem NotSubsetOfSingletonMapplet R X e Y 7 X y Y RAY dom R C domfz gt y Elimination Theorem SingletonNotSubset A PX x X EA setExtension z C A Elimination Theorem DomNotSubsetOfSingleton R X Y z X R i dom R C x Elimination Theorem NotInEmptyDom R X Y x X T E dom R R 4 Elimination Theorem BasicOrderingProperty n m Z n m oan m ano m Elimination Theorem UndefinitionByEmptiness f X Y JE somewhere f anything Elimination Theorem SingletonMappletNotInDom R X Y T X y Y x Z dom R dom setExtension z gt y dom R Elimination T
63. ors at page 165 of Stocks PhD thesis Sto93 Take a look at Appendix C and at the file INSTALLDIR 1ib conf stdpartition spf to see what standard partitions are delivered with Fastest and how to define new ones We think the syntax is rather straightforward The user can edit this file to change erase or add standard partitions thus making this tactic quite powerful and flexible Fastest needs to be restarted if this file is changed because it is loaded only during start up To apply one of those standard partitions to an operation the command is as follows addtactic op_name SP operator expression 27 KeepMaxReading VIS KeepMaxReading DNF 1 KeepMaxReading SP KeepMaxReading SP _ P P 1 2 KeepMaxReading SP 3 KeepMaxReading S 4 KeepMaxReading_SP_5 KeepMaxReading_VIS KeepMaxReading_DNF_2 KeepMaxReading_DNF_1 KeepMaxReading DNF 3 KeepMaxReading DNF 2 genalltt KeepMaxReading DNF 3 Meepiaxneading_ a addtactic KeepMaxReading DNF 1SP smax s lt r genalltt genalltt a Applying just DNF b Applying DNF and then SP to just one test class KeepMaxReading VIS KeepMaxReading DNF _ KeepMaxReading S 1 PWE KeepMaxReading SP 2 l KeepMaxReading SP 3 KeepMaxReading VIS P 4 P5 KeepMaxReading_S KeepMaxReading_DNF_ 1 KeepMaxReading_S KeepMaxReading_SP_ KeepMaxReading SP Po KeepMaxReading_S KeepMaxReading_SP KeepMaxReading_SP_5 KeepMaxReading DNF 2 KeepMaxReading SP
64. ound tool to increase the accuracy of testing at the presence of quantifications 31 Important This tactic tends to produce more repetitive abstract test cases than SEQ 7 5 10 Strong Existential Quantifier Fastest s name SEQ This tactic is an stronger form of WEQ since it always generates a partition of the test classes where it is applied by conjoining the following predicate to the i test class produced by WEQ except to the last one 3x P a Ta vall A A Tn valt ech ae an where 21 Ti Pa T are the quantified variables and their types val val are the i combination of values taken from the set extensions provided by the user for each quantified variable and P is the quantified predicate For instance in the example shown for WEQ SEQ generates the following test classes TC gt 4 gt wAy ALE N y seqZ r 4AyH4 4 x gt wAyXHk gt head y gt 1 TG gt 4 gt wA head 4 gt 4 An daa N y seqZ rA 4AyF 4oet gt wAyF head y gt 1 TCG gt 6 gt wAy A Iz N y isegZ TACAyAF dN oz wAyF head y gt 1 TC4 gt 6 gt wA head 4 gt 6 A2 412 N yisegZ TACAyF N ozZwAyF head y gt 1 TC gt 23 3I1 N y seqZ cE 4 0 ny EL tr gt wAnyF gt head y gt 1 The command to add this tactic is the same than WEQ but changing WEQ for SEQ Important Fastest will not be able to automatically derive abstract test cases from test classes whose charact
65. owtt as we have said earlier As you can see Fastest failed to find abstract test cases for KeepMarReading SP 1 and KeepMaxReading_SP_9 while it should The reason is that for these test classes Fastest will choose 1 0 1 as the finite set for Z Then if you take a look at these test classes run showsch KeepMaxReading_SP_1 you can see that both predicates are satisfied either with two strictly positive or negative numbers but that it is impossible if only 1 0 1 is considered 14 KeepMaxReading VIS L KeepMaxReading DNF 1 KeepMaxReading_SP_1 KeepMaxReading SP 2 KeepMaxReading_SP_2 TCASE KeepMaxReading_SP_3 L KeepMaxReading SP_3_TCASE KeepMaxReading_SP_4 KeepMaxReading SP_4_TCASE L KeepMaxReading_SP_5 KeepMaxReading DNF_2 KeepMaxReading DNF_2_TCASE KeepMaxReading DNF_3 KeepMaxReading_SP_11 JE KeepMaxReading_SP_11_TCASE KeepMaxReading SP 14 L KeepMaxReading SP 15 L KeepMaxReading SP 15 TCASE Figure 9 The extended testing tree includes also the schema boxes representing test cases hanging from those leaves for which Fastest was able to find a test case KeepMaxReading_SP_1 KeepMaxReading_SP_5 smaz SENSOR Z smax SENSOR Z s SENSOR s SENSOR r Z r Z s dom smag s dom smag Smart s lt r Smart s lt r smar s lt 0 smar s gt Q r lt 0 r U e Fastest gives you the chance to define a finite model for each leaf You can do it
66. re terms are used before their declarations Once a specification has been loaded it can be explored printed and saved with the commands described in section 7 11 After loading a specification the user has to select one or more schemas to be tested Only schemas representing operations can be selected A schema represents an operation if it contains any combination of the following a an input or unprimed state variable or b an output or primed state variable To select an schema use selop followed by the name of a Z schema representing an operation The list of candidate Z schemas can be displayed with showloadedops with no arguments It can be selected as many schemas as needed by issuing the same number of selop commands A schema that was previously selected can be deselected with command deselop followed by its name 7 5 Applying Testing Tactics and Generating Testing Trees Testing tactics can be applied to any sub tree of any previously selected schema in particular they can be applied to the entire tree To apply a testing tactic to a particular sub tree that sub tree must already exist Then the first tactic can only be applied to the VIS of the operation The first tactic applied by Fastest is always Disjunctive Normal Form DNF see below To apply DNF to all the selected schemas just run genalltt Except for DNF tactic application is performed in two steps 1 Add the tactic to the list of tactics to be applied 2 Run
67. riable or type If there are no such constants then 0 1 2 or 1 0 1 are chosen depending on the indicated variable or type If there are such constants then a set of type Z will include all of them plus the integer number one unit less than the minimum of these constants and the integer number one unit more than the maximum of these constants While a set of type N will have the same property changing integer by natural and noting that if zero is one of the constants then it will be the minimum As has been said before these are the default rules that are applied if the user does not run any setfinitemodel command for a test class Seeds This option is similar to Given It takes the same constants adds the same upper and lower limits but also adds the mean value between each pair of consecutive constants found in the test class Same considerations than in Given apply if there are no N or Z constants and if zero is one of the natural numbers found in the class As can be seen this option sets the finite sets for the indicated variables or types 44 If a definition is given for type T and another definition is given for variable x of type T then the last takes precedence Also if there is another variable y of type T for which no finite set was defined by the user then the finite set for it will be the one defined for T In order to define the bindings for the fm option command eval might be helpful If one of
68. rtition for expressions of the form RO G R G RANGA RAI G IU R G dom R dom G R G HA dom G C dom R RF G Z dom R N dom G R GH dom R C dom G R G dom RN dom G dom G C dom R n dom R C dom G Standard partition for expressions of the form S lt R R RA 5 R S dom R RA SA 5 C dom R RH 8 5NdomR R S Ndom R dom R C S R S N dom R dom R C S S C dom R Standard partition for expressions of the form S lt R R 4 LE i R S dom R R S 9 C dom R RAS 745 5 H dom R R S Ndom R dom RC S R S N dom R dom R C S S C dom R 53 Standard partition for expressions of the form R gt S R U RET S rank RAL Kos C ran R RES 4 Sra R RA Sorank rankRcCS RA S rank 7 ran R C S 8 C ran R 54 D Elimination Theorems This appendix lists the elimination theorems delivered with this version All the elimination theo rems except ExtensionalUndefinition and UndefinitionByEmptiness were certified with the Z EVES proof assistant Saa97 Slightly weaker versions of the following elimination theorems were certi fied with Z EVES SingletonNotSet SingletonIsNotEmpty SingletonNotSubset SingletonMapplet NotInDom SingletonNotSubsetDom NrresCap SingletonMappletNotEqualRell SingletonNotSub setRel ExcludedMiddleSinglet
69. s all the empty test classes In Fastest pruning can be done manually or automatically We strongly suggest to use the automatic strategy and perhaps complement it with the manual one The simplest form and the one you should try first to use the automatic pruning is by running the following command prunett This command can only be run after genalltt Fastest will try to prune all the empty test classes but in some cases it will left some of them hanging from the tree This is due to the fact that the automatic strategy implements a best effort algorithm However the user can improve this strategy for the current or future projects by adding so called elimination theorems to a configuration file to know more about this go to section 7 7 1 After prunett is done you can either explore the remaining test objectives to see if some of them are empty and then prune them manually or tell Fastest to find abstract test cases as is explained in the following section we suggest this last curse of action In the example we are examining prunett actually prunes all the empty test classes so the user should not prune any node manually The resulting testing tree is shown in Figure 8 There are three commands to prune testing trees manually All of them receive a test class name as parameter 13 KeepMaxReading VIS 5 5 L KeepMaxReading DNF 1 KeepMaxReading SP 1 KeepMaxReading_SP_2 KeepMaxReading_SP_3 KeepMaxReading
70. s it can In general prunett will not be able to prune all the empty test classes since this problem is undecidable Then once prunett finishes it is possible that some empty test classes remain hanging from the tree In this case the engineer has two alternatives we recommend to follow the first one 1 Run genalltca to find abstract test cases from the remaining leaves 7 8 If Fastest could not find abstract test cases for some of them then expand each of these leaves and analyze each of them in order to determine whether they are contradictions or not If some are the engineer has again two options that will be described below if not setfinitemodel should be used 7 10 2 Expand each leaf and analyze it in order to determine whether is a contradiction or not If some are the engineer has again two options that will be described below if not run genalltca 7 8 In any case the engineer has two options when there are empty test classes that were not pruned by prunett We strongly recommend to follow the first one 35 1 Add one or more elimination theorems 7 7 2 then run loadelimtheorems 7 7 3 and finally run prunett again 2 Prune the test classes manually 7 7 5 If all the leaves of a given test class were pruned prunett will try to prune that test class too prunett and genalltca 7 8 can be run iteratively the former will try to prune only those leaves for which no abstract test case was found and the lat
71. s many times as needed specially after prunett and setfinitemodel 7 10 Every time this command is run it will try to find an abstract test case for those leaves for which there is none Then if the user manages to prune more test classes or helps Fastest to find abstract test cases for the remaining classes genalltca will run much faster than in previous executions Besides generating abstract test cases the output of this command is a series of messages printed on the screen For each test class being analysed the command first prints a message like this one Trying to generate a test cases for the class lt tcn gt where tcn is the name of the test class After some time Fastest will print one of the following messages for each test class e If Fastest found an abstract test case for a given test class the following message is written lt tcn gt test case generation gt SUCCESS e If Fastest was unable to find an abstract test case it will print one of the following messages which one will be printed depends on the value of some configuration variables lt tcn gt test case generation gt FAILED lt tcn gt test case generation gt FAILED without performing all the possible evaluations Once genlltca finishes the user can explore and save the abstract test cases with command showsch tca 7 11 Then the user has to analyse those test classes for which a FAILED message was printed As was explained above the F
72. s name NRI o o 10 11 11 11 11 13 14 17 17 17 17 18 19 19 20 20 21 21 7 5 8 Mandatory Test Set Fastest s name MTS o 7 5 9 Weak Existential Quantifier Fastest s name WEQ 7 5 10 Strong Existential Quantifier Fastest s name SEQ 7 6 Dealing with Axiomatic Definitions oa als a ar a TON Basterds A ee eee a ei ee Ge E T 6 2 Symbolic Constants o e e AAN EA a nuda LO A e bl saas d ash wl senp ann g ee a ren ee a cas tan O Hes S 7 6 4 All Other Declarations 4 aie A A FA ARH RAG Poo Command setaxdet ae na a oS oa ee A T ee Be a Be ee e Lalo Prine Testing Trees ao lr Se Phe a Sk tdo ek ee le oo ee C GAN AMON miming W amp oti AD IAE SAA TL Elimmation Theorems gt R 2 AA ARAS ASAS AA d 7 7 3 Loading the Elimination Theorem Library 7 7 4 Semiautomatic Pruning 2 22 6 3 2 a td ek ek A Sek aa ack Ew Tiros Mental PEU pe n Se Bee he hn A a Sh de ira an She toa 7 7 8 Generating Abstract Test Cases Ate eR ais de ADS A A Sk 7 9 Controlling the Generation of Abstract Test Cases 7 10 Defining Finite Models v den A ta BE ada he a Mee Si ae da ea ao 7 10 1 Default Finite Models 25 eii Ago YA E che no to Hed 7 10 2 Command setfinitemodel w w bra n tes A E pelen A hs po A A me ah 7 11 Exploring and Saving the Results ios any ee ee sot ri seme Ee S ve eee e 7 12 How to Quit Fastest Llar
73. setaxdef ident constant_declarations value where ident is the identifier for which the user wants to set a constant value and value is that value This means that Fastest will replace the identifier for the value when reducing expressions 7 6 3 and when calculating abstract test cases The optional parameter constant_declarations must be used when the value refers to constants of basic types see an example below For example the following command sets a value for Mid declared in Figure 15 setaxdef Mid 517 When such a command is issued Fastest checks that the type of the value is consistent with the type of the identifier Also it tries to check that the value satisfies all of the predicates appearing in axiomatic definitions where the identifier is referenced However this check can only be finished when all these predicates become constant i e when all the variables have been bound to a constant value Then when the last identifier is bound to a constant the predicate is evaluated and possibly an error message is printed Therefore if Fastest complains that the value that was last bound to an identifier does not verifies a predicate in an axiomatic definition the user should check whether this last value is the cause of the problem or it is the values previously bound to the other identifiers If this is the case the user can reset the previous values with the same command until no error messages are printed Command eval
74. t s purpose Hence you will get a broad idea of what kind of models are best suited for Fastest by first reading the appendix 6 2 Fastest Conforms to the Z ISO Standard Fastest parses and type checks specifications written in the TEX mark up that conforms to the Z ISO Standard ISO02 Then it does not accept Spivey s grammar 6 3 Fastest Is Meant to be Used for Unit Testing The main and foremost purpose of Fastest is to be an aid in unit testing Then specifications should represent units of implementation or they can be decomposed as such To be more clear we think in an unit as a subroutine a function or a method Therefore if your model ends with schema System representing the behaviour of the whole system and you try to test System Fastest will probably perform poorly Likely System is the disjunction of a number of primitive operations each of which probably represents a unit of implementation Hence you will get the best of Fastest by trying to test each of these operations in isolation instead of working directly with System One important point here is that software design i e decomposing the software into a set of elements assigning a function to each element and defining their relationships GJM91 should guide the specification In doing so you will identify a set of modules or components each providing a public interface to the rest of the system Each module should be simple and small enough to be
75. t there is unsaved data To leave the program just type quit and press the return key 47 A Z Features Unsupported by Fastest The following Z features are still unsupported by Fastest the list is not exhaustive e The hide hide operator Fastest will crash if the specification being loaded uses this operator e Schema names referenced in the predicate part of some schema The referenced schemas will not be unfolded thus severely reducing the effectiveness of both automatic pruning and abstract test case search Test case design will still be quite meaningful e Variable substitution Schema expressions such as A a b where A is a schema and a and b are variables are not supported If B Ala b then B will not be recognized as an operation regardless of A e The following operators if min and maz The if clause will not be rewritten when DNF is calculated as it should be If some expression of some satisfiable test class contains min or maz then it will be impossible to find an abstract test case for that test class e The MTEX mark up input Command loadspec will only load the specification explicitly present in the file passed as parameter It will ignore any input commands present in that file e Inductive types Fastest is unable to find abstract test cases from test classes whose predicates include references to non constant constructors defined in inductive types Automatic pruning might not work correctly in t
76. ter will try to find an abstract test case for them prunett is quite fast but if the number of test classes is very large or they have large predicates the process might take several minutes 7 7 2 Elimination Theorems A test class should be pruned from a testing tree when it is an empty set A test class is an empty set when its predicate is a contradiction For instance the following test classes are empty sets since in SCAddCat_SP_1 the proposition c is false and in SCAddCat_SP_5 the conjunction categs A categs C c is a contradiction SCAddCat_SP_1 SCAddCat_SP_5 level Z level Z categs PCATEGORY categs P CATEGORY MAXNCAT N MAXNCAT N c CATEGORY c CATEGORY c E categs c Z categs categs categs c te t categs C c prunett analyses the predicate of each leaf in a testing tree to determine if the predicate is a contradiction or not Since the problem of finding contradictions in first order logic is undecidable Fastest rests on a best effort algorithm The algorithm uses a library of so called elimination theorems each of which represents a contradiction For example the following two elimination theorems are included in the library Elimination Theorem SingletonIsNotEmpty x X x th Elimination Theorem NotSubsetOfSingleton A PX x X AY Ac zs Fastest uses the library of elimination theorems to prune inconsistent test classes
77. ters of an elimination theorem or equivalence rule by actual parameters A subtyping rule determines whether a type or set is a subtype of another type or set For instance X gt Y isa subtype of X Y which in turn is a subtype of X Y The subtyping rules applied by Fastest are listed in Table 16b During the pruning process Fastest substitutes formal parameters of type T in an elimination theorem for terms of any of the subtypes of T Hence if in a test class there is a term f of say type N CHAR then the parameter R in theorem NotInEmptyDom above will be substituted by f because X Y is a subtype of X Y N matches X and CHAR matches Y So whenever the engineer adds an elimination theorem he or she should make his or her best effort in writing the most general possible formal parameters because the theorem will serve to prune more test classes in future projects 39 Syntactic substitutions Fastest also performs a number of syntactic substitutions that are com mon to the Z notation in the elimination theorems rewrite rules and test classes To name some unnecessary parenthesis are removed and expressions like f x f x and f x are written in a com mon format In this way the user does not need to worry about how predicates have been written 7 7 3 Loading the Elimination Theorem Library The elimination theorem library is automatically loaded during start up If the user adds or modifies the configuration file containing
78. the size options is used but there is a definition within the fm option for a type or a variable which involves a set with a different number of elements then the last takes precedence For example in setfinitemodel any class nsize 3 fm Nnat 1 2 3 4 the finite set for type N will be 1 2 3 4 although it has four elements and not three But if there are more than one variable of say type N one of which is x then setfinitemodel any class nsize 3 fm x 1 2 3 4 will make Fastest to assign 1 2 3 4 to z and another three element set for the other variables which will be calculated following the default rules setfinitemodel can be run after genalltt and before and after genalltca 7 11 Exploring and Saving the Results The specification and the results of the work carried on with Fastest can be displayed or saved in ET X format with the commands of the show family Important If Fastest terminates by any means all data will be lost unless the user has saved it in files with one or more of the commands described in this section showloadedops prints the names of all the Z schemas that look like operation schemas Fastest considers that a Z schema is an operation schema if it includes input or before state variables on one hand and output or after state variables on the other If an schema is the result of an schema expression then all of them might be considered operations For instance if A B V C and B and C
79. this server is not fully implemented e This process structure takes advantage of a quite obvious fact abstract test cases can be easily and efficiently calculated by a highly parallel system testing testing server server knowledge base server testingy server testing server Paea a ky eet r a a E iye l sync Figure 5 Fastest s process structure is composed by a number of clients and servers and just one instance of a knowledge base server 5 5 1 5 2 5 3 An Example We have said that MBT takes as input a formal model of the system to be tested Fastest uses Z specifications The current version does not support the full language see Appendix A for a list of the unsupported Z features The Model A Z Specification Z is a formal notation useful to specify systems that will use complex data structures and will apply complex transformations over them The Z notation is a textual language based on typed first order logic and discrete mathematics For standard presentations of the Z language read any of the excellent available books such as PST96 Jac97 Dil90 and WD96 available on line from here A Z model is a state machine where states are defined by state variables and transitions are predicates over those variables Running Fastest and Loading the Specification We will apply Fastest to test a function that must keep the highest readings taken from a set
80. tifications or negations of universal quantifications It should be noted that this tactic might not produce a partition of the test classes where it is applied if this is unacceptable then see section 7 5 10 Conceptually this tactic transforms a quantification over a potentially infinite set into a quan tification over a user provided set extension Since an existential quantification over a finite set is 30 equivalent to a disjunction then WEQ first transforms the existential quantification into a disjunc tion Then it writes the disjunction into DNF and finally it generates as many test classes as terms the DNF has plus one more characterized by the negation of the other predicates Consider the following example Original predicate z N y seqZez gt wAy gt head y gt zx Set extensions provided by the user z 4 6 y 4 4 gt w A 4 gt head 4 4 V 6 gt wn 4 4 gt head 4 gt 6 A gt why V4 gt w Ahead 4 gt 4 VD MW AN LU V6 gt wA head 4 6 TO 74 gt wAy TG 4 gt w A head 4 gt 4 TC3 gt 3 gt 6 gt wAy Test classes generated by the tactic TC 46 wA head 4 6 TCs gt 3x N y segZ z Z 4 6 A y Z 4 TMW AUE head y gt r First transformation The predicate is written in DNF In order to apply WEQ the user has to indicate the quantified predicate and a set extension for each bound variable or a set extension for each type of
81. tion variable MAX EVAL has been added to limit the number of evaluations when searching for abstract test cases see section 7 8 e A configuration variable DEF SIZE FINITE SET has been added to set the size of finite sets which latter are used to find abstract test cases see section 7 8 e It is possible to load specifications where terms are used before their declarations e Command line editing features like tab completion have been added see section 7 1 1 e In this version it is possible to apply a testing tactic to a selected sub tree of a testing tree and not just to the entire tree as in previous versions e The performance of the abstract test case generation algorithm was improved 2 Introduction to Model Based Testing Testing could be the most costly phase of a software development project We can use formal methods to make testing almost automatic thus changing the cost of testing by the cost of formalization which is reported to be quite less expensive Model based testing MBT uses a formal specification to generate test cases and to verify whether they found errors in the program or not Figure 1 depicts one of the possible MBT methodologies a part of which is implemented by Fastest The methodology is based on SC96 HP95 and Sto93 Testing starts by writing a model of the software under test At the beginning the model is used to generate test cases At the end the model is used as an
82. ty Journal 4 309 327 1995 ISO02 ISO Information Technology Z Formal Specification Notation Syntax Type System and Semantics Technical Report ISO IEC 13568 International Organization for Standardiza tion 2002 Jac97 Jonathan Jacky The Way of Z Cambridge University Press 1997 Lam02 Leslie Lamport Specifying Systems The TLA Language and Tools for Hardware and Software Engineers Addison Wesley Professional 2002 PST96 Ben Potter Jane Sinclair and David Till An Introduction to Formal Specification and Z Prentice Hall International 1996 Saa97 Mark Saaltink The Z EVES System In J P Bowen M G Hinchey and D Till editors ZUM 97 The Z Formal Specification Notation pages 72 85 1997 SC96 P Stocks and D Carrington A Framework for Specification Based Testing IEEE Trans actions on Software Engineering 22 11 777 793 November 1996 Sto93 P Stocks Applying Formal Methods to Software Testing PhD thesis Department of Com puter Science University of Queensland 1993 ULO6 Mark Utting and Bruno Legeard Practical Model Based Testing A Tools Approach Morgan Kaufmann Publishers Inc San Francisco CA USA 2006 WD96 Jim Woodcock and Jim Davies Using Z specification refinement and proof Prentice Hall Inc Upper Saddle River NJ USA 1996 60
83. up lt sch_name gt o The name of the schema to be displayed lt unfold_order gt Displays the result with more or less detail basically it ex pands up to some level the in cluded schema boxes u 1 expands all the schemas lt file_name gt Same as before showsch tca Displays all of the schemas correspond ing to abstract test cases of all testing trees AT EX mark up u lt op_name gt Displays only the abstract test cases of operation schema op_name lt unfold_order gt Same as before lt file_name gt Same as before showsch tcl Displays all of the schemas correspond ing to test classes of all testing trees ETEX mark up lt op_name gt Displays only the abstract test classes of operation schema op_name lt unfold_order gt Same as before lt file_name gt Same as before 46 Command Description Options showspec Displays the entire specification BT X mark up u Same as u 1 before o file name gt Same as before showtt Displays all of the testing trees p lt op_name gt Displays only the testing tree of operation schema op_name o lt file_name gt Same as before x Displays also the test classes that were pruned 7 12 How to Quit Fastest Important Before leaving Fastest save your results Fastest will not save anything by default and will not remember you tha
84. ypes essentially by making all the legal combinations between the elements of the finite sets defined for the basic types For instance the finite set for PZ will be 1 0 1 1 0 1 1 0 1 1 0 1 if the finite set for Z is 1 0 1 7 10 2 Command setfinitemodel If the default finite model does not satisfies the predicate of the test class being analysed i e a FAILED message was printed for it or if the finite model is too large i e an UNKNOWN message was printed the user can help Fastest to select a better finite model for that test class The command to do this is as follows setfinitemodel class_name options where class_name is the name of a test class in some testing tree and options can be any combination of e nzsize lt size gt This option sets the size of the finite sets for N and Z if the class does not contain arithmetic constants otherwise Given is applied see below e btsize lt size gt This option sets the size of the finite sets for all the basic types e size lt size gt This option sets the size of the finite sets for all the preceding types If either nsize and size or btsize and size are used together then nsize and btsize always takes precedence 43 e fm bindings where bindings is a semicolon separated sequence of one or more bindings Each binding must have the following form var type set_extension where var and type are any variable or type app

The Fastest 1.3.6 User's Guide

Contents

Download Pdf Manuals

Related Search

Related Contents