Home

Model Testing – Combining Model Checking and Coverage Testing

1. Legend Spec Specification SUC System under consideration Mspec Specification model Mem Behavioral model Mpsen Design model Msys System model Fig 1 Simplified process of software development Large software systems are developed in several stages see Fig 1 The initial stage of the development is usually the requirements definition its outcome is the informal specification of the system s behavior Spec The informal specification is converted to a formal specifi cation model Mspec A design model of the system Mpsgn is then developed and used to guide the implementation efforts that will yield the actual product the system under consid eration SUC as called in this thesis After the implementation a behavioral model Mar can be extracted from the SUC in order to understand the system s behavior Preliminaries 6 In this thesis the SUC will be modeled in two ways the design model and the behavioral model The term system model Msys is used in this thesis as a synonym referring to Mpsgn or Mn depending on the availability of the models 3 1 1 Specification Model During the requirements definition a specification model Mspec prescribes the desirable behavior as it should be i e the functionality of the system in compliance with the require ments of the user Using a simple but a formal notation for Ms is important to enable a dis cussion of the requirements with the user and the depl
2. System out println Appendix B Property Generation Tool 49 package propgen import java io xx x The class PropertyGenerator reads the specification files x The class PropertyGenerator processes specification files in plain text form x The system properties are generated from the ESG s in the form of an adjacency matrix As the adjacency matrix is stored as a plain text file the PropertyGenerator class do 1 li i read the file line by line li ii extract the system evens from the title line li iii generate node properties for each system event li iv generate edge properties for each entry of the adjacency matrix li v generate some supplementary declaration code for edge properties 1 For debugging just remove the comment sign before the System out println instructions Qsee propgen PropertyGeneratorApp Qsee propgen PropertyGenerator version 1 0 06 Mai 2005 author Baris G ldali public class PropertyGenerator xx x The directory where the specification files are stored The output is also x saved in this directory ST public String directory xx x The array in that the specification files are stored Each element in this x array is processed by the generateProperty method public String specificationFiles xx x The dimension of the adjacency matrix At the beginning the value is zero A public int dimens
3. record en stop en Track en gt X gt X gt X gt X gt X G play_ex G play_ex G play_ex G play_ex G play_ex G pause ex gt X gt X eu X gt X gt X G pause_ex G pause_ex G pause_ex G pause_ex G record ex G record ex G record ex G record ex G record ex gt G stop ex gt X gt X gt X gt X G stop_ex gt X G Track_ex gt X gt X gt X 2v d gt X G stop_ex G stop_ex G stop_ex G Track ex G Track ex G Track ex G Track ex Node Property SPEC SPEC SPEC SPEC EF forward ex EF rewind ex EF track pos ex EF jump ex Edge Property DEFINE Track ex forw track pos ex j play en pause en record en stop en Track en play en pause en record en stop en Track en X play en X pause en X record en X stop en X Track en play en pause en record en stop en Track en play en pause en record en stop en Track en ard ex rewind ex ump ex Appendix C Complete NUSMV Code of RJB Module 60 DEFINE Track en forward en rewind_en SPEC EF mute ex track pos en jump en Edge Property LTLSPEC G forward ex gt X forward en DEFINE Mode ex shuffle ex LTLSPEC G forward ex gt X rewind en continue ex volume ex mute ex LTLSPEC G forward ex gt X track pos en DEFINE Mode en shuffle en LTLSPEC G forward ex gt X jump en
4. 2 ESG this directory contains the specification files from Appendix A 3 PropertyGenerationTool Java application introduces in section 5 3 2
5. checking as a completeness criterion Since the author of this thesis is also a co author of the given references 8 and 9 some paragraphs of this thesis are textually similar to the ones in these references Contents ls Contents EN Ee 1 2 Formal Methods for Software Validation and their Combination Related Work 3 De Preliminare Sa ns ee se o aede ein 5 3 1 E e EE 5 LE Tee TE DEET 6 3 1 2 System Behavior Model sss unda ak Ba Le UM NES cada 7 32 Speeification Based Testing onnes ee ee 8 324 Test Case Generations ea 8 3 2 2 Test Coverage and Spanning Set ec cedere lu 9 3 23 SHONSIO VIEWS sce a a oa enge Base 9 3 3 Model EE ra Ta a TITT JNE 10 E ak kee 10 332 Temporal LOGIC suis pas EG NE b vu dee ae H 11 Sana Models Ne CREE essa iii ie ee weten eu 13 4 Coverage Driven Model Checking A 14 4 1 Converting the System Model into a Kripke Structure 16 4 2 Example Traffic Light Systemi SI A NI 17 4 3 Covering the Specification Model sss sI ee 19 43 1 Node COV Cha Se casaca LA a du SAK Rd Mo 20 4 322 Edse Coverage a el en 20 4 3 3 Complementing the Edge Coverage eese 21 4 4 Check Cases and their Generation side Keane 23 4 5 Model Checking of Check Cases na a u 24 4 6 Complexity Analysis of the Approach sese 25 S tasestudycand ToobSuppObEausse are i I Onus e IRE S ad hup Pad ts ud ins 26 5 1 Specification Mode re 27 5 2 System Model sudo sss sm a HN 30
6. 29 which will be used to illustrate the approach in the rest of this chapter The desired functionality of a traffic light system is as follows Beginning with the color red stopping the traffic flow it changes to red yellow and then to green allowing the traffic to flow After green it changes to yellow and then again to red It is assumed that an external actor e g a controller triggers some events in order to change the state of the traffic light The desired system function will be translated into a formal specification A faulty system model is also constructed in order to show how the approach operates The informal specification above can be formalized with a specification model Mspec Vspeo Espec vo where Vspec tred red yellow green yellow Espec red red yellow red yellow green green yellow yellow red vo red Fig 4 depicts Mspec graphically in the form of an ESG Coverage Driven Model Checking 18 IS Fig 4 Traffic light system specification as an ESG A supposedly faulty Msys for the traffic light system is given in Fig 5 in the form of a FSM The states of Ma represent the colors of the traffic light system The transitions repre sent the color changes of the traffic light system The fault in Maer is obvious The state where the traffic light changes to red yellow is missing Such a fault is useful to demonstrate how the approach localizes the injected fault Fig 5
7. 5 3 FOOL SUDDOLD a io cn comedians Rn A aa 32 5 3 1 Representation of System Model 33 5 3 2 Property Generation OOl sss essen 35 Contents Il 5 3 3 Model Checking ProcesS sss sss mt pp 37 5 4 EE 39 6 Conclusion and Future Work nannte 41 Figure THAER an RE ve ee 42 Mable der see e ete a eI 43 References ae etre eed nd alodium 44 ANGKIOWIGOBITIE TES ostio ta E ETAN RT GESTA NR AS E dial da A po aedis scd 46 Appendix A Specification Piles of ESG Sii se i a an 41 Appendix B Property Generation Tool e esses eene eene eene 48 Appendix C Complete NUSMV Code of RJB Module 56 Appendix D Model Checking Results of the generated Dropertes 61 Appendix E Content of the attached CD 2 ertet Zeie eec ebda 64 Introduction I 1 Introduction With the growing significance of computer systems within industry and wider society techniques that assist the production of reliable software are becoming increasingly important The complexity of many computer systems requires the application of a battery of such tech niques Two of the most promising approaches are model checking and software testing 13 Software testing is the traditional and most common validation method used in the software industry today 3 12 29 It entails the execution of the software system in the real environ ment under operational conditions thus testing is directly applied to the software It is user centric
8. After modifications the model checking process must be repeated Coverage Driven Model Checking 14 4 Coverage Driven Model Checking The approach presented in this thesis aims to check the SUC against the user requirements just as validation and verification aim to do This check can be done in different stages during the software development process Testing for example is mainly applied manually after the implementation of the SUC in its real environment if errors are detected the SUC must be debugged and the relevant portions of the program code must be corrected Model checking can be applied automatically on a system abstraction to check whether the system abstraction contains errors in the case of software this could be a design model if there are some errors they are corrected on the design long before implementation But what about gaining testing information on the SUC before implementation or applying model checking after the SUC is implemented Combining both methods as explained in this thesis has the advantage that testing activities can be transferred into early stages of the development process and can be automated To put it more precisely the approach realizes a coverage based test adequacy criterion 5 6 32 as explained in section 3 2 on Msyst by using model checking A set of properties are de rived from Mspee and model checked on Ma Since the properties are produced from specification based test cases th
9. LTL False T9 066 G Track_ex gt X pause_en LTL False T10 068 G Track_ex gt X stop_en LTL False T11 Fig 21 Properties verified to be false by model checking Table 9 Detected faults for the system function Play and Record a CD or Track No Faults Detected While recording pushing the forward button or rewind button stops the recording process without a due warning Property 59 If a track is selected but the pointer refers to another track pushing the play button invokes playing the selected track the situation is ambiguous 3 During playing pushing the pause button should exclude activation of record button This is not ensured Property 52 4 Track position could not be set before starting the play of the file Property 65 While playing a track the record button should be disabled however it is enabled Property 47 While pausing or recording the stop button should be enabled however it is disabled 6 Properties 53 and 58 There exists some state where the play pause and stop buttons are disabled after executing Track Properties 65 66 and 68 Conclusion and Future Work 41 6 Conclusion and Future Work A new approach to combining specification based testing with model checking introduced in 8 and 9 has been extended and automated The novelty of this approach stems from 1 the holistic view that considers the testing of
10. A faulty Ms as a FSM Fig 6 transfers the FSM in Fig 5 into a Kripke structure The Kripke structure conserves the three states red green and yellow of Maa as normal states Sys but rename them as s s2 and s3 Additionally three transition states s4 ss ss are generated for each transition in Msysr The atomic propositions generated from the events specified in Mspec are assigned to normal and transition states expressing either being enabled or executed at that state For example considering the state transition red yellow in Fig 5 the event yellow must be enabled at state s of the Kripke structure corresponding to the state red in Msys thus s is labeled with the atomic proposition yellowen The additional transition state s4 represents the point of time where the event yellow is executed thus it is labeled with the atomic proposition yellow S yellow i yellow en yellow en Fig 6 Kripke structure for Maa of Fig 5 Coverage Driven Model Checking 19 Formally the Kripke structure is defined as a quadruple K S So R L where S 51 82 83 4 5 S6 where Sys 87 S2 ss and Srs 54 55 56 So si R 51 sa Su 53 85 55 55 51 82 56 56 53 L sp yellowen L s2 yellowen L s3 reden L s4 yellowe L ss reda L s6 yellowex 4 3 Covering the Specification Model As explained in section 3 2 2 adequacy criterion is
11. DEFINE SelectTrack en check none en check on en check off en LTLSPEC G check all en LTLSPEC G check all ex check all ex check none en LTLSPEC G check on en LTLSPEC G check all ex check all ex check off en LTLSPEC G check none ex check all en LTLSPEC G check none ex check none en LTLSPEC G check none ex check on en LTLSPEC G check none ex check off en LTLSPEC G LTLSPEC G check on ex gt X check all en check on ex check none en gt X gt X Mode_en gt X gt X check_all_ex check_all_en LTLSPEC G check_on_ex gt X check_on en LTLSPEC G check_on_ex gt X check_off_en LTLSPEC G check_off_ex gt X check_all_en LTLSPEC G check_off_ex gt X check_none_en LTLSPEC G check_off_ex gt X check_on_en LTLSPEC G check_off_ex gt X check_off_en Node Property SPEC SPEC SPEC SPEC SPEC Edge DEFINE DEFINE 3 Boe PE E E 3 E pipe Et E Ei E TLSPEC TLSPEC TLSPEC LSPEC TLSPEC TLSPEC LTLSPEC LTLSPEC LTLSPEC LTLSPEC LTLSPEC LTLSPEC TLSPEC TLSPEC TLSPEC LSPEC TLSPEC TLSPEC LTLSPEC TLSPEC LTLSPEC LTLSPEC LTLSPEC LTLSPEC LTLSPEC EF play ex EF pause ex EF record ex EF stop ex EF Track ex Property PlayTrack ex play ex pause ex record ex stop ex Track ex PlayTrack en play en pause en
12. Track Mode SelectTrac k playing pause record N stop A Track 1SelectTrack Mode stopped play Arecord ATrack A SelectTrac k Mode A stop record play Track recording paused play Arecord stop pause stop ATrack A Track SelectTrack Mode SelectTrack Mode S 13 SelectTrack Mode K Track nMode A SelectTrack Fig 11 Maa of the top GUI level of the RJB The transition information in FSM normally gets lost during translation of the system model into a Kripke structure because by definition 3 Kripke structures do not entail a labeled transition relation However in order to keep this information transition states are added to the Kripke structure as explained in section 3 3 1 For each transition in the FSM a transition state in the Kripke structure is added and labeled with an atomic proposition indicating the transition label For example if the transition from stopped state to playing state in the system model is triggered by the p ay button then the corresponding transition state is labeled with the atomic proposition playa The transition states have no logical names like playing or stopped they are named with a consecutive number Fig 11 depicts Maa as a Kripke structure of the same abstraction level as Fig 10 Case Study and Tool Support 32 For mo
13. Visit the Sites 13 Configuration Wizard 7 Visualization Case Study and Tool Support 28 Each system function represented as an ESG serves as a specification model Ms for the approach As an example the Ms in Fig 9 specifies the top level GUI interaction for the de sired system function Play and Record a CD or Track The user can play pause record stop the track fast forward and rewind Fig 9 illustrates all legal event sequences related to user system interaction which realize the operations the user might launch when using this system function The main functionality is specified by the utmost level ESG RJBI RP SelectTrack f X O X F Mode Select Track VP Play track Play Track Start B as Play E e Track Fig 9 Ms for the system function Play and Record a CD or Track Because of the large amount of possible interaction sequences given in the user manual for this system function related system event sequences are grouped into other ESG s e g Select Track which are then used as pseudo events in the main ESG RJBI As a convention the pseudo events are identified by a capitol letter distinguishing them from system events Apart from the internal event sequences in ESG Select Track an edge from the pseudo event Select Track to itself in ESG RJBI makes all combinations of event sequences in ESG Select Track possible Similarly an edge from Select Track
14. al Nusmv 2 An opensource tool for symbolic model checking Proc of Computer Aided Verification CAV 02 2002 19 E M Clarke E A Emerson A P Sistla Automatic Verification of Finite State Concur rent Systems Using Temporal Logic Specifications ACM Trans Programming Languages and Systems vol 8 no 2 pp 244 263 Apr 1986 20 E M Clarke O Grumberg D Peled Model Checking MIT Press 2000 21 A Engels L M G Feijs S Mauw Test Generation for Intelligent Networks Using Model Checking Proc of TACAS 1997 pp 384 398 22 A Gargantini C L Heitmeyer Using Model Checking to Generate Tests from Require ments Specification Proc of ESEC FSE 99 ACM SIGSOFT 1999 pp 146 162 23 A Gill Introduction to the Theory of Finite State Machines McGraw Hill 1962 24 M P E Heimdahl S Rayadurgam W Visser G Devaraj J Gao Auto generating Test Sequences Using Model Checkers A Case Study FATES 2003 pp 42 59 25 E Kindler Modelchecking Lecture Notes University of Paderborn 2004 26 K L McMillan Symbolic Model Checking Kluwer Academic Publ 1993 27 Object Management Group UML specification version 1 3 June 1999 www omg org 28 V Okun P E Black Y Yesha Testing with Model Checker Insuring Fault Visibility WSEAS Transactions on Systems 2003 pp 77 82 29 D Peled Software Reliability Methods Springer Verlag 2001 30 D Peled M Y Vardi M Yannakak
15. an event sequence i e v v e E In this context v v is interpreted as a legal event sequence of the event sequencing relation E Additionally Mspec identifies a node vo e Vas the starting node A specification model Mspec V spec Espec vo defined as an ESG with a starting node vo de scribes a set of sample behaviors of a system Because the requirements of the user are speci fied in the early stages of behavioral modeling the outcoming specification model may not be Preliminaries 7 complete As the design phase evolves the present specification model can be modified or extended depending on the changing requirements of the user It is also possible to define forbidden scenarios with ESG i e ones that are not allowed to happen This complementary view of the requirements specification holistic view will be introduced in section 3 2 3 helps to differentiate between desired and undesired system behavior Based on Definition and its interpretation above the complementary specification model of Mspe is formally represented by another ESG M sec V spec E ze Vo where V spe represents the same set of events of Mspec E spec Vspec X Vspee Espec contains all complementary event sequences not included in Espec where any v v E spe is interpreted as an illegal event sequence Vo Vspec is the same initial node of Maes 3 1 2System Behavior Model For verification purposes the behavior o
16. fmust be true 20 The two useful sublogics of CTL are branching time logic and linear time logic The dis tinction between the two lies in how they handle branching in the underlying computation tree In branching time temporal logic the temporal operators quantify over the paths that are possible from a given state In linear time temporal logic operators are provided to describe events along a single computation path 20 Definition 4 Computation Tree Logic CTL is a restricted subset of CTL in which each of the temporal operators X F G U and R must be immediately preceded by a path quanti fier In other words CTL is the subset of CTL that is obtained by restricting the syntax of path formulas using the following rule If and g are state formulas then X f F f G f f U g f R g are path formulas Definition 5 Linear Temporal Logic LTL on the other hand consists of formulas that have the form A f where fis a path formula in which the only state subformulas permitted are atomic propositions An LTL formula is either Preliminaries 13 p where p is an atomic proposition or a composition f fv g fag XfFA GA SU g fR g 20 In this thesis both CTL and LTL formulas are used to specify system properties The system properties defined with temporal logic formulas can be grouped into classes corresponding to their art of formulating the property Three of these property classes are the followings Reac
17. gt X7g The size of the formulas f is always constant Because of this fact the exponential growth of the complexity of LTL model checking can be ignored and the resulting complexity is O Bel x Ssysd HR sysi Additionally CTL model checking is deployed for each formula f generated from nodes of Mspee The number of all nodes is Vspecl 19 implies that the complexity of the CTL model checking is O SH R x f Since the node properties always have the form EFp the size of the formulas f is always constant thus the complexity depends just on the size of Msysi O Ssys Rsysd After adding the complexities of model checking both the node properties and the edge properties the overall complexity of the approach is measured as O V spel X Ssvsd IR sys Case Study and Tool Support 26 5 Case Study and Tool Support In order to show the applicability of the approach to a non trivial system a case study is carried out Applications with a graphical user interface GUI are suitable to be checked by the approach because the user interacts with the system via events The user can trigger these events via graphical components called WIMPs Windows Icons Menus and Pointers like buttons real RealJukebox n x File Edit View Controls Playlists Tools Sites Help 000000 99 44 J 3 Home Play Record CD 4a D Artist bum Genres Check All O Check None Reco
18. interpreter Therefore the Kripke structure representing the system model of RJB from Fig 11 is translated as a single process into amain module see Fig 12 which includes assignment statements specifying the initial values of the state variables and the tran sition relation between the system states The NuSMV code in Fig 12 is not complete the missing code portions are represented with This section of the thesis will extend the code by and by MODULE main represents the system model while playing and recording a CD or Track VAR state stopped playing paused recording sl s2 s3 S4 S5 S6 87 S8 89 S10 s11 s12 s13 sl4 ASSIGN init state stopped next state case state stopped sl s8 s11 state sl state s4 state s12 playing state playing s2 s3 s10 s12 state s2 state s5 state s11 stopped state paused s4 s5 s6 s13 state s3 state s13 paused state recording s7 s9 s14 state s3 state s13 recording 1 state esac Fig 12 State declarations initial state assignment transition relation The state space of the Kripke structure is determined by the declaration of the state vari ables i e a state of the model is an assignment of values to a set of state variables The vari able state is a scalar variable which can be assigned the symbolic values stopped playing paused recording to represent t
19. not only the desirable system behavior but also the undesirable one and 11 supporting and partly replacing the test process by model check ing The specification language chosen is an intuitive and user oriented one rather than an ab stract engineer oriented language The aim of choosing a simple language is to keep the communication with the user during the requirements analysis phase simple and efficient so that many possible scenarios can be described in a simple and quick way These informal de scriptions will be used afterwards in generating verification information An intuitive way of constructing the system model has been considered Proposals also ex ist however for the formalization of the model construction e g in 30 applying learning theory Taking these proposals into account would further rationalize the approach The approach has numerous advantages over traditional testing Firstly model checking is automatically performed resulting in an enormous reduction of the costs and error proneness of manual testing Secondly the generation of system properties is controlled by the coverage of the specification model and its complement This enables an effective handling of the completeness and oracle problems The complexity of the approach is exponential in the size of the specification model but linear in the size of the system model because of the constant size of the properties generated The automatic generation of t
20. or Track 28 Fig 10 System model of RJB as a FSM na 30 Fig 11 Msys of the top GUI level of the RB anne SAS 31 Fig 12 State declarations initial state assignment transition relation 33 Fig 13 Declarations of atomic propositions initial state assignment transition relation 34 Fig 14 Node properties for ESG Play Track ois sese ise ika aa suas ei 36 Fig 15 Not complete list of edge properties for ESG Play Track sess 36 Fig 16 DEFINE declaration for pseudo event Track 37 Fig 17 Starting NuSMV in interactive MOVE oa ee 37 Fig 18 The output of the snow property command before the verification 38 Fig 19 Brot trace ot NUSMW 135 dota page a 38 Fig 20 The output of the snow property command after the verification 39 Fig 21 Properties verified to be false by model checking sss 40 Table Index 435 Table Index Table 1 Node properties for the traffic light system sms eee 20 Table 2 Edge properties for the traffic light system 21 Table 3 Complementary edge properties for the traffic light system 22 Table 4 Check cases generated from the system properties of the traffic light system 23 Table 5 Manual model checking of system properties ss sseeesennennznennzznnnzznntzznnzi 24 Table 6 System functions of KIB au ll 27 Table 7 Specification file of the top lev
21. s6 1 next state s11 next state S12 next state s8 1 next state s13 1 next state s10 1 Is 09 1 OF esac esac next check off ex case next stop ex case next state s11 next state s12 next state s2 1 next state 813 1 next state 85 1 1 0 1 0 esac esac Appendix C Complete NUSMV Code of RJB Module 58 next shuffle en case next forward en case next state sil next state 12 next state sll next state s12 next state s13 0 next state s13 0 Je Za ds do esac esac next continue en case next rewind en case next state sil next state 12 next state sil next state s12 next state s13 0 next state s13 0 Tad de ds esac esac next volume en case next track pos en case next state sil next state 12 next state sll next state s12 next state s13 0 next state s13 0 qe ds qz s esac esac next mute en case next jump_en case next state sil next state 12 next state sil next state s12 next state s13 0 next state s13 0 lias Los qu us esac esac next shuffle ex case next forward ex case next state s11 next state 12 next state sil next state s4 next state s13 1 next state s12 1 Tz Oy 1 0 esac esac next continue_ex case next rewind_ex case
22. show property command before the verification With the command check property the verification of the properties can be started check property checks both CTL properties and LTL properties As the verification of the properties runs the result for each property is printed If a property is verified to be valid true an output is printed as follows specification G Track ex gt X record en is true If a property is verified to be invalid false a counterexample is generated A counterexam ple is an error trace of the system that falsifies the property The shortened output of the model checker for an invalid property is as in Fig 19 specification G Track ex gt X stop en is false as demonstrated by the following execution sequence Trace Description LTL Counterexample Trace Type Counterexample gt btates bll state stopped check all ex 0 check all en 1 check none ex 0 check none en 1 Fig 19 Error trace of NUSMV Case Study and Tool Support 39 Once the verification of the properties has ended the results are stored in the property list as explained above The updated list of properties can be shown again with command show property as in Fig 20 NuSMV gt show property PROPERTY LIST Type Status Counterex Trace PROPERTY LIST 000 EF SelectTrack ex CTL True N A 001 EF Mode ex CTL True N A 047 G pl
23. 2 state s2 state s5 state S11 stopped state paused s4 s5 s6 s13 state s3 state s13 paused state recording s7 s9 s14 state s3 state s13 recording 1 state esac Appendix C Complete NUSMV Code of RJB Module 57 next play_en case next check all en case state s2 state s3 state s5 next state sil next state s12 state s11 state s13 1 next state s13 0 T5 si Os ds do esac esac next pause_en case next check none en case state sl state s4 state next state sil next state s12 S12 1 next state s13 0 Loa Or La 15 esac esac next record en case next check on en case state s6 state s8 state s10 next state s11 next state s12 state s14 0 next state s13 0 l 3e qz s esac esac next stop en case next check off en case state sl state s4 state next state sil next state 12 S12 1 next state s13 0 1 0 qu us esac esac next play ex case next check all ex case next state sl 1 next state s11 next state s12 next state s4 1 next state s13 1 T Or Tee rs esac esac next pause ex case next check none ex case next state s3 1 next state s11 next state s12 next state 87 1 next state 813 1 15 05 1 0 esac esac next record ex case next check on ex case next state
24. 9 the property generation tool generated 101 corresponding system properties in NuSMV language A complete list of the properties and the source code of the property generation tool can be found in the appendix These properties are the inputs for check cases as introduced in section 4 4 As the expected output of the model checker is always valid only the check case inputs are considered in the next section 5 3 3 Model Checking Process For model checking as described in section 3 3 the necessary components are converted to NuSMV language as described above the system model as a NuSMV module and system properties specified in the syntax of CTL and LTL After merging both components together in a text file manually NuSMV can be started with this file as input In this section the model checking process for the system function Play and Record a CD or Track is explained The NuSMV code from above sections are merged and saved in a text file rjb1 smv The complete file can be found in the appendix The main interaction mode of NuSMV is through an interactive shell In this mode the user can activate the various NUSMV computation steps as system commands with different op tions The interactive shell of NUSMV is activated from the system prompt as in Fig 17 system prompt gt NuSMV int rjbl smv lt RET gt NuSMV gt Fig 17 Starting NuSMV in interactive mode In interactive mode the model must first be rea
25. G green X green valid cry G redyellow X real valid cris G yellow X redyellow valid cris G redyellow gt X yellow valid crio G yellow X green valid Cri G redyellow X redyellowen valid Cru G vellowex gt X yellowen gt valid Coverage Driven Model Checking 24 4 5 Model Checking of Check Cases The system property of a check case is model checked and the result is compared with the expected check result of the check case Whenever model checking reveals an inconsistency an error is detected This can in turn be caused by an error in Ms Mspec or Spec These inconsistencies if any are the key factors of fault localization which is a straight forward process Check whether the inconsistency is caused by an error in Maa If the cause of the inconsistency is located in Msys an error in the developer s understanding of the system re quirements is revealed which must be corrected i e Msys is to be repaired Other sources of errors are the specification and Ms ec which are to be checked in the same way The manual model checking of Msys of the traffic light system is sketched in Table 5 including all properties based on Mspe and M see The results of the analysis of Table 5 are summarized as follows 4 of 20 check cases lead to inconsistencies in Msys Thus model checking detected all of the i
26. Hj Hj Hj Hj Hj Hj Hj Hj Hj Hj Hj Hj Mi Mi a aaa a a a a A A 00 0020 a a a a a a Q A H HH H bl ti b bl di b b di dl b b i ti SelectTrack ex Mode ex PlayTrack ex check all ex check none ex check on ex check off ex play ex pause ex record ex stop ex Track ex forward ex rewind ex track pos ex jump ex shuffle ex continue ex volume ex mute ex SelectTrack ex X SelectTrack en SelectTrack ex X Mode en SelectTrack ex X PlayTrack en Mode ex gt X SelectTrack en Mode ex X Mode en Mode ex X PlayTrack en PlayTrack ex X SelectTrack en PlayTrack ex Mode en PlayTrack ex PlayTrack en check all ex check all en check all ex check none en check on en P MM MM b check_all_ex gt check off en check none ex gt X check all en check none ex gt X check none en check none ex gt X check on en check none ex gt X lcheck off en check on ex gt check all en check on ex gt check none en check on ex gt check on en P P4 P4 S check on ex check all ex gt check off en check off ex X check all en Type CTL CTL CTL CTL CTL CTL CTL CTL CTL CTL CTL CTL CTL CTL CTL CTL CTL CTL CTL CTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL Status m rue m ru
27. LTL LTL LTL LTL LTL LTL LTL LTL LTL m rue m rue m rue m rue m rue False m rue m rue m rue m True False False True False True True False False True True True True True False False m rue False m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue N A N A N A N A N A N A N A N A N A T4 TS N A T6 N A N A N A N A Appendix D Model Checking Results of the generated Properties Nase 088 089 090 091 092 093 094 095 096 097 098 099 100 101 aaa QO a a a a a a a A Q shuffle ex shuffle ex continue ex continue ex continue ex continue ex volume ex volume ex volume ex volume ex mute ex mute ex mute ex gt mute ex gt gt P P4 P4 S X volume en X mute en X shuffle en X continue en X volume en X mute en X shuffle en X continue en X volume en X mute en shuffle en continue en volume en mute en LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL m rue m rue m rue m rue m rrue
28. Model Testing Combining Model Checking and Coverage Testing Diplomarbeit im Rahmen der Diplompr fung HII des Studiengangs Informatik DPO4 mit Nebenfach Elektrotechnik an der Universit t Paderborn Baris G ldali Matr Nr 6074300 Erstpriifer Prof Dr Ing Fevzi Belli Zweitpriifer Dr habil Reiko Heckel Erklarung Ich versichere dass ich diese Arbeit selbst ndig unter ausschlie licher Verwendung der angegebenen Literatur angefertigt habe Paderborn 09 05 2005 Ort Datum Unterschrift Abstract Abstract Combining software testing with model checking has several advantages There are a lot of approaches that combine these two techniques in a different manner This master thesis ex tends a new combined approach introduced in 8 and 9 that applies the specification based test case generation concept from 4 to model checking and proposes a concept for automa tion In this approach two models are assumed to be available a specification model that describes the user requirements on the system behavior and a system model that describes the actual system behavior The second model is model checked in order to verify the temporal logic properties generated from the specification model The automation concept includes the generation of the temporal logic properties and their verification using a model checker The thesis also describes how to apply the coverage based test termination criterion to model
29. TL property in 3 will hold only if v is not enabled at that normal state Note that an LTL property as given in 3 is not sufficient to guarantee the impossibility of the execution of the event v since Maa may not execute the event v at all in which case the property in 3 will hold vacuously Hence the property 1 is also required to guarantee the executability of v at least once Table 3 lists all complementary edge properties for the illegal event sequences generated from M spec of the traffic light system in Fig 7 Table 3 Complementary edge properties for the traffic light system Complementary Edge Properties G red gt X green G green X red G red gt X yellow G red gt X Tred en G green gt X redyellow G green gt X greene G redyellow gt X red G yellow gt X redyellow G redyellow gt X yellow n G vellow gt X green G redyellow X redyellowen G vellow gt X vellow n Coverage Driven Model Checking 23 4 4 Check Cases and their Generation The term check case emphasizes here the combination of the terms model checking and test case In analogy to a test case as introduced in chapter 2 the system property f is the input of the model checking in addition to the model to be checked whereby the expected output is specified as a binary value defined as follows Definitio
30. after the development validation and verification techniques are applied Validation entails determining if the im plemented system complies with the requirements and performs the functions for which it is intended It is traditional and is performed at the end of the development process Testing and simulation are examples of validation techniques Testing will be carried out by fest cases i e ordered pairs of test inputs and expected test outputs A test represents the execution of the system under consideration SUC using the previously constructed test cases If the outcome of the execution complies with the expected output the SUC succeeds the test otherwise it fails However the success or failure of a single test is not enough for any assessment on the correctness of the SUC because there can potentially be an infinite number of test cases even for very simple programs Therefore many strategies exist to compensate for these drawbacks Nevertheless the conceptual sim plicity of this very briefly sketched test process is apparently the reason for its popularity 8 Verification means using formal methods to check the compatibility of a system model with a formal specification of the user needs For verification the SUC does not need to be implemented completely The interim models of the SUC during the development process can be used for verification There are two kinds of verification techniques rule based deduc tive verificatio
31. ali A Holistic Approach to Test Driven Model Checking Proc of the 18th International Conference on Industrial amp Engineering Applications of Artificial Intelligence and Expert Systems IEA AIE 2005 ACM Press 2005 to appear 10 F Belli N Nissanke Ch J Budnik A Holistic Event Based Approach to Modeling Analysis and Testing of System Vulnerabilities TR 2004 7 Univ Paderborn 2004 11 B B rard et al System and Software Verification Model Checking Techniques and Tools Springer 2001 12 R V Binder Testing Object Oriented Systems Addison Wesley 2000 13 K Bogdanov et al Working together Formal Methods and Testing FORTEST landscapes document December 2003 14 J P Bowen et al FORTEST Formal Methods and Testing Proc of COMPSAC 02 IEEE Computer Society Press 2002 pp 91 101 15 J Callahan F Schneider S Easterbrook Automated Software Testing Using Model Checking Proc of the 1996 SPIN Workshop Rutgers University New Brunswick NJ 1996 pp 118 127 References 45 16 R Cavada A Cimatti E Olivetti M Pistore M Roveri NuSMV 2 1 User Manual Technical report Istituto Trentino di Cultura Centro per la ricerca scientifica e tec nologica Trento Italy 2002 http nusmv irst itc it NuSMV 17 T S Chow Testing Software Designed Modeled by Finite State Machines IEEE Trans Softw Eng 1978 pp 178 187 18 A Cimatti et
32. an important issue in software testing because the tester has to know when to stop testing the SUC As mentioned earlier a system can not be tested completely so an adequacy criterion is needed to determine the end of the test process Similarly in model checking the completeness of the verified properties must be considered in order to stop the verification step Completeness in this context is defined as a complete set of system properties specified by a formal specification model As mentioned in earlier sections the approach considers an event based system where the system environment interactions are specified with an ESG The nodes of the ESG represent the events or the actions that trigger the events For testing purposes each action specified with a node in ESG should be checked for executability If it will never be executed an unconformity is detected Two nodes of the ESG connected with an edge represent an event sequence For testing purposes a legal event sequence requires that the action referring to the second event should be executable just after executing the action referring to the first event If this is not the case an unconformity is detected Complementing the ESG produces new edges which are not included in the original ESG The edges of the complemented graph represent the illegal event sequences of the system interaction For testing purposes an illegal event sequence requires that the action referring to the second event
33. ay_ex gt X record_en LTL False T3 048 G play ex X stop en LTL True N A 049 G play ex gt X Track en LTL True N A Fig 20 The output ofthe snow property command after the verification The properties with identifier numbers 0 1 48 and 49 are verified to be true On the other hand the property with the identifier number 47 is verified to be false and a counterexample trace with the number 3 is generated This complete error trace can be shown and analyzed by the command show traces In this case the error trace with the number three T3 shows that the property 47 does not hold on the system model of RJB because after state s in which play is executed record is enabled at the next state playing which as seen from to the specification model should not be the case 5 4 Results If all properties generated in section 5 3 2 are considered 11 properties are verified to be false Thus the model checking detected some unconformities between the specification model and the system model The command show property executed with the option shows the properties verified to be false see Fig 21 An excerpt of the faults detected in 10 is given in Table 9 The unconformities detected by model checking in this section indicate some of these faults and also some further faults e The property 59 specifies that globally if there exists a state where event record is executed then the pseudo event Track should no
34. because the tester can observe the system in operation and in this way justify to what extent his her requirements have been met Although testing is not comprehensive enough to detect all errors it can help to increase confidence in the software by determining the number of errors against the tested portion of the software Testing is a cost intensive process because it is mainly based on the intuition and experience of the tester which cannot always be sup ported by existing test tools 8 Many formal methods have been proposed to avoid the drawbacks of testing Model checking is such a method in which the software system as a finite model is restricted to a specific domain of interest and checked against a logic specification automatically For many years model checking has been successfully applied to a wide variety of practical problems including hardware design protocol analysis operating systems reactive system analysis fault tolerance and security This formal method primarily uses graph theory and automata theory to verify user specified properties on the system model The combination of model checking with software testing is proposed in many works 9 This thesis extends and automates a new approach introduced in 8 and 9 that combines these two techniques by applying the specification oriented testing concepts to model check ing Thus the approach combines the advantages of testing and model checking assuming the availabilit
35. continue en volume en mute en LTLSPEC G rewind ex X forward en LTLSPEC G shuffle ex X shuffle en LTLSPEC G rewind ex X rewind en LTLSPEC G shuffle ex X continue en LTLSPEC G rewind ex X track pos en LTLSPEC G shuffle ex X volume en LTLSPEC G rewind ex X jump en LTLSPEC G shuffle ex X mute en LTLSPEC G track pos ex X forward en LTLSPEC G continue ex X shuffle en LTLSPEC G track pos ex X rewind en LTLSPEC G continue ex X continue en LTLSPEC G track pos ex X LTLSPEC G continue ex X volume en track pos en LTLSPEC G continue ex X mute en LTLSPEC G track pos ex X jump en LTLSPEC G volume ex X shuffle en LTLSPEC G jump ex X forward en LTLSPEC G volume ex X continue en LTLSPEC G jump ex X rewind en LTLSPEC G volume ex X volume en LTLSPEC G jump ex X track pos en LTLSPEC G volume ex X mute en LTLSPEC G jump ex X jump en LTLSPEC G mute ex gt shuffle en Node Property SPEC EF shuffle ex SPEC EF continue ex SPEC EF volume ex LTLSPEC LTLSPEC LTLSPEC 2 X G mute_ex gt X G mute_ex gt X X G mute_ex gt continue en volume en mute en Appendix D Model Checking Results of the generated Properties ic Appendix D Model Checking Results of the generated Properties PROPERTY LIST 000 001 002 003 004 005 006 007 EF Hj Hj Hj Hj tj
36. ctivities is pushed back in the software development process by using model checking In other words the purpose of testing is carried out on the system model by using model checking Modelling the Specification Fig 2 Overall structure of the approach using the design model T Informal Specification Modelling the Specification Y Generating Moyet Mano System Properties N N N NS x N Fig 3 Overall structure of the approach using the behavioral model Coverage Driven Model Checking I6 Fig 3 assumes that the user of the approach has no access to the development process so the SUC is a black box for the user The only functional description is the user manual of the SUC In this case two independent activities take place firstly by means of the black box SUC an abstract behavioral model Mga is generated which will be called Msys Secondly from the informal specification a formal specification model is generated from which the system properties are extracted The later step is similar to the one in Fig 2 The general approach introduced above will be applied in this thesis on a specific case where for an event based application system properties are generated from event sequences specified by Mspe and M spec Each event sequence is interpreted as a test input of a test case Whether the event sequence is legal or illegal the test output is defined as executable or not executable Fr
37. cture given by a quadruple X S So R L defined over a set of atomic propositions AP AP includes two atomic proposi tions Ven and Vey for each event v Vspece semantically corresponding to v is enabled and v is executed respectively The set of states S of the Kripke structure will be labeled with these atomic propositions signifying that whether the event v is enabled or executed at that state In Coverage Driven Model Checking 17 order to differentiate between states where events are enabled or executed S is divided into two sets of states Sys and Srs standing for normal states and transition states respectively For any state s Ssys there is a corresponding normal state s e Sys Furthermore for any two states s and s Ss if it is possible to execute an event v Asys at s and execution of v at s results in a state transition to s i e if Rsyst s v s e Ssys then i there is a transition state svs e Srs ii s vs ER ili vs s ER IV Ven L s and V Vex LGv S R and L include no elements other than the ones given above Finally So includes the normal states corresponding to the initial states Ssyso This thesis assumes a correct conversion from Ms s into a Kripke structure where the conversion itself could be a source of error for the verification step 4 2 Example Traffic Light System This section introduces a small example traffic light system taken from
38. d This happens with command go This command reads and initializes the system for verification It is equivalent to the NuSMV command sequence read model flatten hierarchy encode variables build model build flat model build boolean model 16 These commands read the input file and convert the module into an efficient data structure for further verification The properties are extracted from the input file and stored in an internal property list This list of properties can be shown by the command show property For every property the following information is displayed e the identifier of the property a progressive number Case Study and Tool Support 38 e the property formula e the type CTL LTL e the status of the formula Unchecked True False e the number of the corresponding counterexample trace if the formula has been verified to be false Otherwise this field is marked with N A Not Applicable Some of the 101 properties in rjb1 smv are listed by show_property as in Fig 18 NuSMV gt show_property PROPERTY LIST Type Status Counterex Trace PROPERTY LIST 000 EF SelectTrack ex CTL Unchecked N A 001 EF Mode ex CTL Unchecked N A 047 G play ex gt X record_en LTL Unchecked N A 048 G play ex gt X stop en LTL Unchecked N A 049 G play ex gt X Track en LTL Unchecked N A Fig 18 The output of the
39. d in each state A Kripke structure is formally defined as follows 20 Preliminaries 11 Definition 3 Let AP be a set of atomic propositions a Kripke structure K over AP is a quadruple K S So R L where S is a finite set of states So c S is the set of initial states R c SxS is a transition relation such that for every state s e there is a state s e S in that R s s and L 2 is a function that labels each state with the set of atomic propositions that are true in that state 20 A state of a Kripke structure is a snapshot or instantaneous description of the system that capture the values of the variables at a particular point in time There is also the need to know how the state of a system changes as a result of some action of the system or user The changes in the state can be defined by giving the state before the action occurs and the state after the action occurs Such a pair of states determines a transition of the system The com putations of the system can be defined in term of its transitions So the Kripke structure de fines a state transition system 25 3 3 2 Temporal Logic Temporal logic is a formalism for describing sequences of transitions between states in a reactive system and is traditionally interpreted in terms of Kripke structures Reactive systems need to interact with their environment frequently and often do not terminate The behavior of a reactive system emerges when the system responses to
40. del checking the Kripke structure must be translated into a formalism that is ac cepted by the selected model checking tool In this case study the model checker NuSMV is selected for many reasons which are addressed in the next section NuSMV accepts the Kripke structure in the form of a abeled transition system which is also explained in the next section 5 3 Tool Support Using the specification model and the system model the generation and verification of the system properties using tool support can begin For tool deployment both models must be converted into a machine readable format As explained in section 5 1 the specification model is saved in plain text files which include the adjacency matrix representations of the ESG s The system model will be translated into a labeled transition system and also saved in plain text A small Java application given in Appendix B generates system properties from the specification model Both the transition system and the system properties are merged in an additional text file which will be the input for the model checker NuSMV NuSMV 18 is a symbolic model checker which originates from the reengineering reim plementation and extension of SMV the original BDD based model checker developed at CMU 26 NuSMV is able to process files written in an extension of the SMV language In this language it is possible to describe labeled transition systems by means of declaration and instantiation mecha
41. e m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue m rue False m rue m rue m rue m rue False m rue m rue m rue m rue m rue Trace N A N A N A N A N A N A N A N A N A N A N A N A N A N A N A N A N A N A N A N A N A N A T1 N A N A N A N A T2 N A N A N A N A N A Appendix D Model Checking Results of the generated Properties 62 042 043 044 045 046 047 048 049 050 051 052 053 054 055 056 057 058 059 060 061 062 063 064 065 066 067 068 069 070 071 072 073 074 075 076 077 078 079 080 081 082 083 084 085 086 087 aaa a a a A a a a a a a a a a a a MA a a a A A A a A A A a a a A A a a a A A a A a a HA A check_off_ex gt check_off_ex gt check_off_ex gt play_ex gt X play ex gt Xp play ex gt X play ex gt Xs play ex gt XT pause ex gt X pause ex gt X pause ex gt X pause ex gt X pause ex gt X record ex gt X record ex gt X record ex gt X record ex
42. e model checking step effectively performs a testing activity on Maer Additionally the approach systematizes the model checking process and handles the completeness problem of the checked properties with respect to the specification based test adequacy criterion known for long in testing community It is important to notice that this approach involves no testing activity in a classical manner because the SUC is not tested directly The concepts of testing are applied to model checking Fig 2 and Fig 3 show different aspects and the structure of the approach which are illus trated as UML Activity diagrams 27 including control flow solid lines for activities and data flow dashed lines for the inputs outputs of the activities The approach described in Fig 2 assumes that the user of the approach has access to the Mbpsgn during the development process as an output of the design phase which will be called Msys Firstly the requirements on the SUC are defined the outcome is the informal specifica tion Spec After analyzing the requirements the development process forks into two phases During the SUC is designed from the formalized specification Mspec and its complement M spec System properties are generated that will be checked on Maer If model checking shows unconformities then either the design process should be repeated or the requirements should Coverage Driven Model Checking 15 be checked Thus the start of the testing a
43. el ESG RJBI eee 29 Table 8 Specification file of the sub level ESG Play Track eene 29 Table 9 Detected faults for the system function Play and Record a CD or Track 40 References 44 References 1 P Ammann P E Black W Ding Model Checkers in Software Testing NIST IR 6777 National Institute of Standards and Technology 2002 P Ammann P E Black W Majurski Using Model Checking to Generate Tests from Specifications ICFEM 1998 pp 46 54 B Beizer Software Testing Techniques Van Nostrand Reinhold 1990 F Belli Finite State Testing and Analysis of Graphical User Interfaces Proc of 12th ISSRE IEEE Computer Society Press 2001 pp 34 43 F Belli Ch J Budnik Minimal Spanning Set for Coverage Testing of Interactive Sys tems Proc of ICTAC 2004 LNCS 3407 Springer 2004 pp 220 234 F Belli Ch J Budnik Towards Minimization of Test Sets for Coverage Testing of Inter active Systems LNI Software Engineering 2005 GI Essen Germany 2005 pp 79 90 F Belli Ch J Budnik N Nissanke Finite State Modeling Analysis and Testing of Sys tem Vulnerabilities ARCS Workshops 2004 pp 19 33 F Belli B G ldali Software Testing via Model Checking Proc of the 19 International Symposium on Computer and Information Sciences Kemer Antalya Turkey 2004 vol 3280 of LNCS Springer pp 907 916 F Belli B G ld
44. ende System out println 4 modulName s idx kopf idx ende 1 for int i 0 i lt dimension i idx ende zeile indexof idx ende41 eventArray i zeile substring idx kopf idx ende System out print eventArray i w idx_kopf idx ende 1 System out println br close catch FileNotFoundException e System out println File not found g Filename catch IOException e System out println File g Filename can not be read finally return The method fillAdjacencyMatrix extracts from the rest of the specification file the entries of the adjacency matrix The entries are sperated with semicolons For each row the corresponding line is parsed the event names are extracted and saved in the matrix eparam s Filename The complete path of the specification file return no return value public void fillAdjacencyMatrix String s Filename try String zeile BufferedReader br int idx kop idx ende fill the matrix for each entry br new BufferedReader new FileReader s Filename for int j 0 j lt dimension j System out print eventArray j zeile br readLine idx kopf 0 idx ende 0 for int i 0 i lt dimension i idx ende zeile indexOf idx_ende 1 adjacencyMatrix j i zeile substring idx_kopf idx ende equalsIgnoreCase 1 System out print adjacencyMatrix j il idx kopf idx ende 1 System o
45. erators The path quantifiers are used to describe the branching structure in the computation tree There are two such quantifiers A for all computation paths and E for some computation paths These quantifiers are used in a particular state to specify that all of the paths or some of the paths starting at that state have a specific property The temporal operators describe properties of a path through the tree There are five basic operators 20 X neXt requires that a property holds in the next state of the path F Future is used to assert that a property will hold at some state on the path G Global specifies that a property holds at every state on the path U Until holds if there is a state on the path where the second property holds and the first property holds at every preceding state on the path R Release is the logical dual of U It requires that the second property holds along the path up to and including the first state where the first property holds However the first property is not required to hold eventually Path formulas define properties for computation paths of the Kripke structure In order to define some property for a state using path formula path quantifiers are deployed If fis a path formula Ef is a state formula This formula is valid for a state s if there is a path 7 be ginning from s where fis valid Similarly Af is also a state formula saying that on all paths beginning from s
46. events generated by its environment 20 In the temporal logic considered here time is not mentioned explicitly instead a formula might specify that eventually some property holds or that some property never holds Proper ties like eventually or never are specified using temporal operators These operators can also be combined with boolean connectives or nested arbitrarily Temporal logics differ in the op erators that they provide and the semantics of those operators 20 Temporal logic can describe the order of events in time which is expressed by means of state transitions Each transition represents a time unit This is also called discrete time scale Temporal logics are often classified according to whether time is assumed to have a linear or a branching structure Temporal logic formulas can be interpreted over a state transition sys tem e g Kripke structure 20 Computation tree logic CTL formulas describe the properties of computation trees of state transition systems The tree is formed by choosing a state of the transition system as the initial state and then unwinding the structure into an infinite tree with the designated state at the root The computation tree shows all the possible executions of a system starting from the Preliminaries 12 initial state A path x is an infinite sequence of states n sos s2 in the computation tree 20 In CTL the formulas are composed of path quantifiers and temporal op
47. eyword SPEC The node properties generated for sub level ESG Play Track are listed in Fig 14 An edge property is generated for each entry of the adjacency matrix The edge properties are LTL formulas in the form G vx X vol for legal edges represented by 1 and in the form G ve gt X ven for illegal edges represented by 0 in the adjacency matrix as ex Case Study and Tool Support 36 plained in section 4 3 2 An edge property in LTL for a legal edge is defined in NuSMV lan guage as follows LTLSPEC G play_ex gt X pause_en This property specifies that globally if there exists a state in which the event play is executed then the event pause must be enabled at the next state Similarly an illegal edge property in LTL is defined as fol lows LTLSPEC G play ex gt X record en where stands for negation This property specifies that globally if there exists a state where event play is executed then the event record should not be enabled at the next state The LTL properties are introduced by the keyword LTLSPEC Some other edge properties generated for sub level ESG Play Track are listed in Fig 15 A complete list ofthe generated properties can be found in the appendix Node Properties SPEC EF plav ex SPEC EF pause ex SPEC EF record ex SPEC EF stop ex SPEC EF Track ex Fig 14 Node properties for ESG Plav Track Edge Properties LTLSPEC G play ex X
48. f en boolean play ex boolean play en boolean pause ex boolean pause en boolean record ex boolean record en boolean stop ex boolean stop en boolean forward ex boolean forward en boolean rewind ex boolean rewind en boolean track pos ex boolean track pos en boolean jump ex boolean jump en boolean shuffle ex boolean shuffle en boolean continue ex boolean continue en boolean volume ex boolean volume en boolean mute ex boolean mute en boolean stopped playing paused ASSIGN init state stopped init play_en Eug init pause en 0 init record en 1 init stop_en 0 init play_ex 0 init pause_ex 0 init record_ex 0 init stop_ex 0 init check all ex 0 init check all en 1 init check none ex 0 init check none en 1 init check on ex 0 init check on en E init check off ex 0 init check off en 1 init forward ex 0 init forward en 1 init rewind ex 0 init rewind en 1 init track pos ex 0 init track pos en 1 init jump ex 0 init jump en 1 init shuffle ex 0 init shuffle en 1 init continue ex 0 init continue en 1 init volume ex 0 init volume en zx init mute ex 0 init mute_en 1 next state case state stopped sl s8 s11 state sl state s4 state S12 playing state playing s2 s3 s10 s1
49. f the SUC has to be modeled Modeling the system behavior can be considered in two ways Firstly a modeler can produce an abstraction of the desired system functions in the design phase of a development process which the developer will then use as guidance to produce the end product the SUC This kind of model will be called a design model Mpsgn Secondly the behavior of an existing system can be analyzed and described as a behavioral model Mgr Mn is constructed from the view of the user in several steps incrementally in creasing his her intuitive cognition of the SUC usually by experimenting without any primary knowledge about its structure In this thesis an intuitive way of the construction of Man has been considered Proposals also exist however for automating the model construction e g in 30 applying learning theory Taking these proposals into account would further rational ize the approach however it is not in the scope of this thesis In both cases Msys will be modeled as a finite state machine 23 Definition 2 A finite state machine FSM is a quadruple S So A R where Sisaset of states So isa set of start states where So ES Ais an input alphabet Risa transition relation that maps an input symbol a e 4 and a current state s e S to a next states S i e R s a e S Preliminaries 8 Since the approach introduced in this thesis uses model checking as the verification method Ms s will
50. fication files of all ESG s can be found in Appendix A Table 8 Specification file of the sub level ESG Play Track PlayTrack play pause record stop Track Ove des Ose dos 1 0 0 1 1 150 071503 1 0 1 0 1 1 1 1 1 Case Study and Tool Support 30 5 2 System Model As we have no insight into the development process of the commercial software RJB a be havioral model Msn will be used as system model Ms s instead of Mpsgn thus the approach is applicable in the form as illustrated and explained in Fig 3 and in section 4 respectively Msyst will be produced by observing the functional behavior and the changes in the structure of RJB The construction of Ms s for RJB can be explained as follows Firstly by playing with RJB some system states are identified These are the initial state the playing state the paused state the recording state and the stopped state Because the initial state has the same appear ance as the stopped state which is reached if some function is canceled via stop button both states are merged into the stopped state Secondly the state changes are analyzed by clicking the buttons of the GUI which leads to a FSM like in Fig 10 This system model observes only the system states and the system events relating to the system function Play and Record a CD or Track The transitions are labeled with the corresponding names of the buttons that trigger the events and cau
51. g this section in an effective manner Even if additional effort is needed for the holistic view by testing the unspecified system interaction the test engineer creates more confidence in the SUC 3 3 Model Checking Model checking consists of three main steps 20 1 Modeling The system model to be verified must be converted to a formalism accepted by a model checking tool The model can abstract the details that do not affect the correctness of the checked properties 2 Specification The properties that the system model must satisfy should be stated An important point to consider is the completeness That means verifying a single property does not cover all the properties that the system should satisfy 3 Verification This step is executed automatically by the model checker The outcomes of the two preceding steps are given to the model checker as input The result of the verifica tion step shows either that the model satisfies the property or that the model does not sat isfy the property in which case further investigations are required 3 3 1 Kripke Structure Model checking uses a type of state transition graph called a Kripke structure to model a system A Kripke structure is basically a graph consisting of nodes representing the reachable states of the system and edges representing the state transitions of the system It also contains a labeling of the states of the system with properties called atomic propositions that hol
52. gt X record ex gt X stop ex gt p I T stop_ex gt stop_ex gt stop_ex gt P P4 KOM S stop ex Track ex Track ex Track ex Track ex P P4 P4 P4 S Track ex forward ex forward ex forward ex forward ex rewind ex X rewind ex X rewind ex X rewind ex X track pos ex track pos ex gt track pos ex track pos ex jump ex gt Xf jump ex gt Xr jump ex gt Xt jump ex gt Xj shuffle ex shuffle ex X check none en X check on en X check off en play en ause en record_en top_en rack_en play_en pause_en record en stop_en Track_en play_en pause_en record en stop_en Track_en lay_en pause en ecord en Istop en rack en play en pause en record en stop en Track en X forward en X rewind en X track pos en X jump en forward en rewind en track pos en jump en X forward en X rewind en X track pos en X jump en orward en ewind en rack pos en ump en X shuffle en X continue en LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL LTL
53. hability properties safety properties and liveness properties Reachability properties define system properties saying that some state of the system with a desired prop erty is reachable Reachability properties can be formulated using E path quantifier in CTL A reachability property holds if there is some execution of a system including a state where the property holds Liveness properties assure that a system executes as expected or that something good will eventually happen Safety properties on the other hand ensure that the system does not enter an undesired state or that something bad will not happen 11 3 3 3 Model Checker A model checker explores the reachable state space of the model specified as a Kripke structure and verifies whether the expected system properties specified as temporal logic formulae are satisfied over each possible path If a property is not satisfied the model checker answers with invalid and generates a counterexample in the form of a sequence of states called a trace 1 20 Counterexamples can be used to localize the error by tracking down the trace until the state where the error occurs Analyzing the error trace may require an adaptation of the model and a re verification Another reason for error can also be an incorrect modeling of the system or an incorrect specification false negative 20 In each case further modifications on the model or on the specification are required
54. have to be converted into a Kripke structure see section 3 3 1 Conversion from the actual formalism into Kripke structure will be explained in section 4 1 3 2 Specification Based Testing Specification based testing refers to the process of testing a program based on what its specification savs its behavior should be In particular test cases can be developed based on the specification of the program s behavior without having an implementation of the program black box testing Furthermore test cases can be developed before the program even exists There is also another type of testing implementation oriented testing where the source code of the software is taken into account bv generating test cases white box testing There are two main roles a specification can plav in software testing 32 The first is to provide the necessarv information to check whether the observed behavior of the program is correct Checking the correctness of program behavior is known as the oracle problem The second is to provide information to select test cases and to measure test adequacy This sec tion focuses on both aspects of using a specification for generating test cases 3 2 1 Test Case Generation It makes sense to construct test cases in compliance with the tester s expectations of how the system should behave during the early stages of the integrated software development process long before the implementation begins The generated te
55. he events in the eventArray zls lt li gt DEFINE lt i gt module lt i gt ex lt i gt eventl lt i gt ex lt i gt event2 lt i gt ex lt li gt DEFINE lt i gt module lt i gt en lt i gt eventl lt i gt en lt i gt event2 lt i gt en 1 lt p gt Secondly the node properties for each event in the event array is generated lt l gt lt li gt SPEC EF lt i gt eventl lt i gt ex lt 1 gt lt p gt Finally the edge properties for each entry of the adjacency matrix is generated If the entry amp lt lt i gt eventl lt i gt lt i gt event2 lt i gt amp gt is a 1 then a property in the following form is generated 1 Appendix B Property Generation Tool li LTLSPEC G lt i gt eventl lt i gt ex gt X lt i gt event2 lt i gt ex c 1 Otherwise a property in the following form is generated 1 lt li gt LTLSPEC G lt i gt eventl lt i gt ex X lt i gt event2 lt i gt ex 1 Gparam s Filename The complete path of the specification file return no return value public void outputProperties String s Filename try String zeile BufferedReader br int idx_kopf idx_ende create DEFINE declerations BufferedWriter bw bw new BufferedWriter new FileWriter s Filename 1t1 bw newLine bw write DEFINE declerations bw write DEFINE modulName ex for int i 0 i lt dimension i bw write eventArray i
56. he normal system states or sl s14 to represent the transition states see section 3 1 2 The assignment init state sets the initial value of the variable state to stopped Case Study and Tool Support 34 The transition relation of the Kripke structure is expressed by using the next assign ment which defines the value of variables in the next state i e after each transition given the value of the variables in the current states i e before the transition The case segment sets the next value of the variable state to any value in the set s1 s8 s11 if its current value is stopped If the current state is any of s1 s4 or s12 where stands for the boolean operator OR then the next value of the state variable is set to playing Other wise the last assignment of the case segment sets the value of the state variable to its current value so it remains unchanged Besides the state variable representing the system state other variables representing the atomic propositions to label the system states are needed see section 4 1 The variables play en and play ex in Fig 13 are defined to be of type boolean This means that they can assume the integer values 1 set and 0 unset At the initial state stopped the variable play_en is set and play_ex is unset The case segment implementing the transition relation shows how the value of the variable play_en changes If the current state is any of 82 83 85 811 or s13 the
57. he system properties is realized with a small application The generated system properties are model checked in a batch process reporting the verification results A case study has shown the applicability of the approach to non trivial systems Apart from making use of tools there is also potential for a more efficient application of the approach in practice Automatically converting the system model to a formalism accepted by the model checking tool merging of the code for system properties and for the system model and starting the model checking process Also a report generator would enable the production of meaningful and compact reports To keep the examples simple relatively short event se quences have been chosen checking with longer sequences would increase the likelihood of revealing more sophisticated faults Figure Index 42 Figure Index Fig 1 Simplified process of software development ec 5 Fig 2 Overall structure of the approach using the design model 15 Fig 3 Overall structure of the approach using the behavioral model 15 Fig 4 Traffic light system specification as an ESO 18 Fig 5 A faulty Msg asa ESM coesa rs ik ii i ea ki aia aa an 18 Fig 6 Kripke structure Tor Msyst of Fig 3 sa OU 18 Fig 7 Complementing with dashed lines of the Mspec from Fig A L 22 Fig 8 Top menu of the RealJukebox ORID nennen 26 Fig 9 Mspec for the system function Play and Record a CD
58. imension br close return dimension catch FileNotFoundException e System out printin File not found s Filename catch IOException e System out println File s Filename can not be read finally return dimension The method generateMatrix creates a two dimensional quadratic matrix and an array for the event names return no return value public void generateMatrix create a two dimensional matrix in the size of events adjacencyMatrix new boolean dimension dimension create an array for event names eventArray new String dimension The method fillEventArray extracts from the first line of the specification file the modul name and the event names The modul name is the first element of the semicolon seperated title line The event names are also sperated with semicolons The line is parsed and the event names are extracted and saved in the array param s Filename The complete path of the specification file return no return value public void fillEventArray String s Filename try String zeile BufferedReader br int idx_kopf idx_ende extract modul name extract event names br new BufferedReader new FileReader s Filename zeile br readLine idx kopf 0 idx ende 0 Appendix B Property Generation Tool 52 idx ende zeile indexOf idx ende 1 modulName zeile substring idx kopf idx
59. ion 0 xx x The adjacencyMatrix in that the specification files entries are stored x Each entry indicates an existing or non existing edge between two events in the x specification file public boolean adjacencyMatrix xx x The eventArray stores the event names given in the first line of each x specification file ST public String eventArray xx x The modulName is extracted from first line of each specification file Appendix B Property Generation Tool 50 public String modulName xx x The constructer gets the directory where the specification files are located x and an array in which the names of the specification files are stored These x are saved in local attributes x param directory The directory where the specification files are located The output files will also be saved in this directory param specificationFiles An array containing the names of the specification files ST public PropertyGenerator String directory String specificationFiles this directory directory this specificationFiles specificationFiles The method generatePropertyList is the driver method for code generation It creates the complete path of a specification file and extracts the dimension of the adjacency matix Using the dimension information the adjacency matrix and an array for event names are generated After filling these variables with values the code gene
60. is Black Box Checking Journal of Automata Lan guages and Combinatorics 2002 pp 225 246 31 M Y Vardi P Wolper An automata theoric approach to automatic program verifica tion Proc of 1st IEEE Symp Logic in Computer Science LICS 86 IEEE Comp Soc Press 1986 pp 332 244 32 H Zhu P A V Hall J H R May Software Unit Test Coverage and Adequacy ACM Comp Surveys 1997 pp 366 427 Acknowledgments 46 Acknowledgments I would like to thank the people who helped me to write this master thesis trough valuable discussions and comments Fevzi Belli Reiko Heckel H sn Yenig n Ekkart Kindler Muffy Calder Ina Schieferdecker Aditya Mathur Christof Budnik Leonardo de Moura Martin Hirsch Daniela Schilling Laura White Appendix A Specification Files of ESG s LAF 2 Appendix A Specification Files of ESG s esgl txt RJB1 SelectTrack Mode PlayTrack qus IS E ds als 12175175 esg2 txt SelectTrack check all check none check on check off 1 1 0 1 lol E OF lade belo 1 1 1 1 esg3 txt PlayTrack play pause record stop Track Os Os Ty lis 17505058515 1505051505 Iso Lee le eg Le E esg4 txt Track forward rewind track pos jump dismal sese ales less p l rlo dotados AN EC Kex Lajo esg5 txt Mode shuffle continue volume mute Ak e Leds sd lte Io despues i Er Appendix B Pro
61. l ex if i dimension 1 bw write ni else bw write bw newLine bw write DEFINE modulName en for int i 0 i lt dimension i bw write eventArray il en if i dimension 1 bw write ni else bw write bw newLine bw write Node Properties bw newLine for int i 0 i lt dimension i bw write SPEC EF eventArray i _ex bw newLine bw write Edge Properties bw newLine for int j 0 j lt dimension j for int i 0 i lt dimension i if adjacencyMatrix j i bw write LTLSPEC G eventArray j _ex gt X bw write eventArray i _en bw newLine else bw write LTLSPEC G eventArray j _ex gt X I bw write eventArray i w en Appendix B Property Generation Tool 55 bw newLine bw close catch FileNotFoundException e System out printin File not found s Filename catch IOException e System out println File s Filename can not be edited finally return Appendix C Complete NUSMV Code of RJB Module 56 Appendix C Complete NUSMV Code of RJB Module MODULE main VAR state recording sl s2 s3 s4 s5 S7 S8 s9 S10 S11 S12 s13 check all ex boolean check all en boolean check none ex boolean check none en boolean check on ex boolean check on en boolean check off ex boolean check of
62. m rue m rue m rue m rue m rue m rue m rue m rue m rue N A N A N A N A N A N A N A N A N A N A N A N A N A N A Appendix E Content of the attached CD 64 Appendix E Content of the attached CD CD 1 MasterThesis this directory contains the thesis in digital form __Cover pdf _ Subject pdf Thesis pdf esgi txt esg2 txt esg3 txt esg4 txt esg5 txt doc Documentation of PropertyGenerationTool produced by javadoc propgen __GeneratePropertyApp html __package frame html _ package summary html _ package tree html PropertyGenerator html __PropertyGeneratorApp html resources inherit gif _ allclasses frame html _ allclasses noframe html constant values html _ deprecated list html __GeneratePropertyApp html help doc html index html index all html overview tree html _ packages html stvlesheet css src Source code of PropertyGenerationTool propgen PropertyGenerator class PropertyGeneratorApp class PropertyGenerator java PropertyGeneratorApp java run bat Script for running the PropertyGenerationTool 4 NuSMV zchaff 2 2 2 i1686 pc mingw32 Installation of NUSMV 5 RJB rjbi smv NUSMV representation of the Kripke structure in Fig 11 including the system properties generated by PropertyGenerationTool Readme txt
63. n 6 A temporal logic formula f as a property of a Kripke structure K is valid if K satisfies the property f Otherwise fis invalid Check results CR valid invalid is a set containing both the values a property f can get if model checked on K Definition 6 enables the presentation of test cases as a combination of a temporal logic for mula and a binary value as given in the following definition Definition 7 A check case is an ordered pair f cr where f is a system property based on a node property or an edge property of Mspec or a complementary edge property of M spec and cr e CR is a check result From the system properties generated for the traffic light system in sections 4 3 1 4 3 3 the check cases in Table 4 can be generated Table 4 Check cases generated from the system properties of the traffic light system Node Properties Edge Properties cr EF redex valid crs G reda X redyellow valid cr EF redyellow valid cre G redyellow gt X green valid cr EF greens valid cr EF yellow valid cr G green X yellowen valid cr G yellows gt X reden o valid Complementary Edge Properties cro G redex gt X green valid cris G green X red valid crio G red gt X yellow valid crie G green gt X redyellow valid cri G red gt X reden valid cri
64. n and model based verification 25 Model checking is a model based technique for the verification of finite state concurrent systems 20 it can also be used for the verification of non concurrent finite state systems In the case of concurrent systems the main challenge is dealing with the huge number of states state space explosion problem This problem occurs in systems which have many compo nents that can interact with each other or systems that have data structures that can be as signed many different values For non concurrent systems with low complexity the state space explosion problem can be handled easily if the number of states is controllable and if data structures are selected properly Because of the popularity of testing the combination of formal methods and test methods has been widely accepted in both communities 14 15 28 30 Model checking belongs to the most promising candidates for this combination Combining model checking and testing has already been proposed for Formal Methods for Software Validation and their Combination Related Work 4 i generating test cases to be applied on the SUC based on the properties used in model checking 2 21 22 ii model checking of the system model using test traces produced during white box testing of the SUC as properties 15 iii guarantying intermediate errors to propagate to the output by using model checking 28 iv applying model checking directly
65. n the variable play en is set at the next state otherwise it is un set The transition relation of a variable can also be coupled with the transition relation of an other variable the variable play_ex will be set as next ifthe variable state changes from the current state to either of the transition states s1 or s4 The complete code of the modules can be found in the appendix MODULE main represents the system model E T next play_en case while playing and recording a state s2 state s3 CD or Track state s5 state s11 VAR state s13 1 Es bool Abs ay ex boolean P ay_ esac play_en boolean m next play ex case ASSIGN RN j i next state s1 ini ay en 1 S play next state s4 init play ex 0 1 0 esac Fig 13 Declarations of atomic propositions initial state assignment transition relation Case Study and Tool Support 35 5 3 2 Property Generation Tool The specifications to be checked on the system model can be expressed by NuSMV in two different temporal logics CTL and LTL CTL and LTL specifications are evaluated by NuSMV to determine their truth or falsity in the system model When a specification is dis covered to be false NUSMV constructs and prints a counterexample i e a trace of the model that falsifies the property 18 The property generation tool is a small application implemented in Java which processes specification file
66. n these complementary edges from E Loser These additional system properties are used to get a full coverage of the properties based on both the requirements incorporated by original edges and anti requirements incorporated by complementary edges thus leading to a completeness of model checking with respect to the given specification model The complementary edge properties can be seen as safety properties which specify that after the first event of an event sequence is executed the second Coverage Driven Model Checking 22 event should not be enabled This section explains how complementary edge properties are generated from M spec In Fig 7 the graphical view of the superposition of Mspe and M spec is given which obvi ously is a complete graph with the set of nodes Vs ec The dashed lines belong to E spec repre senting the illegal event sequences Fig 7 Complementing with dashed lines of the Ms from Fig 4 For complementary edge coverage for each edge v v e E spec it is required that the event v should not be enabled right after the execution of the event v which can be specified by using the complementary edge property in LTL G Ver gt X vu 3 The complementary edge property is valid on the states of Maa where v is executed and at all consecutive states v is not enabled As from a transition state at which vex holds there is only one outgoing transition and it ends at a normal state the L
67. nd or extend the test suite to continue testing which is called the test termination problem 4 The approach in 4 which will be applied to model checking in this thesis favors an ade quacy criterion based on specification coverage in order to handle the test termination prob lem The test process can stop if all possible scenarios given by the specification are tested on the SUC 3 2 3 Holistic View A short motivation for also considering the forbidden scenarios for testing and modeling them is already made in section 3 1 1 This complementary view of the requirements specifi Preliminaries 10 cation is called the holistic view and is introduced in 4 It helps to differentiate between de sired and undesired system behavior The holistic approach to specification based construction of test suites proposes the gen eration of all possible test cases that cover both the specified and not specified properties of the system regardless of whether they are desirable or undesirable As explained in section 3 1 1 the desirable behavior of the system is specified by Mspec and the undesirable behavior of the system is specified by M spec The holistic view helps to clearly differentiate the correct system reaction from the faulty one as the test cases based on Mspec are to succeed the test and the ones based on M spec are to fail when applied on the SUC Thus the approach handles the oracle problem introduced at the beginnin
68. next state sil next state 12 next state sil next state s4 next state s13 1 next state s12 1 TO 1 0 esac esac next volume ex case next track pos ex case next state s11 next state 12 next state sil next state s4 next state s13 1 next state s12 1 Le Us Lee esac esac next mute_ex case next jump ex case next state sil next state 12 next state sil next state s4 next state s13 1 next state s12 1 15 D 1 0 esac esac Appendix C Complete NUSMV Code of RJB Module 59 Node Property SPEC EF SelectTrack ex SPEC EF Mode ex SPEC EF PlayTrack ex Edge Property DEFINE RJBI ex SelectTrack ex Mode ex PlavTrack ex DEFINE RJB1 en SelectTrack en Mode en PlavTrack en LTLSPEC G SelectTrack ex gt X SelectTrack en LTLSPEC G LTLSPEC G SelectTrack ex gt X Mode en SelectTrack ex gt X PlayTrack en LTLSPEC G LTLSPEC G LTLSPEC G LTLSPEC G Mode ex gt X SelectTrack en Mode ex gt X Mode en Mode ex gt X PlayTrack en PlayTrack ex SelectTrack en LTLSPEC G LTLSPEC G PlayTrack ex PlayTrack ex PlayTrack en Node Property SPEC EF check all ex SPEC EF check none ex SPEC EF check on ex SPEC EF check off ex Edge Property DEFINE SelectTrack ex check none ex check on ex check off ex
69. nisms for modules and processes corresponding to synchronous and asyn chronous composition and to express a set of system properties in CTL and LTL NuSMV can work batch or interactively with a textual interaction shell A NuSMV program is composed of modules A module is an encapsulated collection of declarations Once defined a module can be reused as many times as necessary Furthermore each instance of a module can refer to different data values A module can contain instances of other modules allowing a structural hierarchy to be built A process is a module which is instantiated using the keyword process The program executes a step by non deterministi cally choosing a process and then executing all of the assignment statements in that process specified with keyword ASSIGN There are two kind of assignment statements init and next init denotes the initial state of some variable next assigns to the variable its value at the next state It is implicit that if a given variable is not assigned a new value by the process then its value remains unchanged Case Study and Tool Support 33 5 3 1 Representation of System Model In this section the representation of the Kripke structure as a labeled transition system in NuSMV language is explained Small portions of codes are given as examples for under standing the syntax In each NuSMV code there must be one module with the name main The module main is evaluated by the
70. njected faults Table 5 Manual model checking of system properties System Properties cr EF rede valid cr EF redyellow valid cr EF green valid cr EF yellow valid ers G reda gt X redyellows valid ers G redyellow X greens valido cr G green gt X yellowen valid t crs G yellow X reden valid cro G redex gt X green n valid crio G redex gt X yellow n valid cri G red gt X red valid cry G redyellow gt X red valid cris G redyellow gt X yellow n valid cria G redyellow X redvellow valid cris G greene gt X red valid cris G green gt X redyellow valid cry G green gt X green valid cris G yellow gt X redyellow valid crio G yellow gt X green valid cra G yellow gt X yellow n valid Legend the check case passes the check case fails Coverage Driven Model Checking 25 4 6 Complexity Analysis of the Approach Since there are a finite set of nodes and a finite set of edges in Ms ec the number of proper ties to be checked on Ms s is also finite The number of system properties by node coverage increases linearly with the number of events whereas the number of system properties by edge coverage inc
71. om the test inputs system properties are produced in the form of temporal logic formulae Based on the holistic approach both the specified event sequences and the unspeci fied event sequences are considered by generating the system properties The number of gen erated system properties is limited by the size of the specification so the model checking process can be ended when all system properties are checked thus the completeness problem is handled In the rest of this chapter the approach illustrated in Fig 2 and Fig 3 is explained in detail using a simple example Section 4 1 shows how a system model can be converted into a Kripke structure for model checking purposes Section 4 2 introduces a simple example traf fic light system which will be used in the rest of the chapter Section 4 3 explains the concept of coverage based adequacy criterion and its adaptation to model checking by introducing the terms node coverage edge coverage and the complementary view of the edge coverage Sec tion 4 4 introduces a new term check case and explains its generation and its meaning for the approach Section 4 5 describes the model checking process of the check cases Section 4 6 gives an overview of the complexity of the approach 4 1 Converting the System Model into a Kripke Structure In order to verify the system properties generated from Mspec Vspec Espe Vo on Msys Syst Beet Aaen Rsyst Msyst has to be converted to a Kripke stru
72. on the SUC or more precisely on a model of the SUC learned by experimenting and testing 30 v conducting a series of case studies evaluating how well model checking techniques scale when used for test case generation 24 The approach in this thesis is different than the approaches mentioned above such that the properties to be model checked on the system model are generated from a black box test specification whereby a completeness criterion for the properties is proposed Preliminaries 5 3 Preliminaries This chapter explains some concepts which are necessary to understand the introduced ap proach Firstly the need of modeling the software is explained and some kinds of software models are defined Secondly the concepts of specification based testing are explained which are applied to model checking in this thesis Finally the foundations of model checking are explained 3 1 Modeling Software A model is always helpful when the complexity of the system under consideration exceeds a certain level It is then appropriate to focus on the relevant features of the system i e to abstract unnecessary details from it Different models are used for different purposes e g for requirements definition for design specification etc It is good practice to analyze and com pare these models for detecting and eliminating errors before the final product is released 9 Spec M s M psen SUC Mg
73. oyment of Ms for analysis and re quirement validation purposes respectively In this thesis event based systems are considered instead of state based systems where the user is rather interested in the external behavior black box behavior of the SUC than in its internal mechanism Therefore to specify the behavior of an event based system the devel oper and the user think in terms of system events instead of system states So the notion of event plays a central role An event is considered to be an externally observable phenomenon such as an environ mental or a user stimulus or a system response punctuating different stages of the system activity In this sense let V be the set of all possible events in the specification Mspec is then represented as a digraph 7 which is introduced below Definition 1 An Event Sequence Graph ESG is a directed graph V E with a finite set of nodes V and a finite set of edges E c V x V Mspee interprets the ESG as follows Any node v e V is interpreted as an event or as a stimulus action that triggers that event in the rest of the thesis the terms event and ac tion will be used as synonyms and each specified event is expected to be triggered at least once An edge e E connecting two consecutive events is interpreted as an event sequence For two events v and v in V the event v must be executable enabled after the execution of v if v and v compose
74. perty Generation Tool 48 Appendix B Property Generation Tool package propgen xx x An application class creating an instance of the property generation class x see propgen PropertyGeneratorApp see propgen PropertyGenerator version 1 0 06 Mai 2005 author Baris G ldali public class PropertyGeneratorApp The main method saves the first command line parameter in the variable directory and creates a new array with the given specification files An instance of the PropertyGenerator class is created and the diretory name and the specification files are given as parameters to the constructer param args The command line parameters containing the directory name and the specification files return no return value public static void main String args try if args length c 2 System out println Usage java propgen PropertyGenerator directory specfilel specfile2 System out println return String directory args 0 String inputfiles new Stringlargs length 1 for int i 1 i lt args length i inputfiles i 1 new String args i PropertyGenerator objPropGen new PropertyGenerator directory inputfiles obj PropGen generatePropertyList System out println Property list and declerations are saved under directory catch Exception e System out println Usage java propgen PropertyGenerator directory specfilel specfile2
75. play en LTLSPEC G pause ex X Track en LTLSPEC G record ex X play en LTLSPEC G Track ex X play en Fig 15 Not complete list of edge properties for ESG P ay Track As explained above the specification file may contain pseudo events in the title line e g Track in the example above If an edge property is generated in the form G pseudo eventx X v 4 this property is interpreted over all system events that are represented by the pseudo event In Fig 15 Track represents the system events forward rewind track pos and jump as given in sub level ESG Track in Fig 9 By using two DEFINE declarations these events can be assigned to the pseudo event Track first in the form of executed events and second in the form of enabled events Fig 16 Each occurrence of Track ex will then be replaced by the conjunction of these events forward ex rewind ex track pos ex jump ex using the OR operator Thus the LTL property G Track ex gt X play en in Fig 15 specifies that globally if there exists a state where forward rewind track pos or jump is executed the event play must be enabled at the next state Case Study and Tool Support 37 DEFINE Track_ex forward_ex rewind_ex track_pos_ex jump_ex DEFINE Track_en forward_en rewind_en track_pos_en jump_en Fig 16 DEFINE declaration for pseudo event Track Given the specification files of all ESG s in Fig
76. r This section explains how node properties are generated from Mec For the node coverage for each event v Vspec it is required to check if the event v is ever executable in Maer which can be specified by the CTL formula EF v4 1 This node property is valid if v is executed in some reachable state of Ma Since by defi nition Vex holds only at transition states of Ms s the property EFv successes if there exists a path along which v is ever executed Table 1 lists all node properties generated from Mspec of the traffic light system in Fig 4 Table 1 Node properties for the traffic light system Node Properties EF red EF redyellow EF green x EF yellow 4 3 2 Edge Coverage For achieving the adequacy criterion all edges from Espec Of Mspec must be covered by the generation of system properties Edge coverage can be seen as a liveness property requiring that a legal event sequence is possible in the system i e the second event of an event se quence is enabled after the first event is executed Liveness properties can be defined in LTL with the temporal operator G specifying the property on every state of a computation path This section explains how edge properties are generated from Mspee Coverage Driven Model Checking 21 For achieving the edge coverage for each edge v v Espec it is necessary to check if the event v is enabled right after the executions of
77. ration for system properties and required declerations begin Greturn no return value public void generatePropertyList String s Filename for int i20 i lt specificationFiles length i S Filename new String directory specificationFiles i System out println s Filename dimension countLines s Filename System out println dimension generateMatrix System out println adjacencyMatrix 0 length System out println eventArray length fillEventArray s Filename fillAdjacencyMatrix s Filename outputDeclerations s Filename outputProperties s Filename The method countLines counts the number of lines in the specification file Since the first line contains the modul name and the event names the counted value is decremented by one giving the dimension of the matrix Gparam s Filename The complete path of the specification file Greturn The numer of rows is returned as the dimension of the matrix public int countLines String s Filename int dimension 0 try Appendix B Property Generation Tool 51 String zeile BufferedReader br int idx kopf idx ende open the file count the number of lines close the file br new BufferedReader new FileReader s Filename while zeile br readLine null System out println zeile dimension dimension dimension 1 System out println d
78. rd Status Length ECE CA LA AAKS Find th es 8 Trac Requir Availa realjukebox central Fig 8 Top menu of the RealJukebox RJB Fig 8 represents the utmost top menu as a GUI of the RealJukebox RJB RealJukebox 2 B Build 1 0 2 340 Copyright 1995 2000 RealNetworks TM Inc RJB has been introduced as a personal music management system The user can build manage and play his or her indi vidual digital music library on a personal computer At the top level the GUI has a pull down menu that includes many functions For some of the mostly utilized functions there are buttons as short cuts on the top level GUI The graphical representation of the buttons gives an intuitive understanding of the availability of the corresponding function After a button is pressed either the button returns to its initial enabled state which makes it pressable again or Case Study and Tool Support 27 the button remains pressed and is disabled until some other action is taken which enables the button again As the code of the RJB is not available only black box methodologies are applicable to validate the behavior of the RJB In order to apply the introduced approach on RJB firstly the behavioral system model Ms s of RJB is produced by observing the system Ms s can be pro duced by experimenting with the system and identifying the system states and the appearance of the graphical components at these states that trigger the s
79. reases exponentially with the number of events The number of events can be controlled by abstracting the system or by handling the system functions separately 31 implies that the complexity of the automata based LTL model checking algorithm in creases exponentially in time with the size of the formula f but linearly with the size of the model S R The complexity of LTL model checking is O 2 x S R where size of the formula f the number of symbols propositions logical connectives and temporal operators appearing in the representation of the formula size of the model S R the number of elements in the set of states S added with the num ber of elements in the set of transitions R Based on this result the complexity of LTL model checking might be acceptable for short LTL formulas Additionally the size of the model should be also controllable to avoid the state space explosion problem For the present approach LTL model checking is deployed for each formula f generated from legal and illegal event sequences of Mspec and M spec The number of all legal and illegal event sequences is Vspec X Vspeel WW spec As explained in sections 4 3 2 and 4 3 3 the proper ties have always the same pattern Globally if some property p holds at some state at the next state a property q should either hold in case of a legal event sequence G p X4 or should not hold in case of an illegal event sequence G p
80. s explained in section 5 1 The system properties are generated from the ESG s in the form of an adjacency matrix As the adjacency matrix is stored as a plain text file the property generation tool should i read the file line by line ii extract the system evens from the title line iii generate node properties for each system event iv generate edge properties for each entry of the adjacency matrix v generate some supplementary declaration code for edge properties This section shows the activities of the property generation tool by means of an example As an example the specification files given in Table 8 and Table 7 for the system function Play and Record a CD or Track are chosen At the beginning the first line of the file in Table 8 is read the program extracts from this title line the ESG identifier PlayTrack which can be used in a higher level ESG e g in RJBI in Table 7 as a pseudo event Additionally the event names pause record stop and Track are extracted In this case Track is also a pseudo event used in the context of ESG Play Track For each event extracted from the title line a node property is generated The node proper ties are CTL formulas in the form EF v x as explained in section 4 3 1 A node property in CTL is defined in NuSMV language as follows exemplarily SPEC EF play ex This property specifies that a system state is reachable where event play is executed The CTL properties are introduced by the k
81. se quence The legal event sequences from Mspec represented with the edges of the ESG should be executable on the system on the other hand the illegal event sequences from M spe repre sented by the complementary edges of the ESG should not be executable on the system In specification based testing a set of test cases test suite 1s produced on the basis of a specification The existence of a formal specification makes the automatic generation of test suites possible Usually a test suite should satisfy a given property a criterion specifying when to stop testing Such a criterion could simply refer to some notion of coverage The next section explains more about test coverage and its uses 3 2 2 Test Coverage and Spanning Set Regardless of whether testing is specification oriented or implementation oriented if ap plied to large programs in practice both methods need an adequacy criterion which provides a measure of how effective a test suite is in terms of its potential to reveal faults 32 During the last decades many adequacy criteria have been introduced Most of them are coverage oriented i e they rate the portion of the system specification or implementation that is cov ered by the given test suite in relation to the uncovered portion when this test suite is applied to the SUC This ratio can then be used as a decisive factor in determining the point in time at which to stop testing i e to release the SUC or to improve it a
82. se the state changes stopped playing record stop pause ee pause recording record Fig 10 System model of RJB as a FSM For verification purposes some additional information about the system model is needed Beside the dynamic properties of the system some structural information about the system states is collected by observing the appearance of the graphical components at each state For example a button object on the GUI can be disabled at certain states which makes the func tionality behind this button not executable at these states Case Study and Tool Support 31 Using dynamic and structural properties the system model is translated into a Kripke structure in Fig 11 as explained in section 4 1 The states of the FSM are conserved and con verted to normal states in Kripke structure The executability of the system events are repre sented as atomic propositions e g at state stopped the play button is enabled and can be pressed which is represented with the atomic proposition plaven If some state is not labeled with playen that means the play button is either disabled or not visible at this state Some events are grouped into pseudo events for efficiency purposes For example the label SelectTracken is a macro definition combining all atomic propositions for all events related to the ESG Select Track in Fig 9 Sp Track Mode A SelectTrack Su
83. should not be executable after the action corresponding to the first event is executed The selection of the test cases is carried out by applying the node coverage and edge cover age criteria to Mspec V spec Espeo Vo and M spec Vspe E speo Vo The criteria requires all nodes and edges to be covered by test cases where according to the semantics of ESG com pare with section 3 1 1 covering a node v Vspec means to test the executability of the event v covering an edge v v Espec means to test the executability of v right after v is exe cuted Moreover the approach complementarily requires the testing of the impossibility of an event sequence v v when v v E spec The distinction between initial node vo and the Coverage Driven Model Checking 20 other nodes is not relevant for the property generation and will not be considered any further The generation of the system properties by using Ms ec and M spec will be explained in the following sections The traffic light system from section 4 2 will be used as an example for generating system properties 4 3 1 Node Coverage For achieving the adequacy criterion all nodes from Vspec of Mspec must be covered by the generation of system properties Node coverage can be seen as a reachability property requiring that a state is reachable where an action triggering the specified event is executed Reachability properties are defined in CTL with EF operato
84. st cases can then be run at the end of the development process without any knowledge of the implementation During each phase of software development formal specifications of the software e g finite state machines can be used to generate test cases There are numerous approaches to generate test cases from finite state machines 3 12 17 However if testing is done from a user s point of view internal specifications can not be used for test case generation since the user has no insight into the development process The only reference for the software functionality is the user manual which is mostly formulated in an informal descriptive language The user manual can also be seen as an informal specification or as a system description The challenge in testing is to include user s expectations and behavior into the testing using this informal system description As the user should obey the descriptions in the user manual it can be used as a source for test case Preliminaries 9 generation Thus the system is tested against the user manual If there are discrepancy between the system description in the user manual and the system behavior an error is found As introduced in chapter 2 a test case is a tuple of a test input and an expected test output In this thesis the test inputs are the event sequences specified by Mspec and its complement M spe as defined in 3 1 1 The expected test output is defined by the legality of the event
85. t be enabled at the next state where Track represents the system events forward rewind track pos and jump as given in sub level ESG Track in Fig 9 This property is false because Track is enabled at the system state recording which is the consecutive state of the transition states ze sg Case Study and Tool Support 40 and s o in which event record is executed This situation is also the source of the fault 1 in Table 9 e Similarly the properties 52 and 65 show unconformities which are also the source of the faults 3 and 4 in Table 9 e Fault 2 can not be considered in this context because the faulty functionality was tested in the context of system function 3 Edit Playlists and or Auto Playlists e Faults 5 6 and 7 are the faults that are additionally detected by the properties 47 53 58 65 66 and 68 NuSMV gt show property f PROPERTY LIST Type Status Counterex Trace PROPERTY LIST 031 G check_all_ex gt X check_on_en LTL False T1 036 G check_none_ex gt X check_off_en LTL False T2 047 G play_ex gt X record_en LTL False T3 052 G pause_ex gt X record_en LTL False T4 053 G pause_ex gt X stop_en LTL False T5 055 G record_ex gt X play_en LTL False T6 058 G record_ex gt X stop_en LTL False T7 059 G record_ex gt X Track_en LTL False T8 065 G Track_ex gt X play_en
86. the event v which can be specified by using the LTL formula G Vex S Xv Sch 2 This edge property is valid on the states in Msyst where v is executed and at all consecutive states v is enabled As from a transition state at which vex holds there is only one outgoing transition and it ends at a normal state the edge property in 2 will hold only if v is enabled at that normal state Note that an edge property as given in 2 is not sufficient to guarantee the executability of the event v since Msys may not execute the event v at all in which case the property in 2 will hold vacuously Hence the property 1 is also required to guarantee the executability of v at least once Table 2 lists all edge properties for the legal event sequences generated from Mspec of the traffic light system in Fig 4 Table 2 Edge properties for the traffic light system Edge Properties G reda gt X redyellowen G redyellow X greenen G green X yellowen G yellowe gt X reden 4 3 3 Complementing the Edge Coverage The approach can be extended by the holistic view of edge coverage where the comple mentary specification model M spee Vspeo E spes Vo is also considered by property generation M spe completes the missing edges in Mspec from Fig 4 by adding new edges to the ESG wherever possible as illustrated in by dashed lines in Fig 7 Additional system properties can be generated based o
87. to Mode in RJBI makes all combinations of Case Study and Tool Support 29 event sequences between the two ESG s possible The complementary specification model M spec can be easily produced by adding the missing edges in ESG s For computation purposes each ESG is represented as an adjacency matrix stored in a plain text file specification file The specification files contain semicolon separated data an edge between two nodes representing a legal event sequence is indicated as 1 If there is no edge between the two nodes a 0 is used indicating an illegal event sequence Table 7 shows the specification file of the top level ESG RJBI Table 7 Specification file of the top level ESG RJB RJB1 SelectTrack Mode PlayTrack The first line of the specification file contains the name of the ESG RJBI and the node la bels SelectTrack Mode and PlayTrack The node labels identify also columns and rows of the adjacency matrix Because the row identifiers are the same as the column identifiers they are only given once in the first line of the specification file Similarly Table 8 shows the specification file of the sub level ESG Play Track in RJB1 In the first line the name of the ESG and the system events are given Track is again a pseudo event representing the group of all events related to switching between tracks and changing the track position The speci
88. ut println br close catch FileNotFoundException e System out printin File not found s Filename catch IOException e System out println File g Filename can not be read finally return Appendix B Property Generation Tool 53 The method outputDeclerations generates for each lt i gt event lt i gt in the eventArray two kind of declerations lt l gt lt li gt lt i gt event lt i gt _ex lt li gt lt i gt event lt i gt _en lt 1 gt eparam s Filename The complete path of the specification file return no return value public void outputDeclerations String s Filename try String zeile BufferedReader br int idx_kopf idx_ende create declerations for enabled and executed events Problem auch f r pseudo events wird decleration erzeugt obwohl sie in DEFINE vorkommen BufferedWriter bw bw new BufferedWriter new FileWriter s Filename decl bw newLine for int i 0 i lt dimension i bw write eventArray il ex boolean bw newLine bw write eventArray il en boolean bw newLine bw newLine bw close catch FileNotFoundException e System out printin File not found s Filename catch IOException e System out println File s Filename can not be edited finally return Firstly the method outputProperties generates for a lt i gt module lt i gt DEFINE declerations using t
89. y of a model that specifies the user requirements on the system behavior and a sec ond model that describes the system behavior as designed or as observed The first model is complemented in also specifying the undesirable system properties The approach analyzes both these specification models to generate test cases that are then converted into temporal logic formulae to be model checked on the second model Introduction This thesis is organized as follows Chapter 2 provides an overview of the related work in combining testing and model checking and indicates the contribution and the differences of the approach in this thesis Chapter 3 explains some preliminaries related to the approach in order to build a basic understanding of the technologies used throughout this thesis and to create a terminological base for the rest of the thesis Chapter 4 explains the core of the ap proach where a simple example is used to make the definitions figurative Chapter 5 introduces tool support for the approach and demonstrates a case study where the approach is used to check the conformance of commercial multi media software to its specification In chapter 6 some further ideas are discussed and the work is concluded Formal Methods for Software Validation and their Combination Related Work 3 2 Formal Methods for Software Validation and their Combination Related Work In order to ensure the correctness of a software system during and
90. ystem events Secondly a specification model Ms is required for the approach The user manual of RJB is used to produce the Ms ec The production of Ms ec for RJB in the form of ESG s is ex plained in 10 where the same case study is used to demonstrate a testing technique In 10 RJB is tested manually with the test cases derived from ESG s and some errors are found The approach introduced in this thesis is different than the approach in 10 in relation to the fact that the actual system will not be tested directly the approach verifies properties on an ab straction of the system In section 5 4 the found errors in 10 are compared to the ones found with the approach in this thesis 5 1 Specification Model Because there is no system specification of RJB available to the end user the user manual facilities of RJB are used to produce references for construction of specification models 10 Specification models are produced and incrementally extended in terms of ESG s which are very rudimentary at the beginning but they are refined later on The constructed ESG s are grouped into 13 system functions that are listed in Table 6 Table 6 System functions of RJB 1 Play and Record a CD or Track 8 Skins 2 Create and Play a Playlist 9 Screen Sizes 3 Edit Playlists and or Auto Playlists 10 Different Views of Windows 4 Views Lists and or Tracks 11 Find Music 5 Edit a Track 12 Configure RJB 6

Model Testing – Combining Model Checking and Coverage Testing

Contents

Download Pdf Manuals

Related Search

Related Contents

Model Testing &ndash; Combining Model Checking and Coverage Testing

Contents

Download Pdf Manuals

Related Search

Related Contents

Model Testing – Combining Model Checking and Coverage Testing