UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

A family of protocol testing techniques Chan, Wendy Yuen-Ling 1989

Your browser doesn't seem to have a PDF viewer, please download the PDF to view this item.

Item Metadata

Download

Media
831-UBC_1989_A7 C42.pdf [ 5.45MB ]
Metadata
JSON: 831-1.0064927.json
JSON-LD: 831-1.0064927-ld.json
RDF/XML (Pretty): 831-1.0064927-rdf.xml
RDF/JSON: 831-1.0064927-rdf.json
Turtle: 831-1.0064927-turtle.txt
N-Triples: 831-1.0064927-rdf-ntriples.txt
Original Record: 831-1.0064927-source.json
Full Text
831-1.0064927-fulltext.txt
Citation
831-1.0064927.ris

Full Text

A FAMILY OF PROTOCOL TESTING TECHNIQUES by WENDY YUEN-LING CHAN B.A.Sc, The Univers i ty of B r i t i sh Columbia, 1987 A THESIS SUBMITTED IN PARTIAL FULFILMENT OF THE REQUIREMENTS FOR THE DEGREE OF MASTER OF APPLIED SCIENCE i n THE FACULTY OF GRADUATE STUDIES (DEPARTMENT OF ELECTRICAL ENGINEERING) We accept th is thesis as conforming to the requi red standard THE UNIVERSITY OF BRITISH COLUMBIA August 198 9 © Wendy Yuen-Ling Chan, 1989 In presenting this thesis in partial fulfilment of the requirements for an advanced degree at the University of British Columbia, I agree that the Library shall make it freely available for reference and study. I further agree that permission for extensive copying of this thesis for scholarly purposes may be granted by the head of my department or by his or her representatives. It is understood that copying or publication of this thesis for financial gain shall not be allowed without my written permission. Department of ELECTRICAL ENGINEERING The University of British Columbia Vancouver, Canada Date 1989 AUGUST 10 DE-6 (2/88) ABSTRACT T h i s t h e s i s deve loped th ree t e s t i n g t echn iques t h a t are a p p l i c a b l e to the conformance t e s t i n g of p r o t o c o l s : the UlOv-method, the eUIOv-method and the h y b r i d t e c h n i q u e . The UlOv-method i s f o r t e s t i n g s imple p r o t o c o l s mode l l ed by f i n i t e s t a t e machines (FSMs). Any p r o t o c o l t h a t passes i t s t e s t s possesses an FSM s k e l e t o n tha t i s i d e n t i c a l to the s p e c i f i e d FSM. The UlOv-method i s extended to the eUIOv-method to t e s t more complex p r o t o c o l s t h a t can be mode l l ed by extended FSMs (EFSMs). A da ta f l ow t e s t i n g procedure (DFTP) based on s t a t i c da ta f low a n a l y s i s and FSM t e s t i n g i s deve loped i n t h i s t h e s i s to t e s t the f l ow of parameters and v a r i a b l e s i n a p r o t o c o l . T h i s p rocedure i s augmented w i th the eUIOv-method to form the h y b r i d t e chn ique which i s d i r e c t l y a p p l i c a b l e to the t e s t i n g of complex p r o t o c o l s implemented a c c o r d i n g to t h e i r E s t e l l e s p e c i f i c a t i o n s . The techn ique cap tures p r o t o c o l s w i th er roneous EFSM c o n t r o l s t r u c t u r e s t ha t cannot be d e t e c t e d by e x i s t i n g t e s t i n g methods deve loped by Sa r i k aya and U r a l . KEYWORDS: conformance t e s t i n g , p r o t o c o l s , E s t e l l e , f i n i t e s t a t e machines , unique i n p u t / o u t p u t s , extended f i n i t e s t a t e mach ines , da ta f l ow , f a u l t coverage , p r o t o c o l s p e c i f i c a t i o n . i i TABLE OF CONTENTS A b s t r a c t i i Tab le of Contents i i i L i s t o f F i gu r e s v i L i s t o f T a b l e s . . . v i i Acknowledgement v i i i 1 I n t r o d u c t i o n 1 1.1 Past Tes t Gene ra t i on E f f o r t 3 1. 2 T h e s i s Goal 3 1.3 T h e s i s C o n t r i b u t i o n s 5 1.4 T h e s i s O r g a n i z a t i o n 7 2 The UIOv-Method 8 2.1 The F i n i t e S ta te Machine Model 9 2.2 FSM T e s t i n g Techniques 11 2.2.1 The T-Method 11 2.2.2 The W-Method 11 2.2 .3 The D-Method 12 2 .2 .4 The U-Method 13 2 . 2 . 5 Comments on the Four Methods 14 2 .2 .5 .1 A p p l i c a b i l i t y 14 2 .2 .5 .2 F a u l t Coverage 15 2.3 The Shortcoming of the U-Method 18 2.3.1 Assumptions 18 2.3.2 The UIOS Problem 19 2 .3 .3 The S ta te S igna tu re Problem 2 3 2.4 The UIOv-Method 2 5 2.4.1 Uniqueness Problem A n a l y s i s 26 2.4.2 ~Uv 27 2 .4 .3 IO(S ,K)s 28 2 .4 .4 Comparing the UIOv-Method w i th the Others 31 2.5 Unique Tes t Sequences 33 2.6 FSM T e s t i n g 37 2.7 Chapter Summary 38 3 T e s t i n g Extended F i n i t e S ta te Machines 41 3.1 Background 41 3.2 The EFSM Tab le 42 3.3 Ex t ens i on of the UIOv-Method 44 3.3.1 UIOSs S e l e c t i o n i n an EFSM 45 i i i Table of Contents 3.3.2 V e r i f i c a t i o n of TSS V a r i a b l e s 48 3 .3 .2 .1 V e r i f i c a t i o n of N.TSSs 49 3 .3 .2 .2 V e r i f i c a t i o n of C.TSSs 51 3 .3 .2 .3 UIOSs f o r TSSs 53 3.3.3 The eUIOv-Method 54 3.3.4 An Example 57 3.3.5 Summary of the eUIOv-Method 61 3.4 F a u l t Coverage 62 4 Data Flow T e s t i n g 64 4.1 S t a t i c Data Flow A n a l y s i s 65 4.2 Data Flow Paths 66 4.3 Data Flow T e s t i n g 67 4.4 The Data Flow T e s t i n g Procedure 70 4.5 An Example 72 4.6 Chapter Summary 7 5 4.7 Comments on the DFTP 7 7 5 The Hybr id Technique 80 5.1 Background 82 5.1.1 E s t e l l e 82 5.1.2 Normal Form E s t e l l e S p e c i f i c a t i o n s 84 5.1.2.1 Example of an NFS 8 5 5.2 R e f i n i n g the NFS 87 5.2.1 Canon i c a l T r a n s i t i o n s 87 5.2.2 Re fo rmat t ing the NFS 89 5.2.2.1 E x e c u t a b i l i t y Problems 89 5 .2 .2 .2 The Reformatted NFS 90 5 .2 .2 .3 The Enab l i ng C o n d i t i o n s 91 5 .2 .2 .4 The Def Statements 91 5 .2 .2 .5 Format of the rNFS 92 5.3 E s t e l l e EFSM T e s t i n g 94 5.3.1 Spontaneous T r a n s i t i o n s 96 5.3.2 T e s t i n g the EFSM i n the COTP 97 5.4 E s t e l l e Data f low T e s t i n g 105 5.4.1 Data Flow T e s t i n g f o r the COTP 107 5.5 Chapter Summary 119 6 E v a l u a t i o n and Comparison of the Hybr id Technique 120 6.1 E v a l u a t i o n 120 6.1.1 F a u l t Coverage 120 6.1.2 E x e c u t a b i l i t y 121 6 .1 .3 A p p l i c a b i l i t y 122 6 .1 .4 Tes t Data S e l e c t i o n 123 6 .1 .5 T e s t a b i l i t y 124 6.2 Comparison 126 7 C o n c l u s i o n s 130 i v 7.1 Thes i s Summary 7.2 Future Work . . . B i b l i o g r a p h y Appendix A NFS OF CLASS 0 TRANSPORT PROTOCOL. Appendix B rNFS OF CLASS 0 TRANSPORT PROTOCOL LIST OF FIGURES 2 . 1 An FSM s p e c i f i c a t i o n 20 2.2 A f a u l t y IUT of the FSM i n F i gu re 2.1 21 2.3 An FSM w i th no UIOS f o r s t a t e C 24 2.4 A f a u l t y implementa t ion of the FSM i n F i g u r e 2.3 2 5 2.5 A s imple FSM w i th an i nhe ren t UTS 3 5 v i LIST OF TABLES 2.1 U-method t e s t sequence f o r the FSM i n F i gu re 2.1 21 2.2 D-method t e s t sequence f o r F i gu re 2.1 22 2.3 U-method t e s t sequence f o r FSM i n F i gu re 2.3 24 2.4 UlOv-method t e s t sequence f o r the FSM i n F i g u r e 2 . 1 . . . 2 8 2.5 UlOv-method t e s t sequence f o r the FSM i n F i g u r e 2 . 3 . . . 3 0 3 . 1 An EFSM t a b l e 44 5.1 EFSM t a b l e f o r the C l a s s 0 T r anspo r t P r o t o c o l 95 5.2 Augmented EFSM t a b l e f o r C l a s s 0 T r anspo r t P r o t o c o l . . 1 0 9 v i i ACKNOWLEDGEMENT I would l i k e to thank Dr. Son Vuong f o r h i s gu idance and f o r h i s cons tan t encouragements t ha t I p u b l i s h my work. I would l i k e to thank Dr. Mabo I to f o r h i s c a r e f u l r e a d i n g of t h i s t h e s i s and f o r h i s he lp i n improv ing my w r i t i n g t remendous ly . I would l i k e to thank Dr. Sam Chanson and J i a n p i n g Wu f o r many h e l p f u l d i s c u s s i o n s and f o r t h e i r moral suppor t d u r i n g d i f f i c u l t t imes . A l s o , a ve ry s p e c i a l thank you to Dr. Gunther Schrack , w i thout h im, I would not have been ab le to become a graduate s tuden t . I would l i k e to thank the Na tu r a l S c i ences and E n g i n e e r i n g C o u n c i l o f Canada and Idacom E l e c t r o n i c s L i m i t e d f o r t h e i r support i n the., form of an U n i v e r s i t y and I ndus t r y Coope ra t i v e Research Grant . L a s t l y , many h e a r t f e l t thanks to my pa ren t s f o r t h e i r immeasurable love and unde r s t and ing ; and e s p e c i a l l y t o my b r o t h e r , Ramsey, and my f i a n c e , Dawson, f o r t h e i r cont inuous moral support and t h e i r immense f a i t h i n me; w i thout them, t h i s work would not have been p o s s i b l e . v i i i Introduct ion Dur ing conformance t e s t i n g , the p r o t o c o l imp lementa t ion under t e s t (IUT) i s t y p i c a l l y cons ide r ed as a " b l a c k box" s i n ce i t s source code i s g e n e r a l l y not a c c e s s i b l e . T e s t i n g i s c a r r i e d out u s i n g t e s t sequences. A t e s t sequence i s a sequence of i npu t /ou tpu t (I/O) p a i r s d e r i v e d from the p r o t o c o l s p e c i f i c a t i o n . Tes t i npu t s are a p p l i e d t o the IUT v i a i t s i npu t p o r t . The outputs generated by the IUT are r e c e i v e d v i a i t s output p o r t and compared w i t h the co r r e spond ing outputs i n the t e s t sequence. I f they match, the IUT i s s a i d to conform to the s p e c i f i c a t i o n . The a b i l i t y of a t e s t to d e t e c t non-conforming or er roneous IUTs d u r i n g t e s t i n g depends s o l e l y on the t e s t sequence used . R e c e n t l y , t e s t sequence g e n e r a t i o n has r e c e i v e d much a t t e n t i o n from the r e s e a r c h community; i n p a r t i c u l a r , sequences generated from the fo rma l s p e c i f i c a t i o n of p r o t o c o l s . The formal s p e c i f i c a t i o n language of i n t e r e s t i n t h i s t h e s i s i s E s t e l l e . In E s t e l l e , the c o n t r o l s t r u c t u r e of the p r o t o c o l i s mode l l ed as an extended f i n i t e s t a t e machine (EFSM) wh i l e the da ta f low aspec t of the p r o t o c o l i s d e s c r i b e d by a se t o f P a s c a l s ta tements . Introduct ion 1.1 PAST TEST GENERATION EFFORT Recent work on t e s t sequence g e n e r a t i o n based on E s t e l l e p r o t o c o l s p e c i f i c a t i o n s i n c l u d e those of S a r i k a y a [Sar i87] and U r a l [ U r a l 88 ] , both of whom emphasize the da ta f low aspec t of p r o t o c o l s and both of whom work from normal form E s t e l l e s p e c i f i c a t i o n s [ S a r i 86 ] . Other n o t a b l e t e s t sequence g e n e r a t i o n techn iques t ha t are a p p l i c a b l e to E s t e l l e p r o t o c o l s p e c i f i c a t i o n s i n c l u d e those deve loped f o r t e s t i n g f i n i t e s t a t e machines (FSMs) [Kou87, S a r i 8 2 , S i dh89 ] . These i n c l u d e the T-method [Na i t81 ] ; the W-method [Chow78, S i dh89 ] , the D-method [Gone70], and the U-method [Sabn88, Aho88] . T h e i r a p p l i c a t i o n s to p r o t o c o l conformance t e s t i n g were e x t e n s i v e l y s t u d i e d i n [ S idh89 ] . These methods examine on l y the c o n t r o l s t r u c t u r e of p r o t o c o l s ; they i gno re i n t e r a c t i o n p r i m i t i v e parameters and may face e x e c u t a b i l i t y problems when a p p l i e d to E s t e l l e s p e c i f i c a t i o n s . However, these methods are d i r e c t l y a p p l i c a b l e to the t e s t i n g of s imple p r o t o c o l s t ha t can be mode l led by FSMs. 1.2 THESIS GOAL The goa l o f t h i s t h e s i s i s to deve lop t e s t i n g t e chn iques f o r the conformance t e s t i n g of p r o t o c o l s such t h a t maximum f a u l t coverage can be a ch i e ved . F a u l t coverage i s d e f i n e d i n t h i s t h e s i s a c c o r d i n g to the s p e c i f i c a t i o n s o f 3 Introduct ion the p r o t o c o l s used . The f o l l o w i n g two i s s u e s are not of p r imary concern i n he re : t e s t sequence o p t i m i z a t i o n and t e s t a r c h i t e c t u r e . Problems i n the gene r a t i on of conformance t e s t sequences g e n e r a l l y f a l l i n t o two c a t e g o r i e s : coverage and o p t i m i z a t i o n . Whi le coverage dea l s w i th how to genera te t e s t sequences to ach ieve a p a r t i c u l a r f a u l t cove rage , o p t i m i z a t i o n dea l s w i th how to op t im ize a g i v e n t e s t sequence. A l though o p t i m i z a t i o n i s necessa ry to reduce the c o s t o f a t e s t , i t i s secondary to coverage . Only when a d e s i r a b l e f a u l t coverage i s ach ieved shou ld o p t i m i z a t i o n f o l l o w . T h i s t h e s i s thus focuses on the more impor tan t coverage i s s u e i n t e s t sequence g e n e r a t i o n . Some sample t e s t sequences genera ted i n t h i s t h e s i s are not o p t i m i z e d so t h a t t h e i r i n t e n t s may be e a s i l y f o l l o w e d . In t e s t i n g the IUT of a p r o t o c o l t ha t be longs to the Open System I n t e r c o n n e c t i o n (OSI) Reference Model [Zimm80], an upper t e s t e r and a lower t e s t e r are assumed to be a v a i l a b l e i n . th is t h e s i s to p rov ide c o n t r o l and o b s e r v a t i o n a t the upper and lower i n t e r f a c e s of the IUT. 4 Introduct ion 1.3 THESIS CONTRIBUTIONS T h i s t h e s i s c o n t r i b u t e s to s o l v i n g the problem of g e n e r a t i n g conformance t e s t sequences f o r p r o t o c o l s from t h e i r s p e c i f i c a t i o n s i n the f o l l o w i n g ways. T h i s t h e s i s found the o r i g i n a l U-method t o be inadequate and m o d i f i e d i t so t ha t i t i s now capab le of d e t e c t i n g a l l I/O e r r o r s as w e l l as s t a t e e r r o r s [Chan89b]. I t s f a u l t d e t e c t i o n c a p a b i l i t y i s now e q u i v a l e n t to those o f the W- and D-method. The D-method and W-method are a c t u a l l y s p e c i a l - cases of the m o d i f i e d U-method (UlOv-method) deve loped i n t h i s t h e s i s where the UlOv-method en joys the a p p l i c a b i l i t y advantage of the W-method and the l e n g t h advantage of the D-method wh i l e p r o v i d i n g f u l l f a u l t cove rage . T h i s t h e s i s i n t r o d u c e d the concept o f un ique . t e s t sequences (UTSs) . These are t e s t sequences unique t o the s p e c i f i e d FSM from which they are gene ra ted . Any 'FSM t h a t passes a t e s t u s i n g an UTS possesses a FSM s k e l e t o n i d e n t i c a l to the s p e c i f i e d FSM. T h i s t h e s i s extended the UlOv-method to produce the eUIOv-method f o r t e s t i n g p r o t o c o l s t ha t can be mode l l ed by EFSMs. T h i s t h e s i s deve loped a da ta f low t e s t i n g procedure based on s t a t i c da ta f low a n a l y s i s where each d e f i n i t i o n and 5 Introduct ion usage o f a v a r i a b l e are e x e r c i s e d d u r i n g t e s t i n g and , whenever p o s s i b l e , they are v e r i f i e d as w e l l . T h i s t h e s i s c r e a t ed a h y b r i d t e s t sequence g e n e r a t i o n t echn ique by augmenting the eUIOv-method w i th the da ta f low t e s t i n g p rocedure . T h i s h y b r i d techn ique i s a p p l i c a b l e to t e s t i n g the EFSM c o n t r o l s t r u c t u r e of a p r o t o c o l as w e l l as i t s da ta f l ow ; hence, i t i s d i r e c t l y a p p l i c a b l e to IUTs t h a t are implemented a c c o r d i n g to t h e i r E s t e l l e s p e c i f i c a t i o n s . Dur ing t e s t i n g , the IUT i s checked f o r each t r a n s i t i o n i n i t s E s t e l l e s p e c i f i c a t i o n . Each statement i n the t r a n s i t i o n i s e x e r c i s e d as w e l l as v e r i f i e d whenever p o s s i b l e . T h i s t h e s i s r e f i n e d and r e fo rma t t ed the normal form of E s t e l l e so t h a t i t s t r a n s i t i o n s are i n c a n o n i c a l form and i t s format e x p l i c i t l y b r i n g s out the u n d e r l y i n g EFSM and da ta f low i n an E s t e l l e s p e c i f i c a t i o n . The h y b r i d t echn ique was t a i l o r e d f o r p r o t o c o l s w i th u n d e r l y i n g EFSM c o n t r o l s t r u c t u r e s , t h i s t e chn ique i s thus capab le of d e t e c t i n g f a u l t y IUTs w i th er roneous EFSMs t h a t would o therw ise be missed by the t echn iques deve loped by U r a l and S a r i k a y a . S ince the h y b r i d t echn ique a l s o i n c l u d e s da ta f low t e s t i n g , i t i s capab le of d e t e c t i n g c e r t a i n t ypes of da ta f low e r r o r s i n an IUT tha t would o therw ise be missed by FSM t e s t i n g t e c h n i q u e s . 6 Introduct ion Tes t sequences generated by the h y b r i d t e chn ique are a l s o a p p l i c a b l e to IUTs not implemented a c c o r d i n g t o t h e i r E s t e l l e s p e c i f i c a t i o n s . The f a u l t coverage a ch i e ved would be l i m i t e d to f a u l t s i n the f low of d a t a ; sequenc ing f a u l t s may or may not be c ap tu r ed . 1.4 THESIS ORGANIZATION The remainder of t h i s t h e s i s i s o r g a n i z e d as f o l l o w s . Chapter 2 d i s c u s s e s FSM t e s t sequence g e n e r a t i o n t e chn iques and p resen t s the UlOv-method as w e l l as the UTS concep t . In chapte r 3, a b r i e f i n t r o d u c t i o n to EFSMs i s f o l l o w e d by a d i s c u s s i o n of ex tend ing the UlOv-method to the eUIOv-method f o r the t e s t i n g of p r o t o c o l s mode l led by EFSMs. Chapter 4 p r o v i d e s a b r i e f rev iew of s t a t i c da ta f low a n a l y s i s and shows how the da ta f low t e s t i n g procedure i s deve loped from i t . In chapte r 5, the h y b r i d techn ique i s d i s c u s s e d and a p p l i e d to E s t e l l e u s i n g the C l a s s 0 T r anspo r t P r o t o c o l as an example. An e v a l u a t i o n and a compar ison of the h y b r i d t echn ique w i th e x i s t i n g t e s t sequence g e n e r a t i o n t e chn iques a p p l i c a b l e to E s t e l l e p r o t o c o l s p e c i f i c a t i o n s are p r e sen t ed i n Chapter 6. Chapter 7 conc ludes t h i s t h e s i s w i t h a summary of i t s c o n t r i b u t i o n s and a d i s c u s s i o n of p o s s i b l e f u t u r e work i n the a rea of conformance t e s t i n g . 7 2 THE UIOV-METHOD T e s t sequence g e n e r a t i o n t e chn iques d e v e l o p e d f o r f i n i t e s t a t e machines (FSMs) may be used t o gene ra te conformance t e s t sequences f o r those p r o t o c o l s t h a t can be mode l l ed as FSMs. T h i s chap te r l ooks a t a r e c e n t s tudy done by S idhu [Sidh89] on t h i s approach to conformance t e s t g e n e r a t i o n . Four n o t a b l e t e s t g e n e r a t i o n methods were compared i n t h a t pape r : the T-method, the D-method, the W-method and the U-method. In g e n e r a l , the D-method i s hampered by i t s l i m i t e d a p p l i c a b i l i t y w h i l e the W-method i s u n d e s i r a b l e because o f the l e n g t h y t e s t sequences i t g e n e r a t e s . The T-method, on the o the r hand , has n e i t h e r one o f the above prob lems ; however, i t g e n e r a l l y cannot a c h i e v e f u l l f a u l t cove rage . The most, r e c e n t method, the U-method, i s more w i d e l y a p p l i c a b l e than the D-method and i t gene ra t e s s h o r t e r t e s t sequences than those genera ted by the W-method. F a u l t coverage produced by the U-method was found t o be f u l l i n [ S i dh89 ] . The U-method thus seemed t o be the b e s t o f the f o u r methods. T h i s chap te r shows t h a t the U-method does not a lways a ch i e ve f u l l f a u l t cove rage ; i t p o i n t s out a sho r t com ing w i t h the U-method [Chan89b] t h a t sometimes hampers i t s f a u l t d e t e c t i o n c a p a b i l i t y . The U-method i s then r e v i s e d w i t h the a d d i t i o n o f a v e r i f i c a t i o n p rocedure i n here to form the 8 The UIOv-Method UlOv-method [Chan89b] which c o r r e c t s the problem and produces f u l l f a u l t coverage each t ime . The r e s u l t i n g UIOv-method i s s t i l l more w ide l y a p p l i c a b l e than the D-method and i t g e n e r a l l y produces s h o r t e r t e s t sequences than the W-method does . A l l t e s t sequences generated by the D-method, W-method and UlOv-method possess a p rope r t y t ha t i s r e s p o n s i b l e f o r t h e i r f u l l f a u l t cove rages . T h i s p r o p e r t y d i s t i n g u i s h e s these sequences to be unique t e s t sequences (UTSs) [Chan89b], and i t guarantees the d e t e c t i o n of any e r roneous IUT p r o v i d e d t h a t the number of s t a t e s i n the IUT does not exceed t h a t which i s i n the FSM s p e c i f i c a t i o n . T h i s concept of UTSs i s a l s o rev iewed i n t h i s chap te r . 2.1 THE FINITE STATE MACHINE MODEL A f i n i t e s t a t e machine (FSM) can be r e p r e s e n t e d as F={S, I ,0 ,T,A} where S denotes the se t o f s t a t e s , I denotes the se t o f i n p u t s , O denotes the se t o f o u t p u t s , T denotes the s t a t e t r a n s i t i o n f u n c t i o n which produces a new s t a t e based on the c u r r e n t s t a t e and the c u r r e n t i n p u t , and A denotes the a c t i o n f u n c t i o n which produces an ou tput based aga in on the c u r r e n t s t a t e and the cu r r en t i n p u t . An FSM can a l s o be r ep re sen t ed by a c o l l e c t i o n o f t r a n s i t i o n s each of which performs an output o p e r a t i o n and a 9 The UIOv-Method s t a t e t r a n s i t i o n p r o v i d e d tha t an i npu t event i s c o r r e c t l y r e c e i v e d at the a p p r o p r i a t e s t a r t i n g s t a t e . T h i s r e p r e s e n t a t i o n can be p resen ted i n a t a b u l a r or g r a p h i c a l fo rmat . In the t a b u l a r fo rmat , each column i s l a b e l l e d by a s t a t e to denote the s t a r t i n g s t a t e of a t r a n s i t i o n . Each row i s l a b e l l e d by an i npu t o p e r a t i o n . Each t r a n s i t i o n i s denoted by a t a b l e en t r y i d e n t i f i e d by i t s output o p e r a t i o n and the next s t a t e . The g r a p h i c a l format i s denoted by G=(N,E) , where N i s a set o f nodes r e p r e s e n t i n g the s t a t e s of the machine and E i s a se t o f a r cs r e p r e s e n t i n g the se t of t r a n s i t i o n s . Each a rc s t a r t s a t the s t a r t i n g s t a t e of the t r a n s i t i o n and ends at i t s f i n a l s t a t e . Each a r c i s i d e n t i f i e d by the i npu t event t h a t t r i g g e r e d the t r a n s i t i o n and the output event p roduced . The FSM models c o n s i d e r e d i n t h i s t h e s i s are assumed to be min imal and s t r o n g l y connected Mealy machines t h a t may o r may not be comp le te l y s p e c i f i e d . A Mealy machine, M, i s an FSM whose se t o f outputs i s dependent on the se t o f s t a t e s as w e l l as the se t o f i n p u t s . The Mealy machine i s m i n i m a l , or r educed , i m p l i e s i t does not have e q u i v a l e n t s t a t e s ; t h a t i s , i t has the s m a l l e s t number of s t a t e s p o s s i b l e . Machine M i s comp le te l y s p e c i f i e d i f an output i s s p e c i f i e d f o r each i n p u t i n I f o r each of the s t a t e s i n S. A s t r o n g l y 10 The UIOv-Method connected machine possesses an i npu t sequence which t r a v e r s e s between any two s t a t e s i n the machine. 2.2 FSM TESTING TECHNIQUES There are fou r no tab le t e s t sequence g e n e r a t i o n t echn iques f o r FSMs: the T-method, the W-method, the D-method and the most r e cen t method, the U-method. 2.2.1 The T-Method The T-method [Nait81] i s the s i m p l e s t o f the f ou r methods. T h i s method i s a p p l i c a b l e to any s t r o n g l y connected FSM. I t genera tes a t e s t sequence, c a l l e d a t r a n s i t i o n t o u r , by a p p l y i n g random inpu t s to an FSM u n t i l every t r a n s i t i o n i s t r a v e r s e d at l e a s t once. There are two d i sadvantages to u s i n g the T-method. One i s the t e s t sequences genera ted may c o n t a i n redundant i n p u t s . The o the r be ing the t e s t on l y checks f o r the e x i s t e n c e of t r a n s i t i o n s ; i t does not v e r i f y t h a t the s t a t e s i n each t r a n s i t i o n are c o r r e c t . As a r e s u l t , the T-method may not d e t e c t s t a t e e r r o r s ; i t d e t e c t s on l y output e r r o r s . 2.2.2 The W-Method The o r i g i n a l PW-method [Chow78] was s l i g h t l y m o d i f i e d i n [Sidh89] to form the W-method, which i s a check ing 11 The UIOv-Method exper iment t ha t uses the W-set f o r s t a t e i d e n t i f i c a t i o n . A check ing exper iment i s a t e s t procedure which v e r i f i e s t h a t each i npu t s p e c i f i e d f o r a s t a t e produces the expec ted output and takes the FSM to the c o r r e c t next s t a t e . In the f i r s t p a r t o f a check ing exper iment , each s t a t e i n the FSM i s i d e n t i f i e d u s i n g a chosen c h a r a c t e r i z i n g I/O sequence. In the second p a r t o f the exper iment , each I/O o p e r a t i o n and the f i n a l s t a t e i n each t r a n s i t i o n i n the FSM are v e r i f i e d . The W-set i s a l s o known as the c h a r a c t e r i z a t i o n s e t . I t i s a se t of i npu t sequences which i s composed o f , f o r every p a i r o f s t a t e s i n the FSM, at l e a s t one i n p u t sequence t h a t can d i s t i n g u i s h them. Every m in ima l , s t r o n g l y connected and comple te l y s p e c i f i e d FSM possesses a W-set. Of the f ou r methods, the W-method produces the l o n g e s t t e s t sequences . I t i s capab le of d e t e c t i n g a l l f a u l t s i n an FSM w i th a number of s t a t e s not exceed ing tha t which i s i n the s p e c i f i e d FSM. 2.2.3 The D-Method The D-method [Gone70] i s a check ing exper iment which uses a se t o f d i s t i n g u i s h i n g sequences (DSs) f o r s t a t e i d e n t i f i c a t i o n . An DS can be thought of as a s p e c i a l case of a W-set where the re e x i s t s on l y one sequence of i n p u t s . T h i s 12 The UIOv-Method sequence produces a d i f f e r e n t sequence of outputs f o r every d i f f e r e n t s t a r t i n g s t a t e . Not every comp le te l y s p e c i f i e d , minimal and s t r o n g l y connected FSM possesses an DS. T h i s method, when a p p l i c a b l e , i s a l s o capable o f d e t e c t i n g a l l f a u l t s i n an FSM w i th a number of s t a t e s s m a l l e r than o r equa l to t ha t i n the s p e c i f i e d FSM. 2.2.4 The U-Method The U-method [Sabn88] i s a l s o a check ing exper iment w i th the e x c e p t i o n , t ha t i t uses a sequence of un ique i npu t /ou tpu t s (UIOs) to i d e n t i f y the s t a t e s i n each t r a n s i t i o n . An UIO sequence (UIOS) f o r a s t a t e i s an I/O behav i o r not e x h i b i t e d by any o the r s t a t e i n the FSM. Not every s t a t e i n an FSM possesses an UIOS. In the absence o f an UIOS, a s t a t e s i g n a t u r e i s used which i s formed by c o n c a t e n a t i n g a se t o f i npu t sequences , each of which d i s t i n g u i s h e s the s t a t e from one o the r s t a t e i n the FSM. An FSM does not have to be comp le te l y s p e c i f i e d i n o rde r to possess a se t o f UIOSs. In [ S idh89 ] , i t was found t h a t the U-method possesses a f a u l t d e t e c t i o n c a p a b i l i t y e q u i v a l e n t to those produced by the W- and D-method f o r m i n i m a l , comp le te l y s p e c i f i e d and s t r o n g l y connected FSMs. The U-method genera tes t e s t sequences whose l e n g t h s are 13 The UIOv-Method comparable to those generated by the D-method. T h e i r l eng ths are g e n e r a l l y s h o r t e r than those produced by the W-method. Both the U-method and the W-method are g e n e r a l l y a p p l i c a b l e to comple te l y s p e c i f i e d , s t r o n g l y connected and min imal FSMs, but be ing comple te l y s p e c i f i e d i s a necessa r y c o n d i t i o n f o r the W-method wh i l e i t i s s u f f i c i e n t , but not n e c e s s a r y , f o r the U-method [S idh89] . 2.2.5 Comments On The Four Methods 2.2.5.1 Applicability In d e c i d i n g on which t e s t method to use , the f i r s t f a c t o r to be c o n s i d e r e d i s a p p l i c a b i l i t y , then comes the a c h i e v a b l e f a u l t coverage , and f i n a l l y , the l e n g t h of the t e s t sequence produced . I f a l l T- , W-, D- and U-methods were a p p l i c a b l e to t e s t a p a r t i c u l a r FSM, then any one of the l a t t e r th ree methods i s p r e f e r r e d over the T-method because of t h e i r b e t t e r f a u l t cove rages . Among the th ree methods, the W-method i s the most u n d e s i r a b l e because of i t s l eng thy t e s t sequences. S ince UIOSs g e n e r a l l y occu r more f r e q u e n t l y than DSs do , the U-method seems to s tand out from among the t h r e e . 14 The UIOv-Method In f a c t , DSs are s p e c i a l cases of UIOSs where the i n p u t sequences f o r a l l the UIOSs are i d e n t i c a l . In the sea rch a l g o r i t h m presen ted i n [Sabn88] f o r f i n d i n g minimum UIOSs, i f the r e s u l t i n g UIOSs have i d e n t i c a l i n p u t sequences , then they would a l s o be r e f e r r e d to as DSs. The W-set i s to DSs as the s i g n a t u r e s are to UIOSs. The W-set possesses the same i n p u t c o n s t r a i n t as t h a t i n the DSs. Whi le s i g n a t u r e s are used when UIOSs are absen t , the W-set shou ld be used on l y when the DSs are absent because o f the l eng thy t e s t sequences t ha t can r e s u l t from u s i n g the W-method. From t h i s v i ewpo in t , the UIOSs or the s i g n a t u r e s , hav ing the l e a s t r e s t r i c t i v e c o n s t r a i n t s , occu r more f r e q u e n t l y than the DSs or the W-set does i n FSMs. 2.2.5.2 Fault Coverage The fou r FSM t e s t methods are d i r e c t l y a p p l i c a b l e to the conformance t e s t i n g of those p r o t o c o l s t h a t can be mode l l ed as FSMs. The a b i l i t y o f a t e s t sequence to dec ide whether a p r o t o c o l implementa t ion under t e s t (IUT) conforms to i t s s p e c i f i c a t i o n s o l e l y r e l i e s upon the range o f f a u l t s t h a t i t can d e t e c t . The f ou r methods work by check ing f o r the e x i s t e n c e of t r a n s i t i o n s and, w i th the excep t i on of the T-method, by v e r i f y i n g tha t the s t a t e s i n each t r a n s i t i o n are c o r r e c t . 15 The UIOv-Method In t h i s sense , m i s s i n g and erroneous s t a t e s and I/Os i n an IUT can be d e t e c t e d , but e x t r a s t a t e s and I/Os cannot . However, conformance mere ly r e q u i r e s t ha t an IUT behaves as a c c o r d i n g to i t s s p e c i f i c a t i o n . T h i s i m p l i e s as l ong as an IUT possesses a s k e l e t o n FSM tha t i s i d e n t i c a l to i t s s p e c i f i c a t i o n FSM, i t would be a conforming IUT independent of whether o the r s t a t e s or t r a n s i t i o n s e x i s t . As a r e s u l t , the W-, D- and U-method s u f f i c e as conformance t e s t methods f o r p r o t o c o l s . T h e i r on l y l i m i t a t i o n i s t h a t the IUT must not possess a number of s t a t e s t h a t exceeds t h a t which i s i n the s p e c i f i e d FSM s i n ce e x t r a s t a t e s no l o n g e r guarantee "what you see i s what you ge t " d u r i n g t e s t i n g . FSMs tha t model p r o t o c o l s may not be comp l e t e l y s p e c i f i e d . Those edges t h a t are s p e c i f i e d are r e f e r r e d to as core edges [Sabn88]. For the u n s p e c i f i e d s t a t e - i n p u t p a i r s , a Completeness Assumpt ion can be used where the p r o t o c o l machine i s e i t h e r assumed to produce a n u l l ou tput and remain i n i t s c u r r e n t s t a t e or i t i s assumed to en t e r an e r r o r s t a t e f o l l o w i n g the g e n e r a t i o n of an e r r o r message. The Completeness Assumpt ion a l lows an i n c o m p l e t e l y s p e c i f i e d FSM to become comple te l y s p e c i f i e d . Conformance can thus be d e f i n e d a t two l e v e l s : s t rong and weak. An IUT has s t r o n g conformance to i t s s p e c i f i c a t i o n i f , f o r a l l t e s t i n p u t s , i t genera tes the same outputs as those s p e c i f i e d i n i t s 16 The UIOv-Method s p e c i f i c a t i o n . An IUT has weak conformance to i t s s p e c i f i c a t i o n i f the IUT has the same I/O behav i o r as i t s i n c o m p l e t e l y s p e c i f i e d FSM s p e c i f i c a t i o n . For the non-core edges , the IUT has u n s p e c i f i e d b e h a v i o r . T h i s i m p l i e s s t r ong conformance t e s t i n g can be c a r r i e d out o n l y f o r those IUTs whose s p e c i f i c a t i o n FSMs are comp le te l y s p e c i f i e d ; o the rw i s e , on l y weak conformance t e s t i n g i s p o s s i b l e . The f o l l o w i n g summarizes the f a u l t coverages t h a t were r e p o r t e d i n [Sidh89] of the f ou r t e s t methods. The f a u l t coverage of the weak conformance t e s t sequence f o r the U-method i s b e t t e r than tha t of the T-method s i n c e the T-method on l y checks the I/O ope ra t i ons at each t r a n s i t i o n wh i l e the U-method v e r i f i e s the s t a t e s of each t r a n s i t i o n as w e l l . The f a u l t coverages of the s t rong conformance t e s t sequences, f o r the W-, D- and U-method are i d e n t i c a l and are b e t t e r than tha t of the T-method. The l a t t e r i s aga in based on the f a c t t ha t the T-method does not v e r i f y the s t a t e s d u r i n g t e s t i n g wh i l e the o the r th ree methods do . The former i s based on a l l th ree methods are check ing exper iments except d i f f e r e n t c h a r a c t e r i z i n g I/O sequences are used f o r s t a t e i d e n t i f i c a t i o n . S idhu c l a ims tha t each of the th r ee methods can d e t e c t a l l I/O e r r o r s as w e l l as s t a t e t r a n s i t i o n e r r o r s . T h i s , however, i s not the case as the f o l l o w i n g s e c t i o n w i l l show. 17 The UIOv-Method In g e n e r a l , a t e s t sequence generated by any one of the f ou r methods i s not un ique . The reason be ing an FSM has more than one t r a n s i t i o n t o u r , and i t may have more than one se t o f UIOSs' or DSs, or i t may have more than one W-set. The cho i ce of which c h a r a c t e r i z i n g sequence to use depends on the t e s t e r . 2.3 THE SHORTCOMING OF THE U-METHOD The U-method appeared to be the u l t i m a t e t e s t sequence g e n e r a t i o n method f o r FSMs where the a p p l i c a b i l i t y advantage of the W-method i s combined w i th the l e n g t h advantage of the D-method, and, a t the same t ime , i t possesses f u l l f a u l t d e t e c t i o n c a p a b i l i t y . U n f o r t u n a t e l y , t h i s i s not the c a se . I t was found i n [Chan8 9b] t ha t the f a u l t d e t e c t i o n c a p a b i l i t y o f the U-method i n f a c t depends on the se t o f UIOSs chosen . T h i s s e c t i o n i s e x t r a c t e d from [Chan89b]. I t compares the U-method w i th the D-method and i t shows why the U-method does not have as s t r ong f a u l t coverage as the D-method does . 2.3.1 Assumptions In the f o l l o w i n g d i s c u s s i o n , each s t a t e i n an IUT i s assumed to have a r e s e t i n p u t , r, which takes the IUT back to the i n i t i a l i d l e s t a t e ; no output i s genera ted by the IUT 18 The UIOv-Method i n response to r. An arc to denote t h i s f e a t u r e would be l a b e l l e d as r/-; i t would beg in a t a s t a r t i n g s t a t e and end at the i n i t i a l i d l e s t a t e . Each r/- arc shou ld be t r e a t e d as a t r a n s i t i o n and e x e r c i s e d as w e l l as v e r i f i e d d u r i n g t e s t i n g , but f o r s i m p l i c i t y , each arc w i l l be assumed to be c o r r e c t i n the f o l l o w i n g d i s c u s s i o n . Sample t e s t sequences genera ted i n t h i s s e c t i o n are not o p t i m i z e d to b e t t e r i l l u s t r a t e the r o l e of each subsequence. These sequences can be o p t i m i z e d by e l i m i n a t i n g those t e s t subsequences t h a t are comp le te l y con ta ined i n o the r t e s t subsequences. 2.3.2 The UIOS Problem T e s t i n g of the s imple FSM e x t r a c t e d from [Chan89b] and shown i n F i gu re 2. 1 shows the f a u l t coverage f o r the U-method i s not always i d e n t i c a l to t ha t o f the D-method. 19 The UIOv-Method Figure 2.1: An FSM spec i f icat ion. The t e s t sequence generated by the U-method, shown i n Tab le 2 . 1 , cannot d e t e c t the f a u l t y imp lementa t i on , shown i n F i g u r e 2 .2 , o f the FSM i n F i gu re 2 .1 . The UIOSs chosen f o r s t a t e s 1, 2 and 3 i n t ha t t e s t sequence are a/1 , a/0.a/1 and b/l .a/1 r e s p e c t i v e l y . The r e s u l t i n g t e s t sequence c o u l d not d e t e c t the erroneous t a i l s t a t e f o r the b/1 edge. 20 The UIOv-Method r/- a/1 r/- a/1.a/0.a/1 r/- a / l . b / 1 . b / l . a / 1 r/- a/1.a/0.a/1 r/- b/1 .b/ l . a/1 r/- a/1.a/0.a/1 r/- a/1 .b/1 .b/1 .a/1 r/- a/1 .b/1 .a/0 .a/0 .a/1 r/- a/1 .b/1 .b/1 .a/1 Table 2.1: U-method tes t sequence fo r the FSM in F igure 2.1. b/1 F igure 2.2: A fau l ty IUT of the FSM i n F igure 2.1. 21 The UIOv-Method However, the t e s t sequence generated by the D-method shown i n Tab le 2.2 i s capab le of d e t e c t i n g t h i s f a u l t y IUT. The DSs chosen f o r s t a t e s 1, 2 and 3 are r e s p e c t i v e l y a /1 . a /0 , a/0.a/1 and a/0 .a/0 . r/- a/1.a/0 r/- a/1.a/0.a/1 r/- a /1 .b/1 . a/0 . a/0 r/- a/1.a/0.a/1 r/- b/1 .a/0 .a/0 r/- a/1 . a/0 . a/1 . a/0 r/- a /1 .b/1 . a/0 . a/0 r/- a/1 .b/1 .a/0 .a/0 .a/1 r/- a / 1 . b / 1 . b / 1 . a / 1 . a / 0 Table 2.2: D-method test sequence fo r F igure 2.1. The reason why the U-method t e s t sequence c o u l d not d e t e c t the er roneous t a i l s t a t e f o r the b/1 edge i s because the chosen se t of UIOSs i s unique i n the s p e c i f i c a t i o n FSM, but i t i s not unique i n the f a u l t y IUT i n F i g u r e 2 .2 . Both s t a t e s 1 and 3 i n the f a u l t y IUT cou ld generate the UIOS, b/1. a/1 , chosen f o r s t a t e 3 i n the t e s t . T h i s non-uniqueness i s not de t e c t ed d u r i n g the t e s t i n g of the IUT. As a r e s u l t , the IUT cou ld be i n e i t h e r s t a t e 1 or s t a t e 3 when b/1.a/1 i s observed d u r i n g , t e s t i n g . I f , however, another se t of UIOSs were chosen , f o r i n s t a n c e , a/1 f o r s t a t e 1, a/0.a/1 f o r s t a t e 2 and a/0.a/0 f o r s t a t e 3, then the f a u l t y IUT would be de t e c t ed as these UIOSs are a l s o unique I/O behav io r s i n the f a u l t y IUT. 22 The UIOv-Method The problem w i th the U-method i s thus UIOSs are used based on the assumpt ion tha t they are a l s o UIOSs i n the IUT when i n f a c t they may not be. UIOSs are chosen based on the FSM s p e c i f i c a t i o n . They are capab le of i d e n t i f y i n g the s t a t e s i n the s p e c i f i c a t i o n , but they cannot i d e n t i f y s t a t e s i n the IUT un l e s s they are a l s o UIOSs i n the IUT. In a f a u l t y IUT, UIOSs may not be un ique . Hence, the U-method i n c o r r e c t l y assumes tha t i f UIOSs are unique i n the s p e c i f i c a t i o n , then they must a l s o be unique i n the IUT. As a r e s u l t , an er roneous s t a t e cou ld escape d e t e c t i o n i f i t i s capab le of p roduc ing e x a c t l y the same UIOS t h a t be longs t o another s t a t e . 2.3.3 The State Signature Problem The uniqueness problem may a l s o e x i s t f o r s t a t e s i g n a t u r e s . I t may even be i nhe r en t s i n ce s i g n a t u r e s are not r e q u i r e d to be unique [Chan8 9b] . F i g u r e 2.3 i s a d u p l i c a t e of F i gu re 4 i n [Chan89b] . I t shows an FSM whose s t a t e C has no UIOSs. A s i g n a t u r e , 0 / 0 . 0 / 1 . 1 / 0 , i s genera ted f o r i t . Note t h a t the s i gna tu r e i s not un ique to s t a t e C; s t a t e B i s a l s o capab le of g e n e r a t i n g t h i s I/O sequence. 23 The UIOv-Method 0/1 0/0 1/0 0/0 Figure 2.3: An FSM with no UIOS fo r state C. A t e s t sequence f o r t h i s FSM genera ted by the U-method i s shown i n Tab le 2 .3 . The UIOSs chosen f o r s t a t e s A and B are 0/1 and 1/1 r e s p e c t i v e l y . r/- 0/1 r/- 1/0. 1/1 r/- 0/1. 0/0 . . 0 /1 . 1/0 r/- 1/0. 1/1 r/- 0/1 . 0/0, . 0/1 . 1/0 r/- 1/0. 0/0, .0/1 r/- 1/0. 1/1, .0/0 . 0/1.1/0 r/- 0/1 . 0/0, .0/1 r/- 0/1. 1/0. . 1/1 Table 2.3: U-method tes t sequence fo r FSM i n F igure 2.3. T h i s t e s t sequence cannot d e t e c t the f a u l t y IUT shown i n F i g u r e 2 .4 . The edge 1/1 from s t a t e B i n c o r r e c t l y ended a t s t a t e B i n the f a u l t y IUT, but t h i s i s not d e t e c t e d by the t e s t sequence i n Tab le 2 .3 . The reason i s because the 24 The UIOv-Method s t a t e s i g n a t u r e used to v e r i f y s t a t e C i s not un ique . As a r e s u l t , when the s t a t e s i gna tu r e i s obse rved , the s t a t e t h a t genera ted i t c ou ld have been e i t h e r C or B. T h i s p rob lem, u n l i k e the UIOSs, cou ld be i nhe ren t i n s t a t e s i g n a t u r e s ; t h a t i s , t h i s non-uniqueness cou ld a l s o e x i s t i n the s p e c i f i c a t i o n FSM. As a r e s u l t , the er roneous f i n a l s t a t e a l s o escapes d e t e c t i o n d u r i n g t e s t i n g . 0 / 1 0 / 0 1 / 0 0 / 0 f c ) 1 / 0 1 / 1 Figure 2.4: A fau l ty implementation of the FSM in F igure 2.3. 2.4 THE UIOV-METHOD T h i s s e c t i o n r e v i s e s the U-method w i th the a d d i t i o n of a v e r i f i c a t i o n procedure to e l i m i n a t e i t s un iqueness p rob lems . 25 The UIOv-Method 2.4.1 Uniqueness Problem Analysis The uniqueness problem w i th the U-method c o n c e r n i n g i t s UIOSs i s not e v i den t i n the D-method or the W-method. The reason i s because the i npu t sequences f o r the DSs and the W-set are i d e n t i c a l f o r a l l the s t a t e s i n a g i v en FSM. Dur ing the f i r s t s t a t e i d e n t i f i c a t i o n procedure i n a check ing exper iment genera ted by the D- or W-method, a s t a t e t h a t responds w i th the c o r r e c t output sequence i m p l i e s two t h i n g s : the s t a t e possesses the c o r r e c t DS o r W-set as a c c o r d i n g to the s p e c i f i c a t i o n ; as w e l l , the s t a t e does not generate an DS or W-set t ha t be longs to another s t a t e . T h i s e l i m i n a t e s the p o s s i b i l i t y t ha t more than one s t a t e i n the IUT may produce the same c h a r a c t e r i z i n g I/O sequence. In a check ing exper iment genera ted by the U-method, the f i r s t s t a t e i d e n t i f i c a t i o n procedure may have d i f f e r e n t i n p u t sequences f o r d i f f e r e n t s t a t e s . As a r e s u l t , a s t a t e which responds w i th the expected output sequence i m p l i e s i t possesses the expected UIOS as a c c o r d i n g to i t s s p e c i f i c a t i o n , but i t c e r t a i n l y does not imp ly t h a t i t cannot produce an UIOS tha t be longs to another s t a t e whose i n p u t sequence d i f f e r s from t h a t of i t s own UIOS. 26 The UIOv-Method 2.4.2 ~Uv The way to e l i m i n a t e the uniqueness problem c o n c e r n i n g the UIOSs i s thus to ensure t ha t the chosen se t o f UIOSs f o r a s p e c i f i e d FSM i s a l s o a se t o f UIOSs i n the IUT; t h a t i s , the un iqueness of the UIOSs a l s o ho lds i n the IUT. T h i s can be ach ieved by v e r i f y i n g the uniqueness of the UIOSs p r i o r to t h e i r uses d u r i n g t e s t i n g [Chan89b]. T h i s v e r i f i c a t i o n procedure w i l l be r e f e r r e d to as ~Uv wh i l e the u s u a l s t a t e i d e n t i f i c a t i o n procedure i n the U-method w i l l be r e f e r r e d to as Uv from now on. The U-method w i th the a d d i t i o n o f ~Uv w i l l h e n c e f o r t h be r e f e r r e d to as the UlOv-method. ~Uv i s r e q u i r e d on l y f o r those s t a t e s whose UIOSs have d i f f e r e n t i n p u t sequences ; f o r the o the r s t a t e s , ~Uv i s i m p l i e d i n Uv [Chan89b]. Dur ing ~Uv, a p a r t i a l i n p u t sequence may be s u f f i c i e n t . For i n s t a n c e , g i v en two s t a t e s A and B i n an FSM, i f the UIOS f o r A i s a/1 .b/1 .a/0 and the response o f B to the i npu t sequence a . b . a i s 1 .0 .0 , then B can be t e s t e d f o r the absence of a /1 .b/1 . a/0 by mere ly o b s e r v i n g t h a t B generates the subsequence a / l . b / 0 s i n c e t h i s i s enough to show tha t B cannot g e n e r a t e ' a / 1 . b / 1 . a / 0 . T h i s p a r t i a l i t y reduces the cos t o f the f i n a l t e s t sequence. In ~Uv, the emphasis i s on s t a t e s not g e n e r a t i n g UIOSs t h a t be long to o the r s t a t e s , hence, i d e n t i c a l ou tpu ts genera ted by d i f f e r e n t s t a t e s i n response to the same i n p u t s 27 The UIOv-Method are a c c e p t a b l e ; whereas i n Uv, t h i s would not be a l l owed as i t i m p l i e s one UIOS i s genera ted by more than one s t a t e . An example t e s t sequence u s i n g the UlOv-method i s produced i n Tab le 2.4 f o r the FSM i n F i gu re 2 .1 . T h i s t e s t sequence i s e q u i v a l e n t to t h a t shown i n Tab le 2.1 w i th the e x c e p t i o n t ha t ~Uv i s added. Note t ha t a t subsequence r/- b/1.a/0 the f a u l t y IUT i n F i gu re 2.2 f a i l s s i n ce s t a t e 1 d i s p l a y s r/-b/l .a/1 i n s t e a d ; t ha t i s , s t a t e 1 genera tes the UIOS t h a t be longs to s t a t e 3. r/- a/1 r/- a/1 .a/0 .a/1 r/- a/1 .b/1 .b/1 .a/1 r/- a/1 .b/1 .a/0 r/- a/1 .b/1 .a/0 .a/0 r/- b/1 .a/0 r/- a/1 .b/1 .a/0 r/- a/1 .a/0 .a/1 r/- b/1 .b/1 .a/1 r/- a/1 .a/0 .a/1 r/- a/1 .b/1 .b/1 .a/1 r/- a/1 .b/1 .a/0 .a/0.a/1 r/- a/1 .b/1 .b/1 .a/1 Table 2.4: UlOv-method test sequence f o r the FSM i n F igure 2.1. 2.4.3 IO(S,K)s To c o r r e c t the i nhe r en t uniqueness problem i n s t a t e s i g n a t u r e s , [Chan89b] proposed the use of a se t o f IO(S ,K )s i n p l a c e of a s t a t e s i g n a t u r e . Each member i n the se t o f IO(S ,K)s i s a sequence of I/Os tha t d i s t i n g u i s h e s the s t a t e , 28 The UIOv-Method S, to which the IO(S,K)s b e l o n g s , from a t l e a s t one o the r s t a t e , K, i n the FSM. T h i s i s somewhat s i m i l a r to the W-set w i th the e x c e p t i o n t h a t the i npu t sequences i n the IO(S ,K )s f o r d i f f e r e n t S s t a t e s may be d i f f e r e n t and the number o f sequences i n each se t of IO(S ,K)s may a l s o va ry depend ing on s t a t e S. The s i z e of the se t o f IO(S ,K)s f o r a s t a t e S i s the minimum r e q u i r e d to d i s t i n g u i s h S from a l l o the r s t a t e s i n the FSM. Each se t o f IO(S ,K)s must be unique to s t a t e S. Each se t i s t r e a t e d as though i t i s an UIOS d u r i n g t e s t i n g ; t h a t i s , each i s v e r i f i e d i n the same way UIOSs are v e r i f i e d i n the ~Uv and Uv procedures p r i o r to t h e i r uses d u r i n g t e s t i n g . Dur ing the t r a n s i t i o n t e s t i n g , T t , p o r t i o n of the check ing exper iment , each I/O o p e r a t i o n w i th t a i l s t a t e S w i l l be t e s t e d a number o f t imes equa ls to the number o f I/O sequences i n i t s se t o f IO (S ,K )s . An example i s shown i n Tab le 2.5 f o r the FSM i n F i gu re 2 .3 . 29 The UIOv-Method r/- 0/1 r/- 1/0. 1/1 r/- 0/1. 0/0 r/- 0/1. 1/0 r/- 1/0 r/- 1/0 r/- 0/1 r/- 0/1. 0/0 r/- 0/1. 1/0 r/- 1/0. 1/1 r/- 1/0. 0/0 r/- 1/0. 0/0 r/- 1/0. 1/1 r/- 1/0. 0/0 . o/i r/- 0/1. 0/0. 0/1 r/- o/i. 1/0. 1/1 r/- 0/1. 0/0 r/- 0/1. 1/0 r/- 1/0. 1/1. 0/0 r/- 1/0. 1/1. 1/0 Table 2.5: UlOv-method tes t sequence fo r the FSM i n F igure 2.3. For s t a t e C, IO(C,A) i s 0/0 and IO(C,B) i s 1/0. These two sequences are checked f o r t h e i r absences i n s t a t e s A and B du r i ng . ~Uv. In s t a t e A , a l though 1/0 i s p r e s e n t , 0/0 i s absen t . In s t a t e B, 0/0 i s p resen t but 1/0 i s absen t . Hence, IO(C,A) and IO(C,B) t oge the r can be used to u n i q u e l y i d e n t i f y s t a t e C. Each edge tha t ends at C, 1/0 from A and 1/1 from B, i s checked twice u s i n g 1/0 f i r s t then 0/0 the second t ime . Note t ha t the f a u l t y IUT i n F i g u r e 2.3 possesses the same se t o f UIOSs and IO(C,K)s as t h a t i n the s p e c i f i e d FSM. As a r e s u l t , the er roneous f i n a l s t a t e f o r edge 1/1 i s d e t e c t e d by IO(C ,B ) . 30 The UIOv-Method Whi le the DSs are s p e c i a l cases of the UIOSs, the W-se ts can be viewed as s p e c i a l cases of the IO(S ,K )s where the former has the a d d i t i o n a l c o n s t r a i n t s t h a t the i n p u t sequences must be i d e n t i c a l f o r a l l the s t a t e s and the number of sequences i n each W-set f o r each s t a t e must be i d e n t i c a l . As w e l l , the W-set must e x i s t f o r every s t a t e i n the FSM. In the remainder of t h i s t h e s i s , when UIOSs or IO(S ,K )s are r e f e r r e d t o , i t . i s assumed tha t these are v e r i f i a b l e UIOSs and v e r i f i a b l e IO (S ,K )s . 2.4.4 Comparing The UIOv-Method With The Others The f a u l t coverage produced by the UlOv-method i s b e t t e r than t h a t produced by the U-method. E r roneous t a i l s t a t e s such as those i l l u s t r a t e d i n the p r e v i o u s s e c t i o n s are now d e t e c t a b l e . . The f a u l t coverage of the UlOv-method i s now i d e n t i c a l to those of the W- and D-method. The p roo f i s as f o l l o w s . F i r s t o f a l l , the W-, D- and UlOv-method are a l l check ing exper iments w i th the e x c e p t i o n t h a t they use d i f f e r e n t c h a r a c t e r i z i n g I/O sequences f o r s t a t e v e r i f i c a t i o n . Second ly , the DSs and the W-set are s p e c i a l cases of the UIOSs and the IO(S ,K)s r e s p e c t i v e l y . R e c a l l how the ~Uv procedure f o r a p a r t i c u l a r s t a t e i s i m p l i e d i n 31 The UIOv-Method i t s Uv procedure when the i npu t sequences f o r the UIOSs be l ong in g to o the r s t a t e s are i d e n t i c a l to t h a t o f i t s own UIOS. In t h i s sense , the s t a t e i d e n t i f i c a t i o n p rocedures o f the check ing exper iments generated by the W- and D-method accomp l i sh what both Uv and ~Uv accompl i sh i n the UIOv-method. As a r e s u l t , the f a u l t coverages of the W-, D- and UlOv-method are i d e n t i c a l . The l e n g t h of the t e s t sequences produced by the UIOv-method are o b v i o u s l y l onge r than those produced, by the U-method; however, they , are g e n e r a l l y , s h o r t e r than the sequences d e r i v e d by the W-method s i n ce the l a t t e r r e q u i r e s t ha t each t r a n s i t i o n be t e s t e d a number of t imes equa l s to the f i x e d number of I/O sequences i n the W-set. In compar ison to the D-method, i t i s more d i f f i c u l t as the sequence l eng ths may d i f f e r a c c o r d i n g t o d i f f e r e n t FSMs. The t e s t subsequence co r r e spond ing to Uv and ~Uv i s l i k e l y l onge r than t h a t co r r e spond ing to the s t a t e i d e n t i f i c a t i o n procedure f o r the D-method. However, the subsequence f o r the T t p o r t i o n of the t e s t i s l i k e l y s h o r t e r i n the UIOv-method because of l e s s r e s t r i c t i v e c o n d i t i o n s i n fo rming the UIOSs, which produce UIOSs t h a t are g e n e r a l l y s h o r t e r than DSs. I f the UIOv- and D-method were both a p p l i c a b l e t o an FSM and the DSs are s h o r t e r than the UIOSs, then the D-32 The UIOv-Method method shou ld be used ; o the rw i se , both methods need to be examined. In terms of a p p l i c a b i l i t y , the UlOv-method i s more w ide l y a p p l i c a b l e than both D- and W-methods. T h i s i s obv ious due to the added c o n s t r a i n t s i n the f o rma t i on o f the DSs and W-set. The l i k e l i h o o d tha t a se t o f DSs e x i s t s i n a g i v en FSM i s g e n e r a l l y lower than tha t f o r a se t o f UIOSs or W-set. In g e n e r a l , a .m in ima l and s t r o n g l y connected Mealy machine be ing comp le te l y s p e c i f i e d i s a s u f f i c i e n t but not necessa ry c o n d i t i o n f o r the . a p p l i c a t i o n of the D-, W- and UlOv-method. The necessa ry c o n d i t i o n i s t h a t the FSM possesses an DSs s e t , a W-set or an UIOSs s e t . The same c o n d i t i o n a p p l i e s to i n c o m p l e t e l y s p e c i f i e d machines : so l ong as such a machine possesses a comp le te l y s p e c i f i e d FSM s k e l e t o n from which a se t of DSs or a W-set can be p roduced , or from which stems a set o f UIOSs, the r e s p e c t i v e D-, W-and UlOv-method would be a p p l i c a b l e . Hence, a l l t h r ee methods are a p p l i c a b l e to any FSM independent of whether i t i s comp le te l y or i n c o m p l e t e l y s p e c i f i e d as l ong as the r e q u i r e d c h a r a c t e r i z i n g I/O sequences e x i s t i n the FSM. 2.5 UNIQUE TEST SEQUENCES A l l t e s t sequences genera ted by the D-, W- and UIOv-meth.ods ach ieve f u l l f a u l t coverage i n the t e s t i n g o f FSMs. 33 The UIOv-Method A p r o p e r t y t h a t i s common among these t e s t sequences i s cap tu red i n the concept of unique t e s t ' sequences (UTSs) proposed i n [Chan89b]. F u l l f a u l t coverage i n FSM t e s t i n g i n t h i s t h e s i s i m p l i e s the d e t e c t i o n of a l l e r roneous and m i s s i n g s t a t e s and I/Os. An UTS i s d e f i n e d to be a t e s t sequence t h a t i s unique to a s p e c i f i e d FSM, M, i f t he re does not e x i s t any o the r FSM w i th the same number of s t a t e s and t r a n s i t i o n s , as t ha t i n M capab le . o f p roduc i ng an I/O sequence t h a t . i s i d e n t i c a l to the UTS of M. An IUT thus passes a t e s t t h a t uses an UTS. i f and on l y i f t he . IUT possesses a FSM. s k e l e t o n i d e n t i c a l to the s p e c i f i e d FSM. T h i s i m p l i e s UTSs are capab le of d e t e c t i n g any f a u l t y IUT p r o v i d e d t h a t the number of s t a t e s i n the IUT i s no g r e a t e r than t h a t which i s i n the FSM s p e c i f i c a t i o n . T h i s a l s o i m p l i e s an IUT t h a t passes such a t e s t may possess e x t r a t r a n s i t i o n s i n a d d i t i o n to those s p e c i f i e d i n the FSM s p e c i f i c a t i o n , p r o v i d e d t h a t the IUT has a number of s t a t e s g r e a t e r than or equa l to t ha t which i s i n the FSM s p e c i f i c a t i o n . An UTS can be formed by u s i n g a sequence of I/Os to a c c u r a t e l y d e s c r i b e each t r a n s i t i o n i n the FSM s p e c i f i c a t i o n ; t ha t i s , each I/O o p e r a t i o n i s d e s c r i b e d as i s , t h e i r s t a r t i n g and f i n a l s t a t e s are d e s c r i b e d by t h e i r c h a r a c t e r i z i n g I/O sequences. T h i s i m p l i e s t h a t i f t he re 34 The UIOv-Method e x i s t s a program which generates FSM graphs a c c o r d i n g to a g i v en I/O sequence and a g i ven number of s t a t e s , then i f the g i v en I/O sequence were an UTS, then the re would be one and on l y one graph tha t can be generated from the g i v en sequence. An FSM may have more than one UTS depending on which c h a r a c t e r i z i n g I/O sequence i s s e l e c t e d . I t was found i n [Chan89b] t h a t t e s t sequences produced by the D-method and the UlOv-method were sequences of I/Os t h a t a c c u r a t e l y d e s c r i b e d each t r a n s i t i o n s p e c i f i e d i n the g i v en FSM; t ha t i s , both methods produced UTSs. S ince the W-method i s a s p e c i a l case of the D-method and the UIOv-method, i t i s a l s o capab le of gene r a t i ng UTSs. S ince the T-method d e s c r i b e s on l y the I/O o p e r a t i o n s i n s i d e each t r a n s i t i o n w i thout any r e f e r e n c e to i t s s t a t e s , t h i s method g e n e r a l l y does not produce UTSs i n FSMs w i th the e x c e p t i o n of the f o l l o w i n g type of s imple FSMs. F igure 2.5: A simple FSM with an inherent UTS. 35 The UIOv-Method In the s imple FSM, assuming tha t the t e s t sequence must beg in a t the i n i t i a l s t a t e , s t a t e 1, the s h o r t e s t t r a n s i t i o n t ou r p o s s i b l e i s a/1, a/2, a/3. Th i s i s not an UTS because the re e x i s t s two o the r comp le te l y s p e c i f i e d FSMs, each hav ing th ree s t a t e s and an i npu t se t I = {a}, t h a t i s capab le of gene r a t i ng an I/O sequence i d e n t i c a l t o a / 1 . a / 2 . a / 3 . These two FSMs d i f f e r from t h a t i n F i g u r e 2.5 by the t a i l s t a t e of the a/3 a r c . One FSM has i t s a/3 a rc end a t s t a t e 2; the o the r has i t s a/3 a rc end a t s t a t e 3. However, the t r a n s i t i o n tou r a/1 .a/2 .a/3 .a/1 i s an UTS s i n c e i t bounds the t a i l s t a t e of a/3 to s t a t e 1, the o n l y s t a t e t h a t genera tes a/1. UTSs app ly to both comple te l y and i n c o m p l e t e l y s p e c i f i e d FSM s p e c i f i c a t i o n s s i n ce the D-, W- and UIOv-method are a p p l i c a b l e to any FSM tha t possesses a se t o f DSs, a W-set or a se t of UIOSs r e s p e c t i v e l y . T h i s i m p l i e s any IUT t h a t possesses an FSM s k e l e t o n i d e n t i c a l t o the s p e c i f i c a t i o n FSM, whether i t be comple te l y or i n c o m p l e t e l y s p e c i f i e d , w i l l pass a t e s t u s i n g an UTS based on the s p e c i f i c a t i o n . One q u e s t i o n tha t i s o f t e n brought up i s whether a genera ted t e s t sequence i s c o r r e c t ; t ha t i s , whether the t e s t c o r r e c t l y r ep r e sen t s the s p e c i f i c a t i o n so t h a t any IUT t h a t passes t h a t t e s t must conform to the s p e c i f i c a t i o n . 36 The UIOv-Method One way to v e r i f y t ha t a g i ven t e s t i s c o r r e c t i s to generate a l l p o s s i b l e FSMs tha t co r respond to the g i v en t e s t . I f the t e s t uses an UTS, then the re would e x i s t o n l y one FSM, w i th the same number of s t a t e s and t r a n s i t i o n s as t ha t i n the s p e c i f i c a t i o n , t ha t can be gene ra ted . 2.6 FSM TESTING Much can be l e a r n t from FSM t e s t i n g . In the T-method, t r a n s i t i o n s are on l y e x e r c i s e d d u r i n g t e s t i n g . T h i s method g e n e r a l l y ach ieves a p a r t i a l , f a u l t coverage t h a t i s comparable to t ha t produced by the branch coverage c r i t e r i o n i n sof tware t e s t i n g , where each branch i s e x e r c i s e d a t l e a s t once . From the T-method, i t becomes c l e a r t h a t mere ly e x e r c i s i n g s ta tements , or b ranches , do not c o n s t i t u t e a s u f f i c i e n t t e s t ; t h a t i s , some e r r o r s may escape d e t e c t i o n . These e r r o r s are those found i n elements t h a t a re not d i r e c t l y obse rvab le i n the I/O o p e r a t i o n s ; f o r i n s t a n c e , the s t a t e s i n an FSM.. . The check ing exper iments f o r FSMs so l v e t h i s problem by v e r i f y i n g each s t a t e w i th i t s c h a r a c t e r i z i n g I/O sequence. Th i s i s p o s s i b l e because the v a r i a b l e STATE takes on a f i n i t e se t of p o s s i b l e v a l u e s . As w e l l , each d i f f e r e n t va lue can be c h a r a c t e r i z e d by a d i f f e r e n t I/O sequence. T h i s , however, may not be p o s s i b l e i n so f tware t e s t i n g where a se t o f p o s s i b l e va lues f o r a g i v e n v a r i a b l e 37 The UIOv-Method may be i n f i n i t e . As w e l l , the re may not be a sequence o f e x t e r n a l l y obse rvab le events t ha t can d i f f e r e n t i a t e among d i f f e r e n t va lues of a v a r i a b l e . N e v e r t h e l e s s , FSM t e s t i n g does show tha t e x e r c i s e a long w i th v e r i f i c a t i o n g i v e s improved f a u l t coverage over tha t produced by e x e r c i s e a l o n e . 2.7 CHAPTER SUMMARY In summary, check ing exper iments f o r t e s t i n g FSMs are capab le of d e t e c t i n g a l l s t a t e s and I/O e r r o r s as a c c o r d i n g to an FSM s p e c i f i c a t i o n . . Before the advent of the UIOv-method, check ing exper iments based on DSs were hampered by t h e i r l i m i t e d a p p l i c a b i l i t i e s wh i l e those based on W-sets were handicapped by t h e i r l eng thy t e s t sequences . " With the advent of the UlOv-method, check ing exper iments became more a p p l i c a b l e w i thout the d i sadvantage of a l eng thy t e s t sequence. The UlOv-method so l ves the uniqueness problem i n the UlO-method w i th the use of a v e r i f i c a t i o n p rocedu re . T h i s s o l u t i o n i s independent of which UIOS i s non-unique i n the IUT [Chan89c] ; i t so l ves the problem by a t t a c k i n g i t s cause . T h i s s o l u t i o n permi ts any minimum l eng th UIOS to be used p r o v i d e d tha t i t i s v e r i f i a b l e ; hence, i t does not 38 The UIOv-Method c o n s i d e r a b l y add to the comp lex i t y of the sea rch a l g o r i t h m f o r UIOSs g i ven i n [Sabn88]. Check ing exper iments generate t e s t sequences t h a t are unique to the s p e c i f i e d FSM. As a r e s u l t , any IUT t h a t passes such a t e s t possesses an FSM s k e l e t o n t h a t i s i d e n t i c a l to the s p e c i f i e d FSM; however, i t may have a d d i t i o n a l t r a n s i t i o n s t ha t do not be long to the s p e c i f i c a t i o n . In terms of a p p l i c a b i l i t y , check ing exper iments are g e n e r a l l y a p p l i c a b l e to Mealy machines t ha t are min imal and s t r o n g l y connec ted . . Whether a Mealy machine i s comp le t e l y or i n c o m p l e t e l y s p e c i f i e d i s not impor t an t , so l ong as i t has a comp le te l y s p e c i f i e d s k e l e t o n f o r which a W-set o r a se t o f DSs can be gene ra ted , or from which stems a se t o f UIOSs, a check ing exper iment would be a p p l i c a b l e . One r e s u l t from FSM t e s t i n g i s t ha t mere e x e r c i s i n g of t r a n s i t i o n s a lone g e n e r a l l y cannot uncover a l l f a u l t s . E x e r c i s e of t r a n s i t i o n s a long w i th v e r i f i c a t i o n , whenever p o s s i b l e , produce a b e t t e r f a u l t coverage . In the remainder of t h i s t h e s i s , the "UlOv-method" w i l l be used to r e f e r to the UlOv-method, the W-method, as . w e l l as the D-method f o r s i m p l i c i t y . Th i s i m p l i e s the term "UIOSs" w i l l r e f e r to UIOSs as w e l l as DSs. T h i s i s p o s s i b l e s i n ce DSs are mere ly UIOSs whose i n p u t sequences 39 The UIOv-Method must be i d e n t i c a l f o r a l l the s t a t e s i n an FSM. S i m i l a r l y , the term " IO (S ,K )s " w i l l a l s o r e f e r to the W-sets s i n c e the l a t t e r are r e a l l y IO(S ,K)s whose i npu t sequences are i d e n t i c a l f o r a l l the s t a t e s and whose members must be c o n s i s t e n t l y numbered among the s t a t e s i n an FSM. 40 3 TESTING EXTENDED FINITE STATE MACHINES Techniques f o r t e s t i n g FSMs are a p p l i c a b l e to t e s t i n g s imple p r o t o c o l s t ha t can be mode l led by FSMs. These models , however, are i m p r a c t i c a l f o r complex p r o t o c o l s which may r e q u i r e a very l a r g e number of s t a t e s . For i n s t a n c e , the use of sequence numbers i n a p r o t o c o l i n t r o d u c e s a d i f f e r e n t s t a t e f o r each p o s s i b l e v a l u e . T h i s i s known as the s t a t e space e x p l o s i o n prob lem. A remedy to the s t a t e space e x p l o s i o n problem i s by u s i n g an extended f i n i t e s t a t e machine (EFSM) model f o r the s p e c i f i c a t i o n of more complex p r o t o c o l s . When FSM t e s t i n g t echn iques are a p p l i e d to such models , e x e c u t a b i l i t i e s o f the r e s u l t i n g t e s t sequences are no l onge r guaran teed . T h i s chapte r d i s c u s s e s how the UlOv-method can be extended t o the t e s t i n g of p r o t o c o l s mode l led by EFSMs so tha t e x e c u t a b i l i t y of the f i n a l t e s t sequence i s guaranteed and maximum f a u l t coverage i s ach ieved w i t h i n the l i m i t a t i o n s of t e s t i n g . 3.1 BACKGROUND An EFSM i s an FSM w i th the a d d i t i o n of minor s t a t e v a r i a b l e s . These v a r i a b l e s form a d d i t i o n a l e n a b l i n g c o n d i t i o n s i n the t r a n s i t i o n s to reduce the number of s t a t e s r e q u i r e d i n the u n d e r l y i n g FSM. As a r e s u l t , d i f f e r e n t t r a n s i t i o n s may occur i n response to the same combina t ion o f 41 Testing Extended F in i t e State Machines i n p u t event and s t a r t i n g s t a t e i n an EFSM. A t r a n s i t i o n i n an EFSM may be t r i g g e r e d by th ree types of e n a b l i n g c o n d i t i o n s : the i npu t event , the c u r r e n t s t a t e and a boo lean e x p r e s s i o n i n v o l v i n g minor s t a t e v a r i a b l e s . Each t r a n s i t i o n now c o n s i s t s of th ree o p e r a t i o n s : the ou tput o p e r a t i o n , the s t a t e t r a n s i t i o n and o p e r a t i o n s t h a t a l t e r va lues of the minor s t a t e v a r i a b l e s . The " s t a t e " o f an EFSM no l onge r . r e f e r s to the va lue be l ong ing to the STATE v a r i a b l e a lone but i t r e f e r s to the va lues b e l o n g i n g to the minor s t a t e v a r i a b l e s . as w e l l . The " s t a t e " of an EFSM w i l l be r e f e r r e d to as i t s t o t a l system s t a t e (TSS) from now on . 3.2 THE EFSM TABLE Tes t sequences genera ted from FSMs are g e n e r a l l y done a c c o r d i n g to t h e i r d i r e c t e d graphs . A s i m i l a r graph can be c o n s t r u c t e d f o r EFSMs; however, s i n ce minor s t a t e v a r i a b l e s need to be c o n s i d e r e d as w e l l i n EFSMs to ensure the f i n a l t e s t sequences are e x e c u t a b l e , when these v a r i a b l e s are i n c l u d e d i n an EFSM d i r e c t e d graph , the graph can become very c l u t t e r e d and d i f f i c u l t to use . The t a b u l a r format i s thus b e t t e r s u i t e d f o r r e p r e s e n t i n g EFSMs f o r t e s t i n g purposes and i s used i n here as a t o o l f o r the t e s t sequence g e n e r a t i o n p rocedure . 42 Test ing Extended F in i t e State Machines Columns i n the EFSM t a b l e are l a b e l l e d by the s t a r t i n g TSSs o f the EFSM t r a n s i t i o n s . Rows i n the EFSM t a b l e are l a b e l l e d by the f i n a l TSSs of the EFSM t r a n s i t i o n s . Each t a b l e en t r y r e co rds a t r a n s i t i o n and can be l a b e l l e d by e i t h e r the t r a n s i t i o n i d e n t i f i e r , t * , or the i n p u t and output ope r a t i ons w i t h i n the t r a n s i t i o n . The EFSM t a b l e thus con t a i n s i n f o r m a t i o n on the semant ics and syntax o f an EFSM. By c o n s i d e r i n g b o t h , i n s t ead , o f syntax a l o n e , e x e c u t a b i l i t y i s taken i n t o c o n s i d e r a t i o n d u r i n g the t e s t sequence gene r a t i on p r o c e s s . Tab le 3.1 shows a s imple example of an EFSM t a b l e . There i s on l y one minor s t a t e v a r i a b l e , c , i n the example. When c i s absent at the cu r r en t TSS, C .TSS , or a t the next TSS, N.TSS, i t i n d i c a t e s c can assume any v a l u e . 43 Test ing Extended F in i te State Machines ^ ^ " ^ ^ ^ T S S N.TSS S i c<2 s i s l c = 2 s2 s2 c<2 s2 c = 2 s i c : =c + 1 a/0 s i b/-s2 c:=0 a/3 s2 a/-s2 c : =c+1 b/0 s i c:=0 b/3 Table 3.1 An EFSM table. 3.3 EXTENSION OF THE UIOV-METHOD The UlOv-method i s extended i n t h i s s e c t i o n t o be a p p l i e d to EFSM t e s t i n g . An EFSM i s an FSM w i th a d d i t i o n a l minor s t a t e v a r i a b l e s , hence, the UlOv-method i s d i r ec t l y-a p p l i c a b l e to t e s t i n g i t s FSM p o r t i o n . The UIOSs and preambles , .however, must be c a r e f u l l y s e l e c t e d to p reven t e x e c u t a b i l i t y problems i n the f i n a l t e s t sequence. In a d d i t i o n , s i n ce minor s t a t e v a r i a b l e s c o n t r i b u t e to the TSS, they must a l s o be v e r i f i e d the same way STATE v a r i a b l e s are i n FSM t e s t i n g . 44 Testing Extended F in i te State Machines 3.3.1 UIOSs Select ion In An EFSM For s i m p l i c i t y , those t r a n s i t i o n s i n an EFSM whose s t a r t i n g TSSs i n v o l v e p-uses of minor s t a t e v a r i a b l e s w i l l be r e f e r r e d t o as " e . t r a n s i t i o n s " i n the subsequent d i s c u s s i o n . Those t r a n s i t i o n s t ha t do not w i l l s imp ly be r e f e r r e d to as " t r a n s i t i o n s . " For example, r e f e r r i n g t o Tab le 3 .1 , those t r a n s i t i o n s w i th the f o l l o w i n g I/Os are e . t r a n s i t i o n s : a/0, a/3, b/0 and b/3.< E x e c u t a b i l i t y problems may e x i s t i n the chosen UIOSs i f they c o n t a i n . e . t r a n s i t i o n s and t h e i r e n a b l i n g c o n d i t i o n s are not p a r t o f the UIOSs. An uncompl i ca ted way t o p reven t e x e c u t a b i l i t y problems i n the UIOSs chosen i s to "remove" a l l the e. t r a n s i t i o n s i n the EFSM t a b l e to form a t a b l e r e p r e s e n t i n g a pure FSM. The search a l g o r i t h m i n [Sabn88] f o r . . UIOSs i s now d i r e c t l y a p p l i c a b l e t o the t a b l e . E . t r a n s i t i o n s are a l l , the t r a n s i t i o n s found under the columns l a b e l l e d w i th . TSS v a r i a b l e s c o n s i s t i n g of minor s t a t e v a r i a b l e s . . In p r a c t i c e , . t he , e . t r a n s i t i o n s are not p h y s i c a l l y removed but are s imply i gno red d u r i n g the s e a r c h . A l though t h i s method may not produce minimum UIOSs, i t s advantage i s t ha t e x e c u t a b i l i t y i s guaranteed w i t h i n the UIOSs. T h i s i m p l i e s no s p e c i a l preamble i s r e q u i r e d to enable any UIOS. As w i l l be seen l a t e r on , s p e c i a l preambles can c o n s i d e r a b l y i n c r e a s e the f i n a l l e n g t h o f the 45 Test ing Extended F in i te State Machines t e s t sequence and may be p rob l ema t i c i n the t e s t i n g of e . t r a n s i t i o n s . I f the r e s u l t i n g FSM t a b l e produces on l y n o n - v e r i f i a b l e UIOSs which are UIOSs whose i npu t sequences are not a p p l i c a b l e to o the r s t a t e s f o r v e r i f i c a t i o n , then ~Uv must i n v o l v e e . t r a n s i t i o n s . Th i s may r e q u i r e s p e c i a l preambles to pe rmi t e x e c u t a b i l i t y d u r i n g ~Uv. The t a i l s t a t e s of these preambles must be v e r i f i e d u s i n g t h e i r r e s p e c t i v e UIOSs to ensure ~Uv i s performed f o r the c o r r e c t s t a t e . These preambles a r e . formed on l y f o r the purpose of an execu tab l e ~Uv p rocedure . The Uv and ~Uv procedures d u r i n g t e s t i n g w i l l use these s p e c i a l preambles . I f a s t a t e i n the FSM t a b l e does not have an UIOS, then the EFSM t a b l e has to be used to f i n d an UIOS f o r t h a t s t a t e . The e . t r a n s i t i o n s i n the r e s u l t i n g UIOS r e q u i r e the f o l l o w i n g a t t e n t i o n . I f w i t h i n the UIOS the p-use of the minor s t a t e v a r i a b l e i n an e . t r a n s i t i o n i s enab led by a t r a n s i t i o n t h a t i s a l s o . w i t h i n . the UIOS, then the UIOS i s execu tab l e by i t s e l f and does not r e q u i r e a s p e c i a l preamble . I f , however, the e n a b l i n g t r a n s i t i o n , e t , i s not w i t h i n the UIOS, then the preamble f o r the s t a t e , s, to which the UIOS be longs must i n c l u d e e t . Two p o s s i b i l i t i e s can o c cu r . The e t may have s as i t s ending s t a t e . T h i s i s a problem i f there e x i s t s more than one incoming a r c to s. 46 Testing Extended F in i te State Machines T h i s i m p l i e s the UIOS cannot be used to v e r i f y the t a i l s t a t e s of the o the r incoming a r cs because the UIOS would not have been enab led . Another UIOS or a set o f IO ( s , k ) s would have to be used f o r s t a t e s. I f , however, the re i s o n l y one incoming arc to s and i t enables the UIOS, then the UIOS may be used f o r s. The o the r p o s s i b i l i t y i s t ha t the e t ends a t a s t a t e o the r than s, i n which case a p a r t i a l preamble can be formed from the i n i t i a l s t a t e of the EFSM to the e t , and d e f - f r e e . p a t h s j o i n i n g t h i s p a r t i a l preamble to each of the s t a r t i n g s t a t e s f o r . the incoming a r cs to s complete the preambles . . The UIOS f o r s can be used p r o v i d e d these preambles e x i s t f o r a l l the incoming a r cs to s. Each o f the preambles must have i t s t a i l s t a t e checked to ensure i t a r r i v e s a t the c o r r e c t s t a t e be fo re i t i s used i n the T t p rocedu re . Us ing s p e c i a l . preambles and hav ing to v e r i f y t h e i r end ing s t a t e s i s a pena l t y to pay when UIOSs have e x e c u t a b i l i t y . p rob l ems . . . The r e s u l t i n g t e s t sequence, as w e l l , may not be m in ima l . In a d d i t i o n , i f the t r a n s i t i o n to be t e s t e d i s an e. t r a n s i t i o n which r e q u i r e s an e t to be i n c l u d e d i n the preamble , then the preamble needs to enab le both the e . t r a n s i t i o n and the UIOS. Such a preamble may not e x i s t , i n which case another UIOS has to be found . There may perhaps be an execu tab le set of IO ( s , k ) s f o r s t a t e s 47 Test ing Extended F in i te State Machines t ha t would reduce the number of s p e c i a l preambles r e q u i r e d and produce a s h o r t e r t e s t sequence. An o p t i m i z a t i o n t echn ique such as t ha t used i n [Shen89] would f i n d the bes t a l t e r n a t i v e . For the example i n Tab le 3 .1 , t r a n s i t i o n s a/- and b/-c o n s t i t u t e UIOSs f o r the s t a t e s s2 and s i r e s p e c t i v e l y . S ince they are not e . t r a n s i t i o n s , they do not r e q u i r e s p e c i a l preambles to enable them. 3.3.2 Ve r i f i c a t i on Of TSS Var iables • • The UlOv-method v e r i f i e s a s t a t e i n an FSM w i t h i t s UIOS. S i m i l a r l y , i n an EFSM, va lues of minor s t a t e v a r i a b l e s t ha t c o n t r i b u t e to the TSS shou ld a l s o be v e r i f i e d so t ha t the TSS i s v e r i f i e d , not j u s t the STATE v a r i a b l e i n the EFSM. In the same way tha t a s t a t e i s v e r i f i e d by the UIOS tha t i s unique to i t , an TSS can a l s o be v e r i f i e d by the I/O sequence tha t i s - unique to i t . However, i t may not be p o s s i b l e to v e r i f y the whole TSS as a u n i t . For i n s t a n c e , the re may not e x i s t a t r a n s i t i o n whose C.TSS i s i d e n t i c a l to the N.TSS to be v e r i f i e d so tha t an I/O sequence t h a t beg ins a t t ha t C.TSS t r a n s i t i o n can per form the v e r i f i c a t i o n . The reason i s as f o l l o w s . The C.TSS f o r a p a r t i c u l a r t r a n s i t i o n may not i n v o l v e a l l the minor s t a t e v a r i a b l e s t h a t appear i n 48 Test ing Extended F in i te State Machines a l l the C.TSSs i n the EFSM. U n s p e c i f i e d v a r i a b l e s are a l l owed to assume any v a l u e . As a r e s u l t , an N.TSS f o r a t r a n s i t i o n may not be v e r i f i a b l e as a whole i f t he re does not e x i s t a t r a n s i t i o n w i th an C.TSS which con t a i n s p-uses of a l l the v a r i a b l e s tha t c o n t r i b u t e d to the N.TSS. An example would be the t r a n s i t i o n a/- i n Tab le 3 .1 . T h i s t r a n s i t i o n cannot be used to v e r i f y the N.TSS f o r the t r a n s i t i o n a/3 which has the v a r i a b l e c r e s e t to 0. The C.TSS f o r a/- merely r e q u i r e s t ha t the STATE v a r i a b l e be at s2 , i t says no th ing about the v a r i a b l e c. - Hence, e x e r c i s i n g a/- a f t e r a/3 cannot v e r i f y c a l though i t can v e r i f y t h a t the f i n a l STATE i s a t s2 . The c v a r i a b l e thus has to be v e r i f i e d s e p a r a t e l y . For C .TSSs , each v a r i a b l e i n v o l v e d may a l s o have to be v e r i f i e d s e p a r a t e l y . 3 .3 .2 .1 V e r i f i c a t i o n of N.TSSs V e r i f i c a t i o n of f i n a l TSSs, or N.TSSs, may be a ch i e ved u s i n g I/O . sequences. Each d e f i n i t i o n of a minor s t a t e v a r i a b l e t ha t c o n t r i b u t e s to the N.TSS as w e l l as the d e f i n i t i o n of the STATE v a r i a b l e has to be v e r i f i e d . The STATE v a r i a b l e s can be v e r i f i e d the same way they are v e r i f i e d i n the UlOv-method. For the minor s t a t e v a r i a b l e s , an I/O path i s used to l e ad the d e f i n e d v a r i a b l e to a t r a n s i t i o n whose C.TSS con t a i n s a p r e d i c a t e which uses t h a t 49 Testing Extended F in i te State Machines v a r i a b l e d e f i n i t i o n . The d e f i n i t i o n of the minor s t a t e v a r i a b l e can then be v e r i f i e d u s i n g an I/O sequence t h a t ,begins a t t ha t C.TSS. R e f e r r i n g back to the f i n a l TSS f o r the a/3 t r a n s i t i o n where the STATE v a r i a b l e i s se t to s2 and c i s r e s e t t o 0. None of the C.TSSs i s i d e n t i c a l to i t ; however, the C.TSS s2 AND c<2 can v e r i f y t ha t c i s not a t 2 and STATE i s a t s2 ; as w e l l , the sequence b/0.b/0.b/3 beg inn ing from t h a t C.TSS ban v e r i f y t h a t c was indeed r e s e t to 0. Each e x e c u t i o n o f b/0 increments c by 1 and t r a n s i t i o n b/3 i s not p o s s i b l e u n l e s s c has reached 2 a f t e r two inc rements . As a r e s u l t , the subsequence b/0.b/0 would have incremented c to 2 i f i t were at 0 to beg in w i t h , and the I/O b/3 would v e r i f y t h a t c had been incremented to 2 c o r r e c t l y . Hence, the sequence can v e r i f y t h a t c was r e s e t to 0 c o r r e c t l y . S i m i l a r l y f o r the N.TSS s2 and c=c+l . The v a r i a b l e c can be v e r i f i e d t h a t i t i s incremented c o r r e c t l y by i n i t i a l l y s e t t i n g i t to 0, then to 1. When i t i s a t 0 and STATE i s a t s2 , the s i t u a t i o n i s i d e n t i c a l to tha t mentioned above and the sequence b/0 .b/0 .b/3 v e r i f i e s t ha t STATE i s a t s2 and t h a t c has been both se t to 0 c o r r e c t l y and incremented c o r r e c t l y . When c i s a t 1 and STATE i s a t s2 , the sequence b/0.b/3 v e r i f i e s t ha t STATE i s a t s2 and c i s incremented c o r r e c t l y . The b/0 t r a n s i t i o n increments c to 2, and the b/3 t r a n s i t i o n checks 50 Test ing Extended F in i t e State Machines t h a t c i s c o r r e c t l y a t 2. Hence, c must have been a t 1 to beg in w i t h . 3 .3 .2 .2 V e r i f i c a t i o n of C.TSSs V e r i f i c a t i o n of the s t a r t i n g TSS, or C .TSS , f o r a t r a n s i t i o n r e q u i r e s v e r i f y i n g t ha t the STATE v a r i a b l e i s c o r r e c t and any p r e d i c a t e i n v o l v i n g a minor s t a t e v a r i a b l e i s a l s o c o r r e c t . V e r i f i c a t i o n of the STATE v a r i a b l e i s aga in i d e n t i c a l to the. Uv and ~Uv procedures i n the UIOv-method. , V e r i f i c a t i o n of the p r e d i c a t e i s somewhat d i f f e r e n t . Two t h i n g s have to be checked i n the v e r i f i c a t i o n of a p r e d i c a t e : e f f e c t and c o r r e c t n e s s . The e f f e c t o f the p r e d i c a t e has to be checked , whenever p o s s i b l e , to d i s t i n g u i s h i t from o ther p r e d i c a t e s i n v o l v i n g the same minor s t a t e v a r i a b l e s . Th i s i s s i m i l a r to the STATE v a r i a b l e s be ing d i s t i n g u i s h e d from one ano the r . The d i s t i n g u i s h i n g procedure, i s a l s o an i d e n t i f i c a t i o n p rocess t h a t i d e n t i f i e s the STATE or the p r e d i c a t e by means o f an I/O sequence t ha t c h a r a c t e r i z e s the va lue of . the STATE v a r i a b l e or the presence of the p r e d i c a t e . For i n s t a n c e , r e f e r r i n g to the example i n Tab le 3 .1 , the p r e d i c a t e f o r t r a n s i t i o n a/0 can be d i s t i n g u i s h e d from t h a t f o r t r a n s i t i o n a/3 by s e t t i n g c to 0 or 1 and i n p u t t i n g the sequence a . a . a or a . a r e s p e c t i v e l y . The p r e d i c a t e f o r t r a n s i t i o n a/0 would 51 Test ing Extended F in i t e State Machines prompt the response 0 .0 .3 or 0.3 r e s p e c t i v e l y . The p r e d i c a t e f o r t r a n s i t i o n a/3 can be d i s t i n g u i s h e d from t h a t f o r a/0 by s e t t i n g c to 2 and then i n p u t t i n g a . a . a or a . a to the IUT. The response of the IUT would be 3 .- .- o r 3.- i f the p r e d i c a t e were c o r r e c t . Note t ha t both p r e d i c a t e s have to be v e r i f i e d s e p a r a t e l y the same way t ha t a l l STATE va lues have to be checked s e p a r a t e l y . S imply check ing one does not imply the o the r i s c o r r e c t . Check ing the p r e d i c a t e f o r t r a n s i t i o n a/3 can a l s o employ on l y the I/O sequence a/3. The I/O sequences used are thus UIOSs f o r the p r e d i c a t e s . The o the r i tem a p r e d i c a t e has to be checked f o r i s i t s c o r r e c t n e s s . For i n s t a n c e , i f s i AND c<4 c o n s t i t u t e an C.TSS t ha t enab les t r a n s i t i o n x, then t h i s i m p l i e s s i AND c=0, s i AND c = l , s i AND c = 2 and s i AND c = 3 are a l l capab le of e n a b l i n g x. . T o check t h a t the p r e d i c a t e has been implemented c o r r e c t l y , one way i s to check a l l these p o s s i b i l i t i e s . However, t h i s cou ld r e s u l t i n an ex t reme ly l eng thy t e s t sequence i f the p r e d i c a t e were c<100 i n s t e a d of 4. I n s t ead , the b o u n d a r y - i n t e r i o r va lue c r i t e r i o n can be used here and the p r e d i c a t e c<4 can be checked by s e t t i n g c to 0, 1, then 3 so t h a t the domain of the p r e d i c a t e can be e s t a b l i s h e d . The I/O sequence which c h a r a c t e r i z e s C.TSS s i AND c<4 can then be a p p l i e d to v e r i f y the response o f the IUT i n each case . Check ing f o r the c o r r e c t n e s s o f the 52 Testing Extended F in i t e State Machines p r e d i c a t e has to be cons ide r ed here i n the t e s t sequence g e n e r a t i o n procedure because s e t t i n g the TSS v a r i a b l e s to p a r t i c u l a r va lues may r e q u i r e c e r t a i n sequences o f I/Os to be implemented or c e r t a i n va lues be used at the t ime of i n p u t . Leav ing the v e r i f i c a t i o n procedure u n t i l the t e s t da ta s e l e c t i o n p rocess may be too l a t e s i n c e the I/O sequences have a l r e a d y been determined by t hen . 3 .3 .2 .3 UIOSs f o r TSSs . . In the same way UIOSs are used to v e r i f y s t a t e s , I/O sequences are used to v e r i f y minor s t a t e v a r i a b l e s . I f the v a r i a b l e s are " comp le te l y s p e c i f i e d , " then these I/O sequences must be un ique , as d i s c u s s e d above, so t h a t one p r e d i c a t e can be d i s t i n g u i s h e d from another i n v o l v i n g the same minor s t a t e v a r i a b l e s . For i n s t a n c e , r e f e r r i n g to Tab le 3 . 1 , . s i n c e s t a r t i n g TSSs s i AND c<2, s i AND c=2 and s i are a l l s p e c i f i e d , i f s i AND c=2 were used to v e r i f y a f i n a l TSS, then the I/O sequence tha t beg ins at t h a t TSS must not be a l s o p r o d u c i b l e a t the TSSs s i AND c<2 and s i ; o t h e r w i s e , when the I/O sequence i s obse rved , the c v a r i a b l e a t the IUT c o u l d have been at 2, l e s s than 2 or any v a l u e . The I/O sequence used must thus be unique to the s t a r t i n g TSS. In Tab le 3 .1 , t h i s uniqueness e x i s t s f o r a l l TSSs; t h a t i s , a t TSS s i and c<2, a/0 i s produced and i t i s not genera ted by 53 Testing Extended F in i te State Machines any o the r TSS. T h i s i m p l i e s the uniqueness of a/0 shou ld be checked , p r i o r to i t s use , the same way ~Uv checks the UIOSs f o r the STATE v a r i a b l e s , to ensure i t s un iqueness a l s o e x i s t s i n the IUT. I f TSSs s i AND c=2 and s i d i d not e x i s t , then a/0 would not have to be checked s i n ce i t does not have to d i s t i n g u i s h TSS s i AND c<2 from s i AND s i AND c=2. 3.3.3 The eUIOv-Method The extended UlOv-method, or eUIOv-method, i s the UIOv-method t a k i n g e x e c u t a b i l i t y and the TSS i n t o c o n s i d e r a t i o n . I t c o n s i s t s of the f o l l o w i n g p rocedures . Uv = preamble (s i )@UIOS(s i ) ~Uv = preamble (s i )@~UIOSs(s i ) where p reamb le ( s i ) denotes the preamble t ha t takes the EFSM from i t s i n i t i a l s t a t e to s t a t e s i ; "@" denotes c o n c a t e n a t i o n ; UIOS ( s i ) i s the UIOS be l ong ing to s i and ~UIOSs(s i ) are UIOSs tha t be long to o ther s t a t e s i n the FSM which shou ld not be p r o d u c i b l e by s i . Uv and ~Uv are done f o r each STATE i n the EFSM. Both procedures t o g e t h e r determine the minimum number of STATES i n the EFSM. The cho i ce of preamble ( s i ) f o r each s i must ensure t h a t the subsequent UIOS(s i ) and "U IOSs (s i ) are a l l e x e c u t a b l e . I f no such p reamb le ( s i ) e x i s t s , then e i t h e r another se t of UIOSs shou ld be used or a set o f I O ( s i , k ) s shou ld be used . 54 Test ing Extended F in i t e State Machines Uv and ~Uv must both be done because of the u n c e r t a i n t y of UIOSs w i thout t h e i r v e r i f i c a t i o n s as d i s c u s s e d i n Chapter 2. I f UIOSs are used f o r v e r i f y i n g TSS v a r i a b l e s , then t h e i r un iquenesses must a l s o be v e r i f i e d i n these p r o c e d u r e s . The next procedure i n the eUIOv-method i s t r a n s i t i o n t e s t i n g , or T t . The t e s t i n g of e. t r a n s i t i o n s w i l l be r e f e r r e d to as e T t . T t = (1). t . p r e a m b l e ( s i ) © t r a n s i t i o n ( s i , s f ) @ U I O S ( s f ) + (2) t .p reamble ( s i )@U IOS (s i ) eT t .= (1) pa r . p r eamb le ( s j )@de f- f r ee p a t h ( s j , s i ) @ . e . t r a n s i t i o n ( s i , s f ) @ U I O S ( s f ) + (2) pa r . p r eamb le ( s j )@de f- f r ee p a t h ( s j , s i ) @ UIOS(s i ) I f t . preamble ( s i ) i s equa l to preamble ( s i ) used i n Uv and ~Uv, then (2) i s not r e q u i r e d to v e r i f y i t s t a i l s t a t e to be s i a g a i n ; o the rw i se , v e r i f i c a t i o n i s r e q u i r e d as i n d i c a t e d by (2 ) . T r a n s i t i o n ( s i , s f ) denotes a t r a n s i t i o n t h a t beg ins a t s i and ends a t s t a t e s f . P a r .p reamb le ( s j ) i s a pa th t h a t beg ins a t the i n i t i a l s t a t e and ends a t s t a t e s j . De f - f r e e pa th ( s j , s i ) i s a path t ha t l eads from a t r a n s i t i o n t h a t s t a r t s a t s j to s i . That t r a n s i t i o n at s j houses the de f of the p-use appear ing i n e . t r a n s i t i o n . The t o t a l p reamble , which i s the p a r t i a l path concatenated w i th the d e f - f r e e p a t h , must a l s o have i t s t a i l s t a t e v e r i f i e d as i n d i c a t e d i n 55 Test ing Extended F in i t e State Machines (2 ) . T h i s i n essence i s check ing the s t a r t i n g s t a t e f o r e . t r a n s i t i o n ( s i , s f ) . I f the UIOSs c o n s i s t of e . t r a n s i t i o n s , then embedded w i t h i n the preambles must be de f s t h a t enab le those e. t r a n s i t i o n s . Th i s i s why i t i s p r e f e r a b l e to use s l i g h t l y l onge r UIOSs i f they do not have e . t r a n s i t i o n s i n v o l v e d . Dur ing e T t , a preamble t ha t enab les U lOS (s f ) as w e l l as e . t r a n s i t i o n ( s i , s f ) may not e x i s t . The l a s t procedure i n the eUIOv-method i s the v e r i f i c a t i o n of minor s t a t e v a r i a b l e s i n the TSSs i n each t r a n s i t i o n . msvv . = . t . p r e a m b l e ( s i ) © t r a n s i t i o n ( s i , s f ) @ d e f - f r e e pa th (s f , sk )@I/Os (msvf ) OR pa r . p r eamb le ( s j )@de f- f r ee p a t h ( s j , s i ) @ e . t r a n s i t i o n ( s i , s f ) @ d e f - f r e e pa th (s f , sk )@I/Os (msvf ) where I/Os (msvf) i s the sequence of I/Os to v e r i f y the d e f i n i t i o n of one or more minor s t a t e v a r i a b l e s i n t r a n s i t i o n ( s i , s f ) or e . t r a n s i t i o n ( s i , s f ) . The d e f - f r e e p a t h ( s f , s k ) l eads from s f to the e . t r a n s i t i o n s t a r t i n g a t sk which houses the p r e d i c a t e i n v o l v i n g the d e f i n i t i o n i n t r a n s i t i o n ( s i , s f ) or e . t r a n s i t i o n ( s i , s f ) . I f I/Os(msvf) has to be un ique , then the v e r i f i c a t i o n procedure i d e n t i c a l to Uv and ~Uv has to be c a r r i e d out f o r i t to check i t s un iqueness . P r e d i c a t e s i n the C.TSSs are a l s o v e r i f i e d i n 56 Testing Extended F in i te State Machines t h i s procedure u s i n g the methodology d i s c u s s e d i n the p r e v i ous s e c t i o n . To r e t u r n to the i n i t i a l i d l e s t a t e , i f the r e s e t f e a t u r e r/- i s not a v a i l a b l e , then a sequence of I/Os has t o be used to b r i n g the machine back to the i n i t i a l s t a t e . These sequences of I/Os shou ld be v e r i f i e d p r i o r to t h e i r uses to ensure they end a t the i n i t i a l s t a t e . T h e i r v e r i f i c a t i o n can be done as f o l l ows f o r a s t a t e s i i n the EFSM. . p reamble (s i )@postamble (s i )@UIOS ( id le ) Parameter v a r i a t i o n methods such as the boundary-i n t e r i o r va lue c r i t e r i o n or the most commonly used va lues can be used d u r i n g the t e s t sequence g e n e r a t i o n procedure to ach ieve more thorough t e s t i n g , i n such c a s e s , t e s t sequences may be repea ted to accommodate the v a r i ous va lues s e l e c t e d . 3.3.4 An Example The eUIOv-method i s a p p l i e d to the EFSM i n Tab le 3.1 as an example. The i n i t i a l s t a t e i s taken to be s i and the c v a r i a b l e i s assumed to be i n i t i a l i z e d to 0 a t the b e g i n n i n g of each imp lementa t ion . The r e s e t f e a tu r e r/- i s assumed to e x i s t to b r i n g each s t a t e i n the EFSM back to s i . I t s v e r i f i c a t i o n i s assumed to be c o r r e c t . 57 Testing Extended F in i t e State Machines The UIOSs f o r s i and s2 are b/- and a/- r e s p e c t i v e l y . The UIOSs f o r v e r i f y i n g c<2 at STATE s i s t a r t s w i th a/0 and f o r c=2 at s i i s a/3. T h e i r uniqueness need not be v e r i f i e d s e p a r a t e l y i n the ~Uv procedure s i n ce they share i d e n t i c a l i n p u t s . The UIOSs f o r v e r i f y i n g c<2 at s2 s t a r t s a t b/0 and f o r c = 2 a t s2 i s b/3; a g a i n , t h e i r un iqueness are a l r e a d y conf i rmed i n the Uv p rocedure . The UIOSs f o r v e r i f y i n g d i f f e r e n t c , v a l u e s at the same STATES thus need be v e r i f i e d on l y i n Uv. No preamble i s r e q u i r e d to go to s i . The preamble f o r . s2 i s . a/0 . a/0 . a/3 . . T r a n s i t i o n s a/3, b/0 and b/3 are e . t r a n s i t i o n s and they r e q u i r e the f o l l o w i n g preambles to ensure t h e i r e x e c u t a b i l i t i e s . The preambles are found by t r a v e r s i n g backwards from each e . t r a n s i t i o n to the i n i t i a l s i s t a t e . The p r e d i c a t e s i n the e . t r a n s i t i o n are c o n s i d e r e d and those t r a n s i t i o n s whose N.TSSs enab le these p r e d i c a t e s are t r a c k e d and i n c l u d e d i n the p reambles . preamble(a/3) = a/0.a/0 preamble(b/0) = a/0.a/0.a/3 preamble(b/3) = a /0 . a /0 . a /3 .b/0 .b/0 The f o l l o w i n g t e s t subsequence c o n s t i t u t e the Uv and ~Uv procedure f o r the EFSM i n Tab le 1. Uv: b/-a / 0 . a / 0 . a / 3 . a / - . r / -a/O.r/-58 Test ing Extended F in i te State Machines a / 0 . a / 0 . a / 3 . r / -a / 0 . a / 0 . a / 3 . b / 0 . r / -a / 0 . a / 0 . a / 3 . b / 0 . b / 0 . b / 3 ~Uv: a/O.r/-a / 0 . a / 0 . a / 3 . b / 0 . r / -{The f o l l o w i n g v e r i f i e s the s p e c i a l preambles. } a / 0 . a / 0 . b / - . r / -. a /0 . a/0 . a/3 . a / - . r / -a / 0 . a / 0 . a / 3 . b / 0 . b / 0 . a / - . r / -The f o l l o w i n g t e s t subsequence c o n s t i t u t e s the T t , eT t and msvv p rocedu res . The, i n f o r m a t i o n i n the p a r e n t h e s i s i n d i c a t e the N.TSS to be v e r i f i e d i n the t r a n s i t i o n under t e s t . In t h i s p a r t i c u l a r example, the msvv p rocedure to v e r i f y TSSs i s c a r r i e d out w i th the eTt procedure whenever p o s s i b l e to reduce the l e n g t h of the f i n a l t e s t sequence. S ince a l l the preambles used have a l r e ady been v e r i f i e d i n the Uv and ~Uv p rocedure , they do not have to be v e r i f i e d here a g a i n . T t : b /- ( s l ) . b /-a / 0 . a / 0 . a / 3 . a / - ( s 2 ) . a / - . r / -eTt & msvv: a /0 ( s l AND c=l ) .b/-.a/0{c=2} . a/3 . r/-a/0 .a/0 .a/3 (s2 AND c=0).a/-.b/0{c=1}. b/0{c=2}.b/3 59 Test ing Extended F in i te State Machines a/0 .a/0 .a/3 .b/0 ( s2 AND c=1).a/-.b/0{c=2}. b/3 a / 0 . a / 0 . a / 3 . b / 0 . b / 0 . b / 3 ( s l AND c=0) .b/- . a/0{c=l} .a/0{c=2}.a/3.r/-A l though the UIOSs b/- and a/- f o r STATES s i and s2 are used to v e r i f y the STATEs i n d i c a t e d i n the pa ren theses above, the STATES can a l s o be v e r i f i e d at the same t ime the c v a r i a b l e s are v e r i f i e d i n t h i s p a r t i c u l a r case s i n c e the UIOSs_ f o r the c v a r i a b l e s are capable of d i s t i n g u i s h i n g a m o n g . . d i f f e r e n t c v a r i a b l e s as w e l l as among d i f f e r e n t STATEs. . However, i f these UIOSs are used f o r t h i s pu rpose , they shou ld f i r s t be v e r i f i e d i n procedure ~Uv to ensure they indeed have these c a p a b i l i t i e s . Va lues of the c v a r i a b l e s t ha t have to be v e r i f i e d are r e co rded i n b races to t r a c k the v e r i f i c a t i o n p rocedure . ' For i n s t a n c e , {c=2} t r a c k s the c v a r i a b l e wh i l e i t i s be ing incremented by one. The va lue o f the inc rement , i n t u r n , i s v e r i f i e d by the t r a n s i t i o n t h a t i s enab led when c = 2. V e r i f i c a t i o n of the e f f e c t of the p r e d i c a t e s i s i m p l i e d i n t h i s example i n the v e r i f i c a t i o n of the d e f i n i t i o n s of the c o r r e s p o n d i n g v a r i a b l e s . Domains of the p r e d i c a t e s are a l s o i m p l i c i t l y v e r i f i e d i n the eTt and msvv procedure above where c was se t to 0 f i r s t , then to 1. 60 Test ing Extended F in i te State Machines The f i n a l t e s t sequence may be reduced by e l i m i n a t i n g those t e s t subsequences tha t are comp le te l y c o n t a i n e d i n o the r subsequences. The c o n c l u s i o n one can draw from a t e s t t h a t uses the t e s t sequence generated above i s tha t i f the EFSM has o n l y two s t a t e s , then an IUT tha t passes the above t e s t possesses an EFSM s k e l e t o n i d e n t i c a l to the s p e c i f i e d EFSM. The number of s t a t e s must aga in be r e s t r i c t e d to be equa l to t h a t i n the s p e c i f i c a t i o n . T h i s aga in i m p l i e s t he re may e x i s t e x t r a t r a n s i t i o n s i n the IUT t h a t are not i n the EFSM s p e c i f i c a t i o n . 3.3.5 Summary Of The eUIOv-Method The eUIOv-method i s e s s e n t i a l l y a check ing exper iment t h a t checks an IUT f o r each EFSM t r a n s i t i o n g i ven i n the s p e c i f i c a t i o n . The Uv and ~Uv procedures i n the eUIOv-method e s t a b l i s h the minimum number of s t a t e s i n the EFSM and they v e r i f y the uniqueness of the UIOSs. The T t and eTt p rocedures check each t r a n s i t i o n s p e c i f i e d i n the EFSM by o b s e r v i n g i t s c u r r e n t and f i n a l STATE va lues as w e l l as i t s I/O o p e r a t i o n s . The msvv procedure checks the d e f i n i t i o n s of minor s t a t e v a r i a b l e s t ha t c o n t r i b u t e to the N.TSS o f a t r a n s i t i o n . Whenever p o s s i b l e , these d e f i n i t i o n s are v e r i f i e d to be c o r r e c t . The minor s t a t e v a r i a b l e s t h a t 61 Test ing Extended F in i te State Machines c o n t r i b u t e to the C.TSS of a t r a n s i t i o n are a l s o checked f o r t h e i r c o r r e c t n e s s and t h e i r e f f e c t s . T h e i r e f f e c t s are checked by d i s t i n g u i s h i n g p r e d i c a t e s i n v o l v i n g i d e n t i c a l minor s t a t e v a r i a b l e s and STATE v a r i a b l e s from one ano the r . T h e i r c o r r e c t n e s s are checked u s i n g two boundary v a l ues and an i n t e r i o r va lue to e s t a b l i s h the domains of the p r e d i c a t e s whenever necessa r y . The eUIOv-method r e q u i r e s t ha t va lues of minor s t a t e v a r i a b l e s t ha t c o n t r i b u t e to C.TSSs are t r a c k e d d u r i n g the t e s t sequence gene r a t i on procedure i n o rde r to ensure e x e c u t a b i l i t y o f the f i n a l t e s t sequence and chosen va lues f o r t e s t i n g p r e d i c a t e domains are s e l e c t e d . The t r a c k i n g procedure may r e q u i r e some computat ions as w e l l as p r e -s e l e c t i o n of t e s t d a t a . The eUIOv-method thus coup les the t e s t sequence s e l e c t i o n p rocess w i th the t e s t da ta s e l e c t i o n p rocess whenever necessa r y . These two p rocesses are t r a d i t i o n a l l y c a r r i e d out s e p a r a t e l y i n sof tware t e s t i n g where the t e s t sequences generated may face e x e c u t a b i l i t y prob lems. 3.4 FAULT COVERAGE The eUIOv-method i s based on the UlOv-method; hence , i t produces a f a u l t coverage t ha t i n c l u d e s t h a t which i s produced by the UlOv-method. T h i s i m p l i e s the eUIOv-method 62 Test ing Extended F in i te State Machines i s a l s o capab le of d e t e c t i n g a l l I/O e r r o r s and STATE e r r o r s i n an EFSM p rov ided i t s set o f STATES i s no g r e a t e r than t ha t which i s i n the s p e c i f i c a t i o n . T h i s a l s o i m p l i e s e x t r a I/Os p resen t i n the IUT w i l l not be d e t e c t e d . However, r e f e r r i n g to the term " con formance , " and g i v e n the l i m i t a t i o n s of t e s t i n g , t h i s i s a c c e p t a b l e . As f o r the t e s t i n g of the TSS v a r i a b l e s , a g a i n , e x t r a s tatements cannot be d e t e c t e d . The e f f e c t s of e x t r a statements are d i s c u s s e d i n g r e a t e r d e t a i l i n the next chap te r . I f the p r e d i c a t e s c o n s t i t u t i n g the C.TSSs i n v o l v e mathemat ica l e x p r e s s i o n s , or i f v a r i a b l e s i n the N.TSSs are a s s i gned new va lues w i th mathemat ica l e x p r e s s i o n s , then t h e i r c o r r e c t n e s s may not be guaranteed even though they may d i s p l a y c o r r e c t v a l ues d u r i n g t e s t i n g . Th i s i s s u e w i l l a l s o be d i s c u s s e d i n g r e a t e r d e t a i l s i n the next chap te r . 63 4 DATA FLOW TESTING Whi le s imple p r o t o c o l s can be mode l led by FSMs, the more complex ones r e q u i r e EFSMs to a c c u r a t e l y d e s c r i b e t h e i r f u n c t i o n s and b e h a v i o r s . EFSM models a l o n e , however, cannot d e t a i l the f low of i n f o r m a t i o n tha t o f t e n takes p l a c e from one c o n t r o l phase to another . For i n s t a n c e , i n p u t p r i m i t i v e s o f t e n have accompanying parameters t h a t are i n p u t a t one c o n t r o l phase and s to r ed by the IUT i n the form of a v a r i a b l e f o r usage or r e f e r e n c e i n another c o n t r o l phase . I n s t ead , the f u n c t i o n s of these parameters and v a r i a b l e s can be s e p a r a t e l y d e s c r i b e d i n a da ta f low t r a n s i t i o n embedded w i t h i n the a p p r o p r i a t e EFSM t r a n s i t i o n . These parameters and v a r i a b l e s shou ld a l s o be checked d u r i n g t e s t i n g to ensure t h e i r f u n c t i o n s are c o r r e c t l y c a r r i e d out and the output p r i m i t i v e s are accompanied by the c o r r e c t pa ramete rs . T h i s check ing p rocess can be accompl i shed by means of a da ta f low t e s t i n g p rocedure . An overv iew of the da ta f low t e s t i n g procedure g i v e s a p rocess s i m i l a r to the msvv procedure i n the eUIOv-method, except he re , i n s t e a d of a path t r a c k i n g the d e f i n i t i o n o f a TSS minor s t a t e v a r i a b l e to i t s usage, each da ta pa th t r a c k s the d e f i n i t i o n of a parameter or a v a r i a b l e to i t s usage. Each path i s e x e r c i s e d and v e r i f i e d whenever p o s s i b l e d u r i n g t e s t i n g to ensure the d e f i n i t i o n , or usage, under t e s t i s 64 Data Flow Test ing c o r r e c t . Any p r e d i c a t e tha t appears i n the da ta f low t r a n s i t i o n s a l s o has i t s e f f e c t and c o r r e c t n e s s v e r i f i e d the same way they are v e r i f i e d i n the msvv p rocedure . The da ta f low t e s t i n g techn ique i s based on s t a t i c da ta f l ow a n a l y s i s . I t i s a l s o based on the l e s s o n l e a r n t from FSM t e s t i n g t h a t t r a n s i t i o n e x e r c i s i n g a lone i s not enough, whenever i t i s p o s s i b l e , e lements t ha t are not d i r e c t l y obse r vab l e i n each t r a n s i t i o n shou ld be v e r i f i e d as w e l l . 4.1 STATIC DATA FLOW ANALYSIS S t a t i c da ta f low a n a l y s i s o r i g i n a t e d i n comp i l e r o p t i m i z a t i o n [Hech77]. I t was a p p l i e d to sof tware t e s t i n g i n [Rapp85] and i s now g e n e r a l l y accepted as a s t r u c t u r a l t e s t i n g s t r a t e g y [Weis85]. E s s e n t i a l l y , s t a t i c da ta f low a n a l y s i s t r a c k s each i n p u t v a r i a b l e through a program u n t i l i t i s u l t i m a t e l y used to produce output v a l u e s . A s s o c i a t i o n s between the d e f i n i t i o n o f , or the assignment of a va lue t o , a v a r i a b l e and the usage of t ha t v a r i a b l e are i d e n t i f i e d and examined d u r i n g t e s t i n g . The concept i s based on each d e f i n e d v a r i a b l e must r each a use wh i l e each v a r i a b l e t o be used must have been p r e v i o u s l y d e f i n e d . The f o l l o w i n g d e f i n i t i o n s are i n t r o d u c e d to enhance subsequent d i s c u s s i o n s . In s t a t i c da ta f low a n a l y s i s 65 Data Flow Test ing t e r m i n o l o g y , the p rocess of a s s i g n i n g a va lue to a v a r i a b l e i s c a l l e d the d e f i n i t i o n , or d e f , o f the v a r i a b l e . The use of the v a r i a b l e i n a p r e d i c a t e i s c a l l e d a p-use. The use of the v a r i a b l e i n de te rm in ing the def of another v a r i a b l e i s c a l l e d a c-use [Rapp85]. U r a l [Ural88] was the f i r s t to app ly s t a t i c da ta f l ow a n a l y s i s to the conformance t e s t i n g of p r o t o c o l s . The r e s u l t was a method of gene ra t i ng t e s t sequences based on r i g o r o u s l y - d e f i n e d da ta f low r e l a t i o n s h i p s which a l l ow e a s i e r i n t e r p r e t a t i o n of t e s t r e s u l t s . In compar ison w i t h the method proposed by Sa r i kaya [ S a r i 8 7 ] , t h i s method genera tes more comprehensive t e s t s i n terms of s t r u c t u r a l coverage ; and i n terms of f u n c t i o n a l cove rage , S a r i k a y a 1 s was more complete [U ra l88 ] . 4.2 DATA FLOW PATHS In a p r o t o c o l , a da ta f low path f o r a p a r t i c u l a r parameter or v a r i a b l e r e f e r s to a sequence o f da ta f l ow t r a n s i t i o n s where the f i r s t t r a n s i t i o n con t a i n s a d e f i n i t i o n of the parameter or v a r i a b l e and the l a s t t r a n s i t i o n con t a i n s a usage of t ha t parameter or v a r i a b l e . These two t r a n s i t i o n s are connected by a sequence of t r a n s i t i o n s based on the u n d e r l y i n g EFSM m o d e l l i n g the c o n t r o l s t r u c t u r e of the p r o t o c o l . 66 Data Flow Test ing A da ta f low path of l eng th one i s a pa th embodied w i t h i n the same data f low t r a n s i t i o n ; t ha t i s , the usage of the v a r i a b l e or parameter immediate ly f o l l o w s i t s d e f i n i t i o n . T h i s type of f low path i s e x e r c i s e d whenever the EFSM t r a n s i t i o n i s execu ted . Data f low paths which extend from one EFSM t r a n s i t i o n to another r e q u i r e t ha t the p a r t i c u l a r sequence o f t r a n s i t i o n s be examined d u r i n g t e s t i n g . T h i s sequence may or may not a l r e ady be covered d u r i n g EFSM t e s t i n g . T h i s type of f low path i s r e f e r r e d to as " i n t e r - t r a n s i t i o n a l " [Chan89a] and r e q u i r e s i d e n t i f y i n g the t r a n s i t i o n a t which the d e f i n i t i o n f i r s t o c c u r s , the t r a n s i t i o n a t which the usage o c c u r s , and connec t i ng these two t r a n s i t i o n s w i t h a pa th based on the c o n t r o l s t r u c t u r e . The pa th must be execu tab l e and i t must be f r e e of any r e - d e f i n i t i o n o f the v a r i a b l e or parameter ; t ha t i s , the d e f i n i t i o n i s " l i v e " i n the connec t i ng pa th . 4.3 DATA FLOW TESTING In t e s t i n g the da ta f low of a p r o t o c o l , the v a r i a b l e s and parameters tha t appear i n the data f low t r a n s i t i o n s embedded w i t h i n the EFSM t r a n s i t i o n s are t r a c k e d from the moment they are d e f i n e d u n t i l they are used e i t h e r f o r computa t iona l purposes or as p r e d i c a t e s . When computat ions 67 Data Flow Test ing e v e n t u a l l y l e a d to the d e f i n i t i o n of an output p r i m i t i v e parameter , the path i s f u r t h e r extended to t h a t parameter i n o rde r t h a t the computat ions may be v e r i f i e d to be c o r r e c t . I f v e r i f i c a t i o n i s not p o s s i b l e , the f low paths would on l y be e x e r c i s e d ; they s top at the usage of the v a r i a b l e or parameter . For p r e d i c a t e u ses , the v a r i a b l e or parameter i n v o l v e d may not be v e r i f i a b l e i n terms of e x t e r n a l l y obse rvab le e ven t s , i n which case the f low path aga in would on l y be e x e r c i s e d and stops at the t r a n s i t i o n c o n t a i n i n g the p r e d i c a t e . I f v e r i f i c a t i o n i s p o s s i b l e , where the a c t i o n s enab led by d i f f e r e n t p-uses d i f f e r and are man i f e s t ed i n e x t e r n a l l y obse rvab le e ven t s , then these events would be checked to v e r i f y the p-uses. For i n s t a n c e , a d i f f e r e n t va lue a s s i gned to an output parameter depending on the p r e d i c a t e c o n s t i t u t e s an e x t e r n a l l y obse r vab l e even t . Usages are thus aga in v e r i f i e d a c c o r d i n g to the e f f e c t s they have on de te rm in ing va lues f o r the I/Os or the o rde r i n which they appear . The c o r r e c t n e s s of these usages may be v e r i f i e d d u r i n g the t e s t da ta s e l e c t i o n p rocedure by s e l e c t i n g a p p r o p r i a t e va lues f o r t e s t i n p u t s . The boundary-i n t e r i o r va lue c r i t e r i o n can aga in be used f o r the p r o c e s s . However, i f s p e c i a l preambles are r e q u i r e d so t h a t the p r e d i c a t e s , w i th s e l e c t e d va lues a s s igned to the v a r i a b l e s i n v o l v e d , may be enab l ed , then they must be c o n s i d e r e d aga in 68 Data Flow Test ing d u r i n g the sequence gene r a t i on procedure to ensure the f i n a l t e s t sequence i s execu t ab l e . I t shou ld be noted t h a t i n a p r o t o c o l s p e c i f i c a t i o n , not a l l de f s are n e c e s s a r i l y used i n which case f low paths do not e x i s t f o r those d e f s . An example of t h i s type o f de f i s a def f o r the purpose of i n i t i a l i z i n g a v a r i a b l e where the i n i t i a l i z e d va lue i s not used . Whi le there may be more than one def of a v a r i a b l e , the re may a l s o be more than one usage of i t . Each de f shou ld be e x e r c i s e d and v e r i f i e d at l e a s t once ; the same a p p l i e s f o r each use . More than one usage may e x i s t f o r a s i n g l e de f o f a v a r i a b l e ; hence , some usages may not be t e s t e d i f paths were formed from the de f s a lone s i n ce the number of paths would then be l i m i t e d by the number of d e f s . Hence, usages t h a t have been missed shou ld be t r a cked back to t h e i r a p p r o p r i a t e de f s to form a d d i t i o n a l f low paths so t h a t they can be v e r i f i e d as w e l l . When the usages are p-uses, they r e q u i r e t h a t the de f s produce s p e c i f i c va lues co r r e spond ing to those i n the p-uses . In these c a s e s , the search f o r a def o f the v a r i a b l e must take i n t o c o n s i d e r a t i o n the va lue t ha t i s a s s i g n e d to the v a r i a b l e . S i m i l a r l y , i f a p-use were to v e r i f y a de f s ta tement , the va lue of the def must be c o n s i d e r e d t o ensure Data Flow Test ing e x e c u t a b i l i t y . When the usages are c-uses , the va lues t h a t a r i s e from the def statements are not c r i t i c a l i n the t e s t sequence gene r a t i on p r o c e s s . 4.4 THE DATA FLOW TESTING PROCEDURE As p r e v i o u s l y ment ioned, the procedure f o r t e s t i n g da ta f lows (DFTP) i s s i m i l a r to the msvv procedure i n the eUIOv-method except a l l parameters and v a r i a b l e s are c o n s i d e r e d . A l l f low paths t h a t beg in at t r a n s i t i o n ( s i , s f ) , f o r t e s t i n g the de f s of v a r i a b l e s i n t ha t t r a n s i t i o n , are appended to the a p p r o p r i a t e preambles to form a t e s t subsequence i n the f o l l o w i n g manner. The " d e f - f r e e DF pa th " i n d i c a t e s the pa th t h a t b r i n g s the t r a n s i t i o n , which houses the d e f , t o the t r a n s i t i o n tha t uses or v e r i f i e s , i f p o s s i b l e , the v a r i a b l e . The l a t t e r t r a n s i t i o n i s i n c l u d e d i n the pa th . DFTP = p r e a m b l e ( s i ) © t r a n s i t i o n ( s i , s f ) @ d e f - f r e e DF pa th ( t r ans i t i on )@pos t amb le OR pa r . p r eamb le ( s j )@de f- f r ee p a t h ( s j , s i ) @ e . t r a n s i t i o n ( s i , s f ) @ d e f - f r e e DF path ( e . t r ans i t i on )@pos t amb le The same a p p l i e s to the f low paths t ha t t e s t the usages of v a r i a b l e s i n t r a n s i t i o n ( s i , s f ) or e . t r a n s i t i o n ( s i , s f ) . The t e s t subsequences they form are i n the f o l l o w i n g fo rmat . 70 Data Flow Test ing DFTP = preamble (sk )@def-f ree DF p a t h ( s k , s i ) © t r a n s i t i o n ( s i , s f ) @ p o s t a m b l e ( s f ) OR pa r . p r eamb le ( s j )@de f- f r ee p a t h ( s j , s k ) @ @def-free DF p a t h ( s k , s i ) @ e . t r a n s i t i o n ( s i , s f ) @postamble(sf ) The " d e f - f r e e DF pa th " here i s the d e f - f r e e pa th t h a t i n c l u d e s the t r a n s i t i o n hous ing the def of the v a r i a b l e , and which connects the t r a n s i t i o n to the t r a n s i t i o n where the usage i s , t r a n s i t i o n ( s i , s f ) . The paths to t r a n s i t i o n ( s i , s f ) and e . t r a n s i t i o n ( s i , s f ) are p r e f e r a b l y those p r e v i o u s l y used i n the T t and eTt p rocedu res . I f new paths are u s ed , perhaps due to e x e c u t a b i l i t y problems i n the d e f - f r e e DF paths or due to usage r equ i r ements , then the t a i l s t a t e s o f these new "preambles " to t r a n s i t i o n ( s i , s f ) or e. t r a n s i t i o n ( s i , s f ) must be v e r i f i e d to ensure they end a t the c o r r e c t s t a t e so t ha t da ta f low paths used to v e r i f y de f s of v a r i a b l e s (def- i tDFPs ) are spanned from the c o r r e c t t r a n s i t i o n , and paths used to v e r i f y uses of v a r i a b l e s (use-i tDFPs ) are v e r i f y i n g uses s i t u a t e d a t the c o r r e c t t r a n s i t i o n s . The EFSM t a b l e used i n the eUIOv-method i s augmented w i th e n a b l i n g c o n d i t i o n s f o r the da ta f low t r a n s i t i o n s to a i d i n de te rm in ing executab le f low paths between two 71 > Data Flow Test ing s e l e c t e d da ta f low t r a n s i t i o n s . I f the da ta f low t r a n s i t i o n i s preceded w i th a p r e d i c a t e i n v o l v i n g minor s t a t e v a r i a b l e s , then t h e i r p-uses and de fs would be e x t r a c t e d t o form new TSSs i n the EFSM t a b l e . New columns or rows may thus be added i n the augmented t a b l e a long w i th new t a b l e e n t r i e s . Those p r e d i c a t e s t ha t i n v o l v e i n p u t parameters would be i n d i c a t e d i n the a p p r o p r i a t e t a b l e e n t r i e s to r e f l e c t s p e c i f i c va lues are r e q u i r e d at the t ime of i n p u t d u r i n g t e s t i n g . 4.5 AN EXAMPLE The f o l l o w i n g i s a s imple example to i l l u s t r a t e the DFTP. R e f e r r i n g back to the EFSM t a b l e i n Tab le 3 .1 , l e t the re be da ta f low t r a n s i t i o n s added to the EFSM t r a n s i t i o n s as f o l l o w s . The da ta f low t r a n s i t i o n s are denoted by DF and are enc l o sed i n a b l o ck d e l i m i t e d by BEGIN . . . END. Each EFSM t r a n s i t i o n i s i d e n t i f i e d by a number, t r a n s i t i o n 1: IN: a ( a . addr ) C.TSS: S i AND c<2 N.TSS: S i AND c:=c+l OUT: O(a .addr ) t r a n s i t i o n 2: IN: b (b .addr ) C.TSS: s i N.TSS: s i 72 Data Flow Test ing OUT: -t r a n s i t i o n 3: IN: a ( a . addr ) C.TSS: s i AND c = 2 N.TSS: S 2 AND c : = 0 DF: BEGIN address :=a .addr END OUT: 3 (a .addr ) t r a n s i t i o n 4: IN: a ( a . addr ) C.TSS: s 2 N.TSS: s 2 OUT: -t r a n s i t i o n 5: IN: b (b .addr ) C .TSS : S 2 AND c < 2 N.TSS: S 2 AND c:=c+l OUT: O(b.addr ) t r a n s i t i o n 6: IN: b (b .addr ) C.TSS: s 2 AND c = 2 N.TSS: S i AND c : = 0 DF: BEGIN 3 . add r :=b . add r©address END OUT: 3 (3 .addr ) The f low of each a . addr and b .addr to an output parameter i n t r a n s i t i o n s 1, 3 and 5 can be v e r i f i e d by s imp ly execu t i ng the t r a n s i t i o n s and o b s e r v i n g t h a t the output parameters enc losed i n p a r e n t h e s i s are c o r r e c t d u r i n g the EFSM t e s t i n g p rocedure . In t r a n s i t i o n 3, a . addr had to 73 Data Flow Test ing be remembered by the address v a r i a b l e so t ha t i t may be used l a t e r i n t r a n s i t i o n 6 to be appended to b .addr to form the output parameter 3 .addr . In EFSM t e s t i n g , t h i s f l ow of i n f o r m a t i o n may have been i gno red s i n ce i t r e q u i r e s a p a r t i c u l a r sequence of t r a n s i t i o n s to o c cu r . The DFTP i s thus a p p l i e d here to check t h i s f low of d a t a . A da ta f l ow path which connects t r a n s i t i o n 3 to t r a n s i t i o n 6 i s 3 . 5 . 5 . 6 . o r , i n terms of an I/O sequence, a / 3 . b / 0 . b / 0 . b / 3 . T h i s pa th t r a c k s the def of the address v a r i a b l e i n t r a n s i t i o n 3 to i t s usage i n t r a n s i t i o n 6. S ince the v a r i a b l e i s then used to compute the output parameter 3. addr , the def of the v a r i a b l e can be v e r i f i e d by obse r v i ng the va lue o f the v a r i a b l e , 3 .addr . I f t h i s da ta f low path were not i n c l u d e d i n the EFSM t e s t i n g p r o c e s s , then i t would be t e s t e d s e p a r a t e l y i n the DFTP by b u i l d i n g a preamble t h a t b r i n g s the EFSM from i t s i n i t i a l s i s t a t e to the TSS t h a t enab les t 3 , and conca t ena t i ng the preamble t o the da ta f low pa th t o form the f o l l o w i n g t e s t subsequence. DFTP: a / 0 . a / 0 . a / 3 . b / 0 . b / 0 . b / 3 The above t e s t subsequence t e s t s the c o r r e c t n e s s o f the def o f the v a r i a b l e add ress ; i t a l s o t e s t s the c o r r e c t n e s s o f i t s usage. In a d d i t i o n , from t h i s t e s t subsequence, i t can be seen tha t the i npu t parameters a .addr and b .addr are used c o r r e c t l y to form the output parameter 3 .addr . 74 Data Flow Test ing 4.6 CHAPTER SUMMARY The da ta f low t e s t i n g procedure i s based on s t a t i c da ta f low a n a l y s i s and the l e s sons l e a r n t from FSM t e s t i n g . I t i s d i f f e r e n t from s t a t i c da ta f low a n a l y s i s because a de f i s not merely t r a c e d to i t s usage, but i t i s v e r i f i e d as w e l l whenever p o s s i b l e . S i m i l a r l y , a usage i s not j u s t e x e r c i s e d but i t s e f f e c t a l s o v e r i f i e d whenever p o s s i b l e . When the usage i s a p-use, the re are two th i ngs t ha t can be checked : i t s e f f e c t and i t s c o r r e c t n e s s . I t s c o r r e c t n e s s can be v e r i f i e d by a p p l y i n g parameter v a r i a t i o n methods as d i s c u s s e d i n the p rev ious chapter to e s t a b l i s h the domain of the p r e d i c a t e and then by obse r v i ng i t s e f f e c t s , v i a i t s c h a r a c t e r i z i n g I/O sequence, to v e r i f y i t s e x i s t e n c e i n the IUT. When the usage i s a c-use and i f i t i n v o l v e s mathemat ica l exp re s s i ons or o the r parameters or v a r i a b l e s , then i t s c o r r e c t n e s s i s more d i f f i c u l t to check. T h i s i s d i s c u s s e d i n g r e a t e r d e t a i l s i n the next s e c t i o n . The e f f e c t s of usages are v e r i f i e d as f o l l o w s . When a v a r i a b l e i s used as a c-use and i t d e f i n e s an ou tput p r i m i t i v e parameter , the parameter would be t r a c k e d and observed to v e r i f y the c o r r e c t n e s s of the def and the c-use of the v a r i a b l e . When the usage i s a p-use, then the e f f e c t s among d i f f e r e n t p-uses of the same v a r i a b l e a t the same TSS are compared and whenever p o s s i b l e , these e f f e c t s 75 Data Flow Test ing are t r a c k e d to v e r i f y the e f f e c t of the p-use. For i n s t a n c e , i f the p r e d i c a t e x=2 enab les the ass ignment statement y :=2, and the p r e d i c a t e x<>2 enab les the ass ignment statement y :=4, then i f the v a r i a b l e y were used to compute an output parameter i n another t r a n s i t i o n , t h i s output parameter would be t r a cked and i t s va lue checked to ensure t h a t y was a s s igned the c o r r e c t va lue c o r r e s p o n d i n g to the a p p r o p r i a t e p r e d i c a t e i n v o l v i n g the v a r i a b l e x. I f , however, the v a r i a b l e y i s i t s e l f used i n a p-use, then the d i f f e r e n t p-uses of y and t h e i r d i f f e r e n t e f f e c t s would aga in be t r a c k e d u n t i l they are e x t e r n a l l y obse r vab l e or u n t i l they are proved to be n o n - v e r i f i a b l e by l o o p i n g back to the i n i t i a l p-uses f o r the v a r i a b l e x, i n which c a se , the p-use of x would on l y be e x e r c i s e d . The DFTP employs the same method of g e n e r a t i n g t e s t subsequences as t ha t used i n the msvv procedure i n the eUIOv-method. The r e s u l t i s t ha t a def t h a t was not v e r i f i e d i n the EFSM t e s t i n g procedure i s now v e r i f i e d i n da ta f low t e s t i n g and the preamble ensures t h a t i t i s l o c a t e d a t the expected t r a n s i t i o n . The same a p p l i e s to the usages t h a t were missed by the eUIOv-method. The preambles i n t h e i r t e s t subsequences ensure t ha t the usages are s i t u a t e d at the c o r r e c t t r a n s i t i o n s . 76 Data Flow Test ing 4.7 COMMENTS ON THE DFTP The DFTP can d e t e c t e r r o r s i n the de f s and usages of v a r i a b l e s p rov ided they are e x t e r n a l l y obse r vab l e or v e r i f i a b l e and no e x t r a def or usage statements e x i s t i n the IUT. Erroneous de fs or usages of v a r i a b l e s or parameters t ha t cannot be e x t e r n a l l y observed and v e r i f i e d may escape d e t e c t i o n . The p o s s i b l e e f f e c t s of e x t r a def s tatements i n an IUT are as f o l l o w s . As an example, c o n s i d e r a d e f - f r e e pa th t l . t 2 . t 3 . t 4 where a def o f a v a r i a b l e i n t l i s to be v e r i f i e d by i t s use i n t 4 . A c c o r d i n g to the s p e c i f i c a t i o n , i f the IUT were c o r r e c t l y implemented, then the de f i s indeed i n t l and the use i n t4 indeed v e r i f i e s i t . However, i f t3 e r r o n e o u s l y r e d e f i n e d the v a r i a b l e i n the IUT, which i s unknown to and unexpected by the t e s t e r , the usage i n t4 would have v e r i f i e d the def i n t3 i n s t e a d of the one i n t l as expec ted . I f the v e r i f i c a t i o n r e s u l t were p o s i t i v e and i f the def i n t l were i n f a c t e r roneous , then the e r r o r would have gone u n n o t i c e d . I f the v e r i f i c a t i o n r e s u l t were n e g a t i v e , then the def i n t l would be suspec ted of b e i n g er roneous when i n f a c t i t may be c o r r e c t . As a r e s u l t , e x t r a statements may d i s t o r t t e s t r e s u l t s and may not be d e t e c t e d . 77 Data Flow Test ing I f the uses were p-uses, then i t i s g e n e r a l l y assumed t h a t a l l p o s s i b l e c o n d i t i o n s are cons ide r ed s i n ce t h i s on l y c o n s t i t u t e s good p r a c t i c e . For i n s t a n c e , i f x>3 appears i n an e n a b l i n g c o n d i t i o n , then x<3 and x=3, or a comb ina t ion of the two, shou ld a l s o be p r e s e n t ; o the rw i se , t e s t i n g x>y would r e q u i r e t ha t x be set to 3 and a va lue l e s s than 3 as w e l l to ensure t h a t the e n a b l i n g c o n d i t i o n i s i ndeed c o r r e c t . However, t h i s would not be p o s s i b l e i f the s p e c i f i c a t i o n d i d not s p e c i f y what the IUT i s to do when x<3 and x=3. I f the s p e c i f i c a t i o n d i d s p e c i f y them, then i f the IUT e r r o n e o u s l y missed the c o n d i t i o n x>y a l t o g e t h e r so t h a t x c o u l d have assumed any v a l u e , then t e s t i n g x<3 and x = 3 would have de t e c t ed the m i s s i n g p-use p rov ided the e f f e c t o f the p-uses are v e r i f i a b l e . Hence, the bes t a l t e r n a t i v e i s to s p e c i f y a l l p o s s i b i l i t i e s . I f the def statements i n v o l v e d mathemat ica l e x p r e s s i o n s , then the va lue used as t e s t i npu t c o u l d be j u s t as impor tant as the sequence of t e s t i npu t s to be used . A w e l l known example i s the e x p r e s s i o n y:=2 + x. I f x were chosen to be 2, then i f y were e r roneous l y set to 2*x, the er roneous usage of x, or the def of y , would have gone u n n o t i c e d . For t h i s type of d e f s , i t seems the most a p p r o p r i a t e method of s e l e c t i n g t e s t da ta i s by knowing ahead of t ime what cou ld p o s s i b l y go wrong. However, t h i s 78 Data Flow Test ing i s i m p o s s i b l e because e v e r y t h i n g "under the sun" would have to be taken i n t o c o n s i d e r a t i o n . I n s t ead , one way to s e l e c t t e s t da ta c o u l d be w i th the b o u n d a r y - i n t e r i o r va lue method, where extreme va lues and middle ranged va lues are used . A more p r a c t i c a l approach would be to s e l e c t as t e s t da ta a l l those va lues t ha t are f r e q u e n t l y used i n a r e a l imp lementa t ion of the p r o t o c o l . T h i s approach can a l s o be extended to app ly to t e s t sequence s e l e c t i o n ; t h a t i s , s e l e c t those sequences t h a t are most l i k e l y used i n a r e a l imp lementa t ion to be t e s t e d . T h i s , however, r e q u i r e s c l o s e c o o p e r a t i o n between the t e s t e r s and the u s e r s . 79 5 THE HYBRID TECHNIQUE When the eUIOv-method i s augmented w i th the DFTP, a h y b r i d techn ique i s formed which i s e s s e n t i a l l y a check ing exper iment t ha t i s a p p l i c a b l e to t e s t i n g complex p r o t o c o l s t ha t are mode l led w i th .EFSMs augmented w i th d e s c r i p t i o n s d e t a i l i n g the f u n c t i o n s of t h e i r parameters and v a r i a b l e s . The h y b r i d t echn ique i s a l s o d i r e c t l y a p p l i c a b l e to the t e s t i n g of p r o t o c o l s t ha t are implemented a c c o r d i n g to t h e i r E s t e l l e s p e c i f i c a t i o n s . The EFSM p o r t i o n of the p r o t o c o l , m o d e l l i n g i t s c o n t r o l f l ow , i s checked u s i n g the eUIOv-method i n the h y b r i d t e chn ique . The Pasca l s ta tements i n the E s t e l l e s p e c i f i c a t i o n which d e s c r i b e the da ta f low aspec t of the p r o t o c o l can be used to guide the DFTP w i t h i n the h y b r i d t echn ique to e x e r c i s e and v e r i f y , whenever p o s s i b l e , the i npu t and output p r i m i t i v e parameters i n the IUT as w e l l as i t s minor s t a t e v a r i a b l e s . The h y b r i d t echn ique i s b e l i e v e d to be adequate f o r t e s t i n g E s t e l l e s p e c i f i e d p r o t o c o l s based on the f o l l o w i n g o b s e r v a t i o n s . In FSM t e s t i n g , the UlOv-method t e s t s each t r a n s i t i o n by o b s e r v i n g i t s I/O ope ra t i ons and v e r i f y i n g t h a t i t s s t a r t i n g and f i n a l s t a t e s are c o r r e c t . As a r e s u l t , a l l e lements i n an FSM t r a n s i t i o n are e x e r c i s e d and v e r i f i e d . In EFSM t e s t i n g , the eUIOv-method t e s t s each t r a n s i t i o n by o b s e r v i n g i t s i npu t and output p r i m i t i v e s and v e r i f y i n g t h a t 80 The Hybrid Technique i t s s t a r t i n g and f i n a l TSS v a r i a b l e s are c o r r e c t . As a r e s u l t , the eUIOv-method a l s o e x e r c i s e s and v e r i f i e s each element i n an EFSM t r a n s i t i o n . When i t comes to t e s t i n g an E s t e l l e s p e c i f i c a t i o n , s i n ce i t houses EFSM t r a n s i t i o n s and da ta f low t r a n s i t i o n s , i t s EFSM t r a n s i t i o n s can be t e s t e d u s i n g the eUIov-method. The da ta f low t r a n s i t i o n s can be t e s t e d by e x e r c i s i n g and v e r i f y i n g , whenever p o s s i b l e , s tatements i n v o l v i n g the i npu t and output p r i m i t i v e parameters as w e l l as the minor s t a t e v a r i a b l e s . Once a l l these parameters and v a r i a b l e s are a l s o t e s t e d , a l l e lements i n an E s t e l l e t r a n s i t i o n would have been e x e r c i s e d and v e r i f i e d . The h y b r i d techn ique can thus be viewed as an e x t e n s i o n to the eUIOv-method where, not on l y minor s t a t e v a r i a b l e s are examined, but a l l o the r v a r i a b l e s as w e l l as parameters c o n t r i b u t i n g to da ta f low are examined as w e l l . The h y b r i d techn ique i s thus d i r e c t l y a p p l i c a b l e i n the t e s t i n g of p r o t o c o l s t ha t are implemented a c c o r d i n g t o t h e i r E s t e l l e s p e c i f i c a t i o n s . Dur ing t e s t i n g , the IUT i s checked f o r each t r a n s i t i o n i n the E s t e l l e s p e c i f i c a t i o n one a t a t i m e , e x e r c i s i n g and v e r i f y i n g each statement i n the t r a n s i t i o n whenever p o s s i b l e . T h i s chapter p rov i des an example of how the h y b r i d t echn ique can be used to generate a conformance test , sequence from an E s t e l l e s p e c i f i c a t i o n to t e s t an IUT 81 The Hybrid Technique genera ted from the s p e c i f i c a t i o n . The C l a s s 0 T r a n s p o r t P r o t o c o l i s used as the sample p r o t o c o l i n he re . 5.1 BACKGROUND T h i s s e c t i o n p rov i des a b r i e f i n t r o d u c t i o n to E s t e l l e and i t s normal form. 5.1.1 Este l le E s t e l l e i s a fo rma l d e s c r i p t i o n techn ique deve loped by ISO [IS088] f o r the s p e c i f i c a t i o n o f , but not l i m i t e d t o [Vuon88b], communicat ion p r o t o c o l s and s e r v i c e s . E s t e l l e i s based on an EFSM model f o r s p e c i f y i n g the c o n t r o l s t r u c t u r e of a p r o t o c o l and a se t o f P a s c a l s tatements f o r s p e c i f y i n g i t s data f low . E s t e l l e p r o t o c o l s p e c i f i c a t i o n s are implementa t ion o r i e n t e d and comp i l e r s have been deve loped to generate automat ic p r o t o c o l implementa t ions from t h e i r E s t e l l e s p e c i f i c a t i o n s [Vuong88a]. E s t e l l e d e f i n e s a system u s i n g a h i e r a r c h y of modules . Parent modules may dynami ca l l y c r ea t e and d e s t r o y c h i l d modules. Modules c o n t a i n a b s t r a c t message i n t e r f a c e s o r i n t e r a c t i o n p o i n t s t ha t can be connected to form communicat ion channe l s . S e l e c t e d se t s o f messages or 82 The Hybrid Technique i n t e r a c t i o n p r i m i t i v e s may be exchanged ac ross these channe ls to f a c i l i t a t e communicat ion among modules. A p r o t o c o l can be s p e c i f i e d u s i n g one or more modules . The a c t i o n s of each module, co r r e spond ing to the behav i o r s of the p r o t o c o l , are d e f i n e d by a set o f EFSM t r a n s i t i o n s . The complete " s t a t e " o f the module, or the p r o t o c o l machine, i s cap tu red by the STATE v a r i a b l e as w e l l as o the r minor s t a t e v a r i a b l e s i f they e x i s t . Each t r a n s i t i o n i n the module i s composed of a set o f ope r a t i ons and a se t o f e n a b l i n g c o n d i t i o n s . The e n a b l i n g c o n d i t i o n s may o r may not i n c l u d e an i n p u t even t , the cu r r en t s t a t e and a boo lean e x p r e s s i o n i n v o l v i n g minor s t a t e v a r i a b l e s or i n p u t p r i m i t i v e parameters . Each of these c o n d i t i o n s i s o p t i o n a l and, i f absen t , i s assumed to be s a t i s f i e d . The e n a b l i n g c o n d i t i o n i n v o l v i n g minor s t a t e v a r i a b l e s g e n e r a l l y i n d i c a t e s the c i r cumstance under which d i f f e r e n t t r a n s i t i o n s are t r i g g e r e d i n response to the same p a i r o f i n p u t event and s t a r t i n g s t a t e . Once the e n a b l i n g c o n d i t i o n s i n a t r a n s i t i o n are s a t i s f i e d , a set o f ope r a t i ons may be c a r r i e d o u t . These may i n c l u d e an output o p e r a t i o n , a s t a t e t r a n s i t i o n , and a se t o f o p e r a t i o n s , s p e c i f i e d i n P a s c a l , i n v o l v i n g minor s t a t e v a r i a b l e s or i n t e r a c t i o n p r i m i t i v e parameters . The Pasca l statements may i n c l u d e p rocedure and f u n c t i o n c a l l s as w e l l as c o n d i t i o n a l and loop s ta tements . 83 The Hybrid Technique C o n d i t i o n a l statements permi t a cho i ce of output o p e r a t i o n s to be per formed w i t h i n a s i n g l e t r a n s i t i o n . 5.1.2 Normal Form Este l le Speci f icat ions An E s t e l l e s p e c i f i c a t i o n may be s i m p l i f i e d to a form t h a t i s more e a s i l y r ep resen ted by d i r e c t e d g raphs . T h i s s i m p l i f i e d form of an E s t e l l e s p e c i f i c a t i o n i s known as i t s normal form s p e c i f i c a t i o n (NFS) [ S a r i 8 6 ] . Modules i n the E s t e l l e s p e c i f i c a t i o n are combined u s i n g symbol i c e x e c u t i o n to form a s i n g l e module i n the NFS. S t a tes t h a t have been grouped i n t o s t a t e se t s i n the E s t e l l e s p e c i f i c a t i o n are expanded i n t o the i n d i v i d u a l s t a t e s they r e p r e s e n t i n an NFS. T h i s i s done by r e p l i c a t i n g the a p p r o p r i a t e t r a n s i t i o n a number of t imes equa l s to the number of s t a t e s i n the s t a t e s e t . C o n d i t i o n a l and l oop statements are a l s o e l i m i n a t e d i n the NFS by r e p l i c a t i n g the t r a n s i t i o n which houses those statements a number of t imes equa ls to the number of branches or the s i z e of the l o o p ; t h i s assumes loops do not have v a r i a b l e bounds. P rocedure and f u n c t i o n c a l l s are e l i m i n a t e d w i t h i n t r a n s i t i o n bod ies u s i n g symbol i c e x e c u t i o n . Procedures are assumed to be non-r e c u r s i v e and do not c o n t a i n loops w i th v a r i a b l e bounds. The o v e r a l l appearance of an NFS i s t h a t of a g i a n t EFSM w i th Pasca l ass ignment statements embodied w i t h i n the 84 The Hybrid Technique EFSM t r a n s i t i o n s i n v o l v i n g minor s t a t e v a r i a b l e s and i n t e r a c t i o n p r i m i t i v e parameters . An NFS d i s p l a y s the two types of f lows i n an E s t e l l e s p e c i f i c a t i o n more e x p l i c i t l y . C o n t r o l f low i s marked by changes i n the STATE v a r i a b l e and the i npu t and output o p e r a t i o n s i n v o l v i n g the i n t e r a c t i o n p r i m i t i v e s . Data f low i s i d e n t i f i e d by the o p e r a t i o n s , s p e c i f i e d i n P a s c a l , on the minor s t a t e v a r i a b l e s and i n t e r a c t i o n p r i m i t i v e parameters . An E s t e l l e s p e c i f i c a t i o n hence fo r t h r e f e r s to the o r i g i n a l form of the s p e c i f i c a t i o n i n subsequent d i s c u s s i o n s . 5.1.2.1 Example of an NFS [Ural88] p rov i des an example of an NFS of the C l a s s 0 T r anspo r t P r o t o c o l . T h i s NFS i s p o l i s h e d and rep roduced here i n Appendix A. A l l redundant assignment s tatements are e l i m i n a t e d ; d e t a i l s t ha t have been l e f t out are added back i n . Each t r a n s i t i o n i n the NFS i s i d e n t i f i e d w i th a number. The c u r r e n t s t a t e or the s t a r t i n g s t a t e of each t r a n s i t i o n i s denoted w i th FROM. The f i n a l s t a t e or the next s t a t e of each t r a n s i t i o n i s denoted w i th TO. The PROVIDED c l a u s e expresses the e n a b l i n g c o n d i t i o n i n v o l v i n g minor s t a t e v a r i a b l e s or i npu t p r i m i t i v e parameters . In an E s t e l l e 85 The Hybrid Technique s p e c i f i c a t i o n , the PROVIDED c l ause denotes on l y the c o n d i t i o n s under which d i f f e r e n t s t a t e t r a n s i t i o n s occu r f o r the same combinat ion of i npu t event and s t a r t i n g s t a t e . In an NFS, the PROVIDED c l ause a l s o houses b ranch ing c o n d i t i o n s r e s p o n s i b l e f o r branch paths w i t h i n t r a n s i t i o n s . An example of t h i s i s t r a n s i t i o n s t3 and t 4 . The b ranch ing c o n d i t i o n s " c r . i n . m a x . t p d u . s i z e <> n i l " and " c r . i n . m a x . t p d u . s i z e = n i l " have been e x t r a c t e d from a s i n g l e t r a n s i t i o n i n the E s t e l l e s p e c i f i c a t i o n ; t h a t t r a n s i t i o n was r e p l i c a t e d tw ice t o form t r a n s i t i o n s t3 and t4 i n the NFS. Each i n p u t i n t e r a c t i o n p r i m i t i v e i s preceded by the keyword WHEN. A t r a n s i t i o n may not have an i npu t i n t e r a c t i o n p r i m i t i v e . An example i s t r a n s i t i o n t l 4 . T h i s type of t r a n s i t i o n i s known as spontaneous t r a n s i t i o n s . Each output i n t e r a c t i o n p r i m i t i v e i s preceded by OUT. Each output o p e r a t i o n r e s i d e s i n s i d e a b l o c k i n the body of the t r a n s i t i o n d e l i m i t e d by BEGIN . . . END. Opera t ions to be performed at each t r a n s i t i o n i n v o l v i n g minor s t a t e v a r i a b l e s and i n t e r a c t i o n p r i m i t i v e parameters are expressed i n Pasca l and are a l s o e n c l o s e d i n the b l o c k d e l i m i t e d by BEGIN . . . END. The i n t e r a c t i o n p r i m i t i v e parameters are e n c l o s e d i n p a r e n t h e s i s f o l l o w i n g t h e i r r e s p e c t i v e p r i m i t i v e s . These paramete rs , when r e f e r r e d to i n s i d e the t r a n s i t i o n s , are preceded by the p r i m i t i v e names and e i t h e r " i n " or " ou t " to 86 The Hybrid Technique i n d i c a t e whether they be long to an i npu t or output p r i m i t i v e r e s p e c t i v e l y . When an output p r i m i t i v e parameter i s a s s i gned a cons tan t v a l u e , the cons tan t i s d i r e c t l y p l a c e d i n the a p p r o p r i a t e p o s i t i o n i n the OUT s ta tement . An example i s i n t l , where "norma l " i s d i r e c t l y p l a c e d a t the output parameter l i s t . When the output p r i m i t i v e parameter i s a s s i gned a va lue i d e n t i c a l to t h a t of a minor s t a t e v a r i a b l e , the v a r i a b l e name i s d i r e c t l y p l a c e d i n the a p p r o p r i a t e p o s i t i o n a t the co r r e spond ing OUT s ta tement . An example i s i n t 3 , where " q t s . e s t i m a t e " r e p l a c e s the l a s t parameter name f o r the p r i m i t i v e t c i n d . These d i r e c t p lacements e l i m i n a t e redundant assignment s ta tements . 5.2 REFINING THE NFS An E s t e l l e s p e c i f i c a t i o n i n i t s normal form p r o v i d e s a g r a p h i c a l d e s c r i p t i o n of a p r o t o c o l i n terms o f an " e n r i c h e d " EFSM. The NFS i s f u r t h e r r e f i n e d and r e f o r m a t t e d i n t h i s s e c t i o n to o b t a i n c a n o n i c a l t r a n s i t i o n s and to s e p a r a t e l y b r i n g out the u n d e r l y i n g EFSM and. da ta f l ow f o r t e s t i n g purposes . 5.2.1 Canonical Trans i t ions In o rde r to form c a n o n i c a l t r a n s i t i o n s i n an NFS, exp re s s i ons ORed i n a PROVIDED c l ause shou ld be e x t r a c t e d 87 The Hybrid Technique and the t r a n s i t i o n r e p l i c a t e d a c c o r d i n g l y . The reason i s because OR i s mere ly a way of combining d i f f e r e n t system s t a r t i n g s t a t e s which t r i g g e r the same t r a n s i t i o n when a p a r t i c u l a r i npu t i s r e c e i v e d . An example of t h i s k i n d o f combina t ion i s the s t a t e se t f e a tu r e i n E s t e l l e . S t a t e se t s combined d i f f e r e n t s t a r t i n g STATE v a r i a b l e s t ha t t r i g g e r the same t r a n s i t i o n upon r e c e i v i n g the same i n p u t i n t o one s e t . In forming the NFS, each s t a t e i n the se t would be e x t r a c t e d and the t r a n s i t i o n r e p l i c a t e d f o r each member i n the s e t . The same shou ld thus be done f o r a l l the v a r i a b l e s r e s p o n s i b l e f o r the TSS. For example, i f t r a n s i t i o n t3 i n Appendix A had OR i n i t s PROVIDED c l ause i n s t e a d of AND, then t3 would be r e p l i c a t e d as f o l l o w s : WHEN c r ( . . . ) FROM i d l e PROVIDED c r . i n . m a x . t p d u . s i z e <> n i l TO w f t r t 3 : BEGIN r e m o t e . r e f e r := . . . ; END; WHEN c r ( . . . ) FROM i d l e PROVIDED c r . i n . o p t i o n = ok TO w f t r t 3 i : BEGIN r e m o t e . r e f e r := . . . ; END; 88 The Hybrid Technique 5.2.2 Reformatting the NFS S ince E s t e l l e uses an EFSM to model the c o n t r o l s t r u c t u r e of a p r o t o c o l and a set o f P a sca l s ta tements to d e s c r i b e i t s da ta f l ow , conformance t e s t i n g o f a p r o t o c o l implemented a c c o r d i n g to i t s E s t e l l e s p e c i f i c a t i o n shou ld have i t s c o n t r o l s t r u c t u r e checked a g a i n s t the s p e c i f i e d EFSM and i t s da ta f low checked a g a i n s t the P a s c a l d e s c r i p t i o n s [Chan89a]. A t e s t sequence g e n e r a t i o n techn ique f o r an E s t e l l e s p e c i f i c a t i o n shou ld thus c o n s i d e r both i t s EFSM model as w e l l as i t s da ta f low s ta tements . The NFS i s r e f o rma t t ed here to separate and b r i n g out the u n d e r l y i n g EFSM and da ta f low to a i d t h i s t e s t sequence g e n e r a t i o n p r o c e s s . F a c to r s t ha t c o n t r i b u t e to e x e c u t a b i l i t y problems are a l s o brought out i n the r e f o rma t t ed NFS. 5.2.2.1 Executability Problems There are two types of enab l i ng c o n d i t i o n s i n an E s t e l l e s p e c i f i c a t i o n : those t ha t c o n t r i b u t e to e x e c u t a b i l i t y problems and those t ha t do n o t . C o n d i t i o n s t h a t i n v o l v e i npu t p r i m i t i v e parameters be long to the l a t t e r ca tegory because a p p r o p r i a t e va lues can always be i n p u t a t the t ime of t e s t i n g to permi t e x e c u t a b i l i t y . On the o the r hand, c o n d i t i o n s i n v o l v i n g minor s t a t e v a r i a b l e s c o u l d 89 The Hybrid Technique c o n t r i b u t e to the e x e c u t a b i l i t y problem as these v a r i a b l e s are not d i r e c t l y a c c e s s i b l e . T h e i r va lues may depend on p r e v i ous i npu t p r i m i t i v e parameters or they may r e q u i r e t h a t a p a r t i c u l a r sequence of I/Os occur be fo re they do . The e x e c u t a b i l i t y problem thus su r f a ces i f these v a r i a b l e s are not c o n s i d e r e d d u r i n g the s e l e c t i o n of t e s t sequences . The r o l e s of these v a r i a b l e s i n the EFSM and da ta f low are made e x p l i c i t i n the r e fo rma t t ed NFS to a i d e x e c u t a b i l i t y . 5.2.2.2 The Reformatted NFS The major d i f f e r e n c e between an NFS and a r e f o r m a t t e d NFS i s t ha t the l a t t e r separa tes and b r i n g s out the EFSM and da ta f low from an E s t e l l e s p e c i f i c a t i o n . . The f o l l o w i n g f e a t u r e s i n an E s t e l l e s p e c i f i c a t i o n c o n s t i t u t e an EFSM. Minor s t a t e v a r i a b l e s t ha t appear a t the PROVIDED c l ause toge the r w i th the STATE v a r i a b l e preceded by FROM c o n s t i t u t e the c u r r e n t TSS i n the EFSM. The va lues ob ta ined from t h e i r a l t e r a t i o n s i n the body o f a t r a n s i t i o n and the new STATE v a r i a b l e i n d i c a t e d by the keyword TO c o n s t i t u t e the f i n a l TSS i n the EFSM. Input p r i m i t i v e parameters found at the PROVIDED c l a u s e s i n an E s t e l l e s p e c i f i c a t i o n toge the r w i th t h e i r i npu t i n t e r a c t i o n p r i m i t i v e s denoted by WHEN c o n s t i t u t e the se t o f i n p u t s i n the EFSM. The output se t i s composed of the ou tput 90 The Hybrid Technique p r i m i t i v e s i n d i c a t e d by OUT. The rema in ing s tatements i n the E s t e l l e s p e c i f i c a t i o n be long to i t s da ta f l ow . An EFSM can be e x t r a c t e d from e i t h e r an E s t e l l e s p e c i f i c a t i o n or i t s NFS by ga the r i ng s tatements t h a t co r respond to the f e a t u r e s mentioned above. In an NFS, t h i s r e q u i r e s t ha t some e n a b l i n g c o n d i t i o n s i n the PROVIDED c l ause be separa ted and some Pasca l statements c o r r e s p o n d i n g to da ta f low be d u p l i c a t e d . 5.2.2.3 The Enabling Conditions E n a b l i n g c o n d i t i o n s i n the PROVIDED c l ause i n an NFS t h a t enable d i f f e r e n t t r a n s i t i o n s must be sepa ra ted from those b ranch ing c o n d i t i o n s t ha t a f f e c t d i f f e r e n t paths w i t h i n a s i n g l e t r a n s i t i o n . In an E s t e l l e s p e c i f i c a t i o n , the f i r s t se t o f c o n d i t i o n s i s expressed i n the PROVIDED c l ause and c o n t r i b u t e s to the EFSM; the second se t o f c o n d i t i o n s i s found i n the IF c l ause o r the CASE c l a u s e i n s i d e a t r a n s i t i o n and c o n t r i b u t e s to the f low of d a t a . Both types of c o n d i t i o n s may i n v o l v e minor s t a t e v a r i a b l e s as w e l l as i npu t i n t e r a c t i o n p r i m i t i v e parameters . 5.2.2.4 The Def Statements The o ther major change r e q u i r e d of the NFS i n i t s r e f o r m a t i o n i s t ha t statements w i th de fs of v a r i a b l e s t h a t 91 The Hybrid Technique have p-uses i n the PROVIDED c l ause i n the E s t e l l e s p e c i f i c a t i o n must be gathered i n t o one b l o c k , r e s t o f the statements w i th de fs of v a r i a b l e s or parameters t h a t have f u t u r e c-uses or p-uses r e s p o n s i b l e f o r paths w i t h i n a t r a n s i t i o n are ga thered i n t o another b l o c k . The f i r s t b l o c k determines the next TSS i n the EFSM. The second b l o c k b r i n g s out the da ta f low a spec t . For those v a r i a b l e s t h a t have uses t ha t be long to both b l o c k s , t h e i r def s tatements are d u p l i c a t e d and p l a c e d i n both b l o c k s . 5.2.2.5 Format of the rNFS The f o l l o w i n g shows the gene ra l form of the r e f o r m a t t e d NFS ( rNFS) . t* : WHEN i . i . p . { i . i . p . p . p-uses} FROM e s t a t e AND {m.s.v. p-uses} TO n . s t a t e AND BEGIN {m.s.v. defs} END; OUT o . i . p . PROVIDED ( {m.s.v. or i . i . p . p . p-uses}) BEGIN {m.s.v. defs} { i . i . p . p . c-uses} {m.s.v. c-uses} { o . i . p . p . defs} END; where t * : rNFS t r a n s i t i o n l a b e l i . i . p . : i npu t i n t e r a c t i o n p r i m i t i v e i . i . p . p . : i npu t i n t e r a c t i o n p r i m i t i v e parameter 92 The Hybrid Technique e s t a t e : c u r r e n t s t a t e m . s . v . : minor s t a t e v a r i a b l e n . s t a t e : next s t a t e o . i . p . : output i n t e r a c t i o n p r i m i t i v e o . i . p . p . : output i n t e r a c t i o n p r i m i t i v e parameters An rNFS t r a n s i t i o n i s composed of an EFSM t r a n s i t i o n and a da ta f low t r a n s i t i o n . The group of s tatements from the WHEN c l ause to the OUT c l ause d e s c r i b e s the EFSM t r a n s i t i o n ; r e s t o f the statements s t a r t i n g w i th the PROVIDED c l ause d e s c r i b e the da ta f low . A l l ou tput p r i m i t i v e s are expressed i n the OUT c l a u s e . I f i n the o r i g i n a l s p e c i f i c a t i o n , the re e x i s t s two p o s s i b l e c h o i c e s of output p r i m i t i v e s w i t h i n a s i n g l e t r a n s i t i o n , then i t s co r r e spond ing EFSM p o r t i o n would be r e p l i c a t e d and these output p r i m i t i v e s e x t r a c t e d and put i n t o each EFSM t r a n s i t i o n . The p r e d i c a t e t ha t determines which output p r i m i t i v e to use would a l s o be e x t r a c t e d and put i n the FROM c l ause i f i t i n v o l v e s a v a r i a b l e ; o the rw i se , i t would be put i n the WHEN c l a u s e . V a r i a b l e s i n the p r e d i c a t e are thus t r e a t e d as TSS v a r i a b l e s . I f the p r e d i c a t e a l s o a f f e c t s da ta f l ow , then i t would be r e p l i c a t e d and. p l a c e d a t the PROVIDED c l ause as w e l l to i n d i c a t e the da ta f low p a t h s . The NFS of the C l a s s 0 T ranspo r t P r o t o c o l i n Appendix A i s r e f o rma t t ed i n t o an rNFS shown i n Appendix B. Note t h a t 93 i The Hybrid Technique when two rNFS t r a n s i t i o n s share an i d e n t i c a l EFSM t r a n s i t i o n , t h e i r l a b e l s i n d i c a t e them as " t e a " and " t e b " where " t e " l a b e l s the rNFS t r a n s i t i o n and " a " and " b " l a b e l i t s two da ta f low pa ths . Th i s type of rNFS t r a n s i t i o n cor responds to a s i n g l e E s t e l l e t r a n s i t i o n w i th two branch paths w i t h i n . The r e fo rma t t ed NFS can be e a s i l y genera ted from an E s t e l l e s p e c i f i c a t i o n by f o l l o w i n g the same procedure as t h a t f o r g e n e r a t i n g the NFS w i th the e x c e p t i o n t h a t the e n a b l i n g c o n d i t i o n s are kept sepa ra te . As w e l l , minor s t a t e v a r i a b l e s t ha t appear i n the PROVIDED c l a u s e s are i d e n t i f i e d and t h e i r def statements are e x t r a c t e d and d u p l i c a t e d whenever necessa r y . I f more than one output p r i m i t i v e e x i s t s i n a t r a n s i t i o n , they would a l s o be e x t r a c t e d as d i s c u s s e d above. 5.3 ESTELLE EFSM TESTING T h i s s e c t i o n shows how an E s t e l l e EFSM may be t e s t e d u s i n g the eUIOv-method. Tab le 5.1 i s an EFSM t a b l e r e p r e s e n t i n g the EFSM of the C l a s s 0 T r anspo r t P r o t o c o l e x t r a c t e d from i t s rNFS i n Appendix B. 94' The Hybrid Technique "V. C.TSS F.TSS IDLE WFCC WFTR DATA DATA o .b .oO DATA i .b . <>0 WFCC tcreq (qr=ok) /cr IDLE tcreq (qrook) /tdind cr (opook) /dr dr/ ndreq, tdind teres (qr>qe) /dr, tdind tdreq/ dr tdreq /ndreq ndind /tdind nrind /tdind WFTR q .e .= . . . cr (op=ok) /tcind DATA i.b.=0 o.b.=0 q .e .=. . . cc/ tccon DATA i.b.=0 o.b=0 teres (qr<=qe) /cc DATA o .b .oO tdatr /-DATA o.b.=0 -/dt DATA i . b . 0 0 dt/-DATA i.b.=0 -/ tdat i Table 5.1 EFSM table fo r the Class 0 Transport Protocol . 95 The Hybrid Technique 5.3.1 Spontaneous t rans i t ions Spontaneous t r a n s i t i o n s are E s t e l l e t r a n s i t i o n s t h a t do not r e q u i r e i npu t s to be enab led . These t r a n s i t i o n s are enab led as l ong as t h e i r TSSs are s a t i s f i e d . A spontaneous t r a n s i t i o n thus v e r i f i e s a l l or p a r t of a f i n a l TSS f o r another t r a n s i t i o n when i t i s enab led and i t s ou tput i s observed d u r i n g t e s t i n g . In a d d i t i o n , i t s absence i s capab le of v e r i f y i n g a l l or p a r t o f a f i n a l TSS f o r another t r a n s i t i o n whose TSS va lues do not equa l to those of the s t a r t i n g TSS f o r the spontaneous t r a n s i t i o n . For i n s t a n c e , i f a spontaneous t r a n s i t i o n has the f o l l o w i n g s t a r t i n g TSS and ou tpu t : FROM s i AND x = y OUT o l then when -/o l i s obse rved , i t v e r i f i e s t h a t the STATE v a r i a b l e was at s i and the x v a r i a b l e was equa l to y. When -/o l i s not obse rved , then e i t h e r STATE was not a t s i o r x was not equa l to y. Hence, the absence of a spontaneous t r a n s i t i o n output i s e q u a l l y s i g n i f i c a n t d u r i n g t e s t i n g . In summary, the presence of a spontaneous t r a n s i t i o n output v e r i f i e s an N.TSS i d e n t i c a l to the spontaneous t r a n s i t i o n C.TSS. I t s absence v e r i f i e s an N.TSS t h a t i s d i f f e r e n t from i t s C.TSS. 96 The Hybrid Technique 5.3.2 Test ing the EFSM i n the COTP As an example, the eUIOv-method i s a p p l i e d to the EFSM t a b l e i n Tab le 5.1 f o r the C l a s s 0 T r anspo r t P r o t o c o l (COTP). The EFSM had to be completed w i th the Completeness Assumpt ion to generate a se t o f UIOSs i n t h i s c a se . The Completeness Assumpt ion used i n the example i s t h a t u n s p e c i f i e d i npu t s are i gno red and the IUT remains i n i t s c u r r e n t s t a t e . The a d d i t i o n a l t r a n s i t i o n s a r i s i n g from the assumpt ion are not t e s t e d i n he re , but they would be i f they had been p a r t o f the s p e c i f i c a t i o n . The UIOSs chosen f o r the s t a t e s i n the EFSM are as f o l l o w s : UIOS(IDLE) = t c r e q ( q t s . r e q = ok ) / c r UIOS(WFCC) = d r / n d r e q , t d i n d UIOS(WFTR) = t d r eq/d r UIOS(DATA) = td req/ndreq T h i s i s done by s e l e c t i n g I/O sequences t ha t are unique to the s t a t e s from the f i r s t f ou r columns of the t a b l e . These columns denote TSSs determined s o l e l y by the STATE v a r i a b l e s ; hence, t h e i r t r a n s i t i o n s are not e . t r a n s i t i o n s . S ince the r e s e t f e a tu r e does not e x i s t i n the C l a s s 0 T r a n s p o r t P r o t o c o l , each of the f o l l o w i n g I/O sequences takes a s t a t e back to the i n i t i a l IDLE s t a t e : postamble(WFCC) = d r / n d r e q , t d i n d 97 The Hybrid Technique postamble(WFTR) = td r eq/d r postamble(DATA) = td req/ndreq The f o l l o w i n g I/O sequences are chosen as preambles t o take the EFSM from i t s i n i t i a l IDLE s t a t e to each of the o the r s t a t e s . No s p e c i a l requ i rement e x i s t s f o r the preambles s i n ce the UIOSs are themselves execu t ab l e . preamble(WFCC) = t c r e q ( q t s . r e q = ok ) / c r preamble(WFTR) = c r ( o p t i o n = ok)/tc ind~ preamble(DATA) = t c r e q ( q t s . r e q = o k ) / c r . c c / t c c o n The f o l l o w i n g t e s t subsequences v e r i f y the postambles to ensure they do end at the i n i t i a l IDLE s t a t e . The procedure can be shor tened by v e r i f y i n g on l y those postambles t h a t are a c t u a l l y used . t c r e q ( q t s . r e q = o k ) / c r . d r / n d r e q , t d i n d . t c r e q ( q t s . r e q = o k ) / c r . d r / n d r e q , t d i n d ( f o r WFCC) c r ( o p t i o n = o k ) / t c i n d . t d r e q / d r . t c r e q ( q t s . r e q = o k ) / c r . d r / n d r e q , t d i n d ( f o r WFTR) t c r e q ( q t s . r e q = o k ) / c r . c c / t c c o n . t d r e q / n d r e q . t c r e q ( q t s . r e q = o k ) / c r . d r / n d r e q , t d i n d ( f o r DATA) The f o l l o w i n g t e s t subsequences c o n s t i t u t e the Uv and ~Uv procedures f o r the EFSM. Uv: t c r e q ( q t s . r e q = o k ) / c r d r / n d r e q , t d i n d t c r e q ( q t s . r e q = o k ) / c r . d r / n d r e q , t d i n d c r ( o p t i o n = o k ) / t c i n d . t d r e q / d r 98 The Hybrid Technique t c r e q ( q t s . r e q = o k ) / c r . c c / t c c o n . t d r e q / n d r e q ~Uv: d r /-t d r e q / -t c r e q ( q t s . r e q = o k ) / c r . t c r e q / - . d r / n d r e q , t d i n d t c r e q ( q t s . r e q = o k ) / c r . t d r e q / - . d r / n d r e q , t d i n d c r ( o p t i o n = o k ) / t c i n d . t c r e q / - . t d r e q / d r c r ( o p t i o n = o k ) / t c i n d . d r / - . t d r e q / d r t c r e q ( q t s . r e q = o k ) / c r . c c / t c c o n . t c r e q / - . t d r e q / n d r e q t c r e q ( q t s . r e q = o k ) / c r . c c / t c c o n . d r / - . t d r e q / n d r e q Note t ha t s i n ce WFTR and DATA both have an UIOS w i t h t d r e q as i n p u t , the ~Uv procedure i s shor tened . IDLE and WFCC t e s t i n g f o r t d r e q / - v e r i f i e s the absences of both UIOSs. WFTR t e s t i n g f o r t d r eq/d r i n Uv v e r i f i e s the absence o f t d r e q / n d r e q , the UIOS f o r DATA. DATA t e s t i n g f o r td req/ndreq i n Uv v e r i f i e s the absence of t d r e q / d r , the UIOS f o r WFTR. D u p l i c a t e d t e s t subsequences can be e l i m i n a t e d to op t im i ze the f i n a l t e s t sequence. The next procedure i n the eUIOv-method i s T t ; i t t e s t s and v e r i f i e s a l l t r a n s i t i o n s . With the e x c e p t i o n o f e. t r a n s i t i o n s t i l and t l 3 , a l l the t r a n s i t i o n s or t a b l e e n t r i e s are t e s t e d i n t h i s p rocedure . The f o l l o w i n g t e s t subsequences are d e r i v e d f o r t h i s p rocedure . T t : t c r e q ( q t s . r e q = o k ) / c r . d r / n d r e q , t d i n d t c r e q ( q t s . r e q o o k ) / t d i n d . t c r e q ( q t s . r e q = o k ) / c r . 99 The Hybrid Technique d r / n d r e q , t d i n d c r ( o p t i o n < > o k ) / d r . t c r e q ( q t s . r e q = o k ) / c r . d r / n d r e q , t d i n d c r ( o p t i o n = o k ) / t c i n d . t d r e q / d r t c r e q ( q t s . r e q = o k ) / c r . d r / n d r e q , t d i n d . t c r e q ( q t s . r e q = o k ) / c r . d r / n d r e q , t d i n d t c r e q ( q t s . r e q = o k ) / c r . c c / t c c o n . t d r e q / n d r e q c r ( o p t i o n = o k ) / t c i n d . t c r e q ( q t s . r e q > q t s . e s t i m a t e ) / d r , t d i n d . t c r e q ( q t s . r e q = o k ) / c r . d r / n d r e q , t d i n d c r ( o p t i o n = o k ) / t c i n d . t d r e q / d r . t c r e q ( q t s . r e q = o k ) / c r . d r / n d r e q , t d i n d c r ( o p t i o n = o k ) / t c i n d . t e r e s ( q t s . r e q < = q t s . e s t i m a t e ) / c c . t d r e q / n d r e q . d r / n d r e q , t d i n d t c r e q ( q t s . r e q = o k ) / c r . c c / t c c o n . t d r e q / n d r e q . t c r e q ( q t s . r e q = o k ) / c r . d r / n d r e q , t d i n d t c r e q ( q t s . r e q = o k ) c r . c c / t c c o n . n d i n d / t d i n d . t c r e q ( q t s . r e q = o k ) / c r . d r / n d r e q , t d i n d t c r e q ( q t s . r e q = o k ) c r . c c / t c c o n . n r i n d / t d i n d . t c r e q ( q t s . r e q = o k ) / c r . d r / n d r e q , t d i n d t c r e q ( q t s . r e q = o k ) / c r . c c / t c c o n . t d a t r / - . - / d t . t d r e q / n d r e q t c r e q ( q t s . r e q = o k ) / c r . c c / t c c o n . d t / - . - / t d a t i . t d r e q / n d r e q Note t h a t the l a s t two subsequences c o n t a i n the spontaneous t r a n s i t i o n s -/dt and - / t d a t i . These are i n c l u d e d because t h e i r TSSs are enab led f o l l o w i n g t d a t r / - and d t /-r e s p e c t i v e l y . T h e i r outputs shou ld thus be observed d u r i n g 100 The Hybrid Technique t e s t i n g ; hence, they are i n c l u d e d i n the f i n a l sequence. T h i s i m p l i e s t d a t r / - and d t/- do not r e q u i r e UIOS(DATA) to v e r i f y t h e i r f i n a l s t a t e s . T h e i r f i n a l s t a t e s are a u t o m a t i c a l l y v e r i f i e d by the presences of -/dt and - / t d a t i . T h i s type of spontaneous t r a n s i t i o n s can be d i r e c t l y appended to t h e i r e n a b l i n g t r a n s i t i o n s to denote t h e i r l a c k of i npu t s and when they are enab led . In t h i s example, the EFSM t a b l e en t r y f o r t d a t r / - can be changed to t d a t r / - . - / d t ; d t /- can be changed to d t / - . - / t d a t i . The columns and rows f o r -/dt and - / t d a t i can be removed. The row where t d a t r / -.-/dt appears can be r e l a b e l l e d as d a t a , o u t . b u f f e r = 0 ; where d t / - . - / t d a t i appears can be r e l a b e l l e d as d a t a , i n . b u f f e r = 0 . Conca tena t i ng the spontaneous t r a n s i t i o n s removes a l l the e . t r a n s i t i o n s i n t h i s case . The eTt procedure i s not a p p l i c a b l e here s i n ce the o n l y e . t r a n s i t i o n s are spontaneous t r a n s i t i o n s . However, i f they had not been spontaneous t r a n s i t i o n s , the procedure to form t h e i r t e s t subsequences would be as f o l l o w s . E x t r a c t the e . t r a n s i t i o n , i n t h i s example, take t i l or - /d t . A c c o r d i n g to i t s column l a b e l , i t s s t a r t i n g TSS i s a t DATA and ou t . b u f f e r <> 0. T r a v e l down the rows and f i n d the one whose l a b e l denotes a f i n a l TSS i d e n t i c a l to t h a t . The sea rch would s top at DATA and o u t . b u f f e r = t d a t r . i n . t s d u . f ragment , denoted as DATA, o . b . o O i n the 101 The Hybrid Technique t a b l e . Any en t r y a t t h i s row i s an e n a b l i n g c o n d i t i o n f o r t i l . There i s on l y one en t r y i n t h i s example, namely t r a n s i t i o n t l O or t d a t r / - . Hence, t d a t r / - must precede -/dt to enable the l a t t e r . To t e s t - /d t , a preamble must be formed which beg ins a t IDLE and ends w i th t d a t r / - . A p a r t i a l preamble t c r e q ( q t s . r e q = o k ) / c r . c c / t c c o n takes the EFSM from i d l e to DATA, then t d a t r / - i s conca tena ted t o i t t o form the complete preamble. The f o l l o w i n g t e s t subsequences would be used to t e s t -/d t : e T t : ( 1 ) t c r e q ( q t s . r e q = o k ) / c r . c c / t c c o n . t d a t r / - . t d r e q / n d r e q ( 2 ) t c r e q ( q t s . r e q = o k ) / c r . c c / t c c o n . t d a t r / - . - / d t . td req/ndreq where subsequence (1) f i r s t v e r i f i e s the preamble to ensure i t ends a t the c o r r e c t s t a t e , thus v e r i f y i n g the s t a r t i n g s t a t e of the e. t r a n s i t i o n to be t e s t e d . Subsequence (2) then t e s t s the e . t r a n s i t i o n , - /d t , and v e r i f i e s i t s f i n a l s t a t e w i th t d r eq/nd req . S ince -/dt i s r e a l l y a spontaneous t r a n s i t i o n , subsequence (1) i s not p o s s i b l e . Subsequence (2) i s i d e n t i c a l to t ha t f o r t e s t i n g the t r a n s i t i o n t d a t r / - , hence , i t i s a l r e ady i n c l u d e d . The l a s t procedure i s msvv to v e r i f y the s t a r t i n g and f i n a l TSSs at each t r a n s i t i o n . The on l y two s t a r t i n g TSSs t h a t i n v o l v e minor s t a t e v a r i a b l e s are DATA AND o . b . o O and DATA AND i . b . o O . However, s i n ce they enable spontaneous 102 The Hybrid Technique t r a n s i t i o n s , the e f f e c t s of these p r e d i c a t e s have a l r e a d y been v e r i f i e d i n the T t procedure when the outputs from these t r a n s i t i o n s are obse rved . The f i n a l TSSs t h a t have to be v e r i f i e d here are i d e n t i f i e d by those t r a n s i t i o n s whose row l a b e l s i n c l u d e de f s of minor s t a t e v a r i a b l e s . In the example, these are t r a n s i t i o n s t 3 , t 5 , t 7 , t l O , t i l , t l 2 and t l 3 . I t shou ld be noted tha t wh i l e an use must be p receded by a def o f the v a r i a b l e , not every def w i l l n e c e s s a r i l y be used . These de f s can e a s i l y be i d e n t i f i e d by compar ing the column l a b e l s w i th the row l a b e l s . For i n s t a n c e , the d e f s i n . b u f f e r = 0 and o u t . b u f f e r = 0 do not appear a t the column l a b e l s . T h i s i m p l i e s these two de f s are never used . However, s i n ce the re e x i s t s two spontaneous t r a n s i t i o n s which are enab led when s t a t e i s a t DATA and i n . b u f f e r or o u t . b u f f e r are <> 0, these de fs can i m p l i c i t l y be v e r i f i e d by o b s e r v i n g tha t those two spontaneous t r a n s i t i o n s do not o c c u r ! T h i s a l s o v e r i f i e s t ha t the p r e d i c a t e s u s i n g i . b . and o . b . are c o r r e c t . S ince the domains of these p r e d i c a t e s are e i t h e r 0 or not 0, they do not r e q u i r e the boundary-i n t e r i o r va lue c r i t e r i o n , but the c r i t e r i o n can be used to s e l e c t ve ry l a r g e and very sma l l v a lues t o v e r i f y the domains when they are not a t 0. The o the r de f s to be v e r i f i e d i n c l u d e q t s . e s t i m a t e = o u t . b u f f e r = t d a t r . i n . t s d u . fragment ( o . b . o O ) and i n . b u f f e r = 103 The Hybrid Technique d t . i n . u s e r . da ta ( i . b . o O ) . For q t s . e s t i m a t e = t r a n s i t i o n t3 or c r ( o p t i o n = o k ) / t c i n d enab les i t . Hence, the column l a b e l s can be searched f o r a p-use of q t s . e s t i m a t e . None i s found i n the example, however, f o r s t a t e WFTR, t r a n s i t i o n t8 r e q u i r e s i t s i npu t parameter q t s . r e q to be > q t s . e s t i m a t e , hence, t8 can be used to v e r i f y the de f i n t 3 . For the second q t s . e s t i m a t e = . . . d e f i n e d i n the four th" row, t r a n s i t i o n t5 enab les i t . A search of the column l a b e l s aga in tu rns up t r a n s i t i o n t 8 . Hence, i f the re e x i s t s a pa th t ha t i s f r e e of a def of q t s . e s t i m a t e , then t8 can a l s o be used to v e r i f y the def i n t 5 . From t 5 , the on l y t r a n s i t i o n s t h a t would e x i t the s t a t e DATA are t l 4 , t l 5 and t l 6 which a l l l e a d to IDLE. From IDLE, t r a n s i t i o n t l l e ads to WFCC, but t r a n s i t i o n s from WFCC e i t h e r takes the EFSM back to IDLE or to DATA a g a i n , the l a t t e r i n t r o d u c i n g a new def of q t s . e s t i m a t e . The o the r path from IDLE tha t does not l oop back to IDLE i s v i a t3 which a l s o enab les a new def o f q t s . e s t i m a t e . Hence, i t can be conc luded t h a t the re i s no d e f - f r e e path t h a t would b r i n g t5 to t 8 , o r t o any t r a n s i t i o n generated from WFTR which con t a i n s a p-use of q t s . e s t i m a t e ; hence, the def of q t s . e s t i m a t e c o u l d never l e a d to the p-use of i t i n t 8 , or i n the o the r t r a n s i t i o n from WFTR, t 7 . The rema in ing de fs to be v e r i f i e d are o . b . <> 0 and i . b . <> 0. For both of them, the on l y s t a r t i n g 104 The Hybrid Technique TSSs tha t make use. of them be long to spontaneous t r a n s i t i o n s . Hence, t h e i r v e r i f i c a t i o n s are automat ic and i m p l i c i t when those spontaneous t r a n s i t i o n s are enab led and obse rved . Hence, f o r the msvv p rocedure , the re i s on l y one t e s t subsequence. msvv: c r ( o p t i o n = o k ) / t c i n d . t e r e s ( q t s . r e q > q t s . e s t i m a t e ) / d r , t d i n d The minor s t a t e v a r i a b l e q t s . e s t i m a t e used i n the p r e d i c a t e (q t s . r eq > q t s . es t imate ) i n t8 can be made more v i s i b l e by changing i t s s t a r t i n g TSS from WFTR to "WFTR, q t s . e s t i m a t e d e f ' d " . However, t h i s i s g e n e r a l l y not necessa r y as minor s t a t e v a r i a b l e s are t y p i c a l l y i n i t i a l i z e d to some i n i t i a l va lues at the beg inn ing of the s p e c i f i c a t i o n . The f i n a l unopt imized t e s t sequence f o r the EFSM of the C l a s s 0 T r anspo r t P r o t o c o l has 98 t e s t i n p u t s . I f d u p l i c a t e t e s t subsequences are removed, the op t im ized t e s t sequence has 76 t e s t i n p u t s . 5.4 ESTELLE DATA FLOW TESTING T h i s s e c t i o n d i s c u s s e s how the da ta f low p o r t i o n o f an IUT genera ted a c c o r d i n g to i t s E s t e l l e s p e c i f i c a t i o n can be t e s t e d . 105 The Hybrid Technique In t e s t i n g the da ta f low of a p r o t o c o l based on i t s E s t e l l e s p e c i f i c a t i o n , the v a r i a b l e s and parameters t h a t appear i n the da ta f low p o r t i o n of the rNFS are t r a c k e d from the moment they are d e f i n e d u n t i l they are used e i t h e r f o r computa t iona l purposes or as p r e d i c a t e s . V e r i f i c a t i o n f o r the d e f s , the e f f e c t s of the uses as w e l l as the c o r r e c t n e s s o f p-uses are a p p l i e d whenever p o s s i b l e as ment ioned i n the p r e v i ous chap te r . E n a b l i n g c o n d i t i o n s i n spontaneous t r a n s i t i o n s t h a t i n v o l v e minor s t a t e v a r i a b l e s aga in may a i d i n the p roces s of v e r i f i c a t i o n i n the same way they do i n the eUIOv-method; t h a t i s , t h e i r absences a l s o v e r i f y those minor s t a t e v a r i a b l e s whose a ss igned va lues are d i f f e r e n t from those of t h e i r C.TSSs to be indeed d i f f e r e n t . The EFSM t a b l e used i n the eUIOv-method i s augmented w i th e n a b l i n g c o n d i t i o n s f o r the da ta f low t r a n s i t i o n s to a i d i n de te rm in ing execu tab le f low paths between two s e l e c t e d rNFS t r a n s i t i o n s . I f the da ta f low p o r t i o n i n a rNFS t r a n s i t i o n i s preceded w i th a PROVIDED c l ause i n v o l v i n g minor s t a t e v a r i a b l e s , then t h e i r p-uses and de f s would be e x t r a c t e d to form new TSSs i n the EFSM t a b l e . New columns or rows may thus be added i n the augmented t a b l e a l ong w i th new t a b l e e n t r i e s . Those PROVIDED c l a u s e s t h a t i n v o l v e i n p u t parameters would be i n d i c a t e d i n the a p p r o p r i a t e t a b l e 106 The Hybrid Technique e n t r i e s to i n d i c a t e t h a t s p e c i f i c va lues are r e q u i r e d a t the t ime of i n p u t d u r i n g t e s t i n g . One of the advantages of s e p a r a t i n g the EFSM t r a n s i t i o n s from the da ta f low t r a n s i t i o n s i n an rNFS su r f a ce s he re : d u r i n g EFSM t e s t i n g , r e p l i c a t e d t r a n s i t i o n s due to da ta f low paths are not u n n e c e s s a r i l y t e s t e d t w i c e ; whereas, i f the NFS were used , EFSM t e s t i n g would c o n t a i n redundant t e s t subsequences. 5.4.1 Data Flow Test ing fo r the COTP T h i s s e c t i o n p rov i des an example of da ta f low t e s t i n g u s i n g the rNFS of the C l a s s 0 T r anspo r t P r o t o c o l . The EFSM t a b l e shown i n Tab le 5.1 i s f i r s t augmented w i th the necessa ry da ta f low p o r t i o n s to form the t a b l e shown i n Tab le 5.2. Note t ha t i n the rNFS, the re are two da ta f low paths i n each of t r a n s i t i o n t 3 , t5 and t 6 . However, s i n ce t h e i r PROVIDED c l auses i n v o l v e o n l y i n p u t pa ramete rs , no rows or columns needed to be added i n . The next s tep i s to i d e n t i f y and e x t r a c t a l l the t r a n s i t i o n s t h a t span i n t e r - t r a n s i t i o n a l da ta f low paths (de f- i tDFPs ) . Each t r a n s i t i o n i n the rNFS i s examined one a t a t ime . To beg in w i t h , t r a n s i t i o n t l does not have any d e f - i t D F P . A l l the d e f i n i t i o n s i n t ha t t r a n s i t i o n are used t h e r e ; hence , e x e r c i s i n g the t r a n s i t i o n a lone e x e r c i s e s as 107 The Hybrid Technique w e l l as v e r i f i e s a l l the de f s i n the t r a n s i t i o n s i n c e the usages are f o r d e f i n i n g output parameters . The same goes f o r t r a n s i t i o n s t 2 , t 4 , t l 4 , t l 5 and t l 6 . In t r a n s i t i o n s t l O and t l 2 , r e c a l l t ha t spontaneous t r a n s i t i o n s t i l and t l 3 may be appended to them because t h e i r e x e c u t i o n i n d i c a t e t i l and t l 3 would a l s o be executed . As a r e s u l t , the de f - i tDFPs i n t l O and t l 2 are " au tomat i c " and have a l r e a d y been i n c l u d e d i n the T t procedure d u r i n g EFSM t e s t i n g . Hence, these two t r a n s i t i o n s do not have to be c o n s i d e r e d here a g a i n . 108 The Hybrid Technique " ^ ^ C . T S S F.TSS IDLE WFCC WFTR DATA DATA o .b .oO DATA i .b . <>0 WFCC tcreq (qr=ok) /cr IDLE tcreq (qrook) /tdind cr (opook) /dr dr (dr=ui) /ndreq, tdind dr (droui ) /ndreq, tdind teres (qr>qe) /dr, tdind tdreq/ dr tdreq /ndreq ndind /tdind nrind /tdind WFTR q .e .=. . . cr (op=ok, mts<>=0) /tcind cr (op=ok, mts=0) /tcind DATA i.b.=0 o.b.=0 q .e .=. . . cc (mtsoO) /tccon cc (mts=0) /tccon DATA i.b.=0 o.b=0 teres (qr<=qe| /cc DATA o.b.<>0 tdatr /-DATA o.b.=0 -/dt DATA i . b . o O dt/-DATA i.b.=0 -/ tdat i Table 5.2 Augmented EFSM table fo r Class 0 Transport Protocol . 109 The Hybrid Technique Each of the rema in ing t r a n s i t i o n s i n the rNFS c o n t a i n s d e f - i t D F P s : t 3 a , t 3 b , t 5 a , t5b and t 7 . The def s tatements t h a t span the i tDFPs i n these t r a n s i t i o n s are as f o l l o w s . t 3 a : r e m o t e . r e f e r := c r . i n . s o u r c e . r e f t p d u . s i z e := c r . i n . m a x . t p d u . s i z e ; ( c r . i n . m a x . t p d u . s i z e <> n i l ) t 3 b : r e m o t e . r e f e r := c r . i n . s o u r c e . r e f t p d u . s i z e := . . . ; ( c r . i n . m a x . t p d u . s i z e = n i l ) t 5 a : i n . b u f f e r := n i l ; o u t . b u f f e r := n i l ; t p d u . s i z e := . . . ; { o u t . b u f f e r . s e t . m a x . s i z e ( t pdu . s i ze ) } ( c c . i n . m a x . t p d u . s i z e <> n i l ) t 5 b : i n . b u f f e r := n i l ; , o u t . b u f f e r := n i l ; t p d u . s i z e := . . . ; { o u t . b u f f e r . s e t . m a x . s i z e ( t pdu . s i ze ) } ( c c . i n . m a x . t p d u . s i z e = n i l ) t 7 : i n . b u f f e r := n i l ; o u t . b u f f e r := n i l ; T r a n s i t i o n s t 7 , t8 and t9 c o n t a i n usages of v a r i a b l e s or parameters whose d e f i n i t i o n s do not r e s i d e w i t h i n the same t r a n s i t i o n s . The usages are l i s t e d as f o l l o w s : 110 The Hybrid Technique t 7 : c c . o u t . d e s t . r e f e r := r e m o t e . r e f e r c c . o u t . c a l l i n g . t . a d d r := c a l l i n g . t . a d d r ; c c . o u t . c a l l e d . t . a d d r := c a l l e d . t . a d d r ; c c . o u t . m a x . t p d u . s i z e := t p d u . s i z e ; o u t . b u f f e r . s e t . m a x . s i z e ( t p d u . s i z e ) t 8 : d r . o u t . d e s t . r e f e r := r e m o t e . r e f e r ; t 9 : d r . o u t . d e s t . r e f e r := r e m o t e . r e f e r ; t 6 a : { t d i n d . o u t . t s . u s e r . r e a s o n := d r . i n . a d d . c l r . r e a s o n ; } ( d r . i n . d i s c . r e a s o n = " u s e r . i n i t " ) t 6b : ( d r . i n . d i s c . r e a s o n <> " u s e r . i n i t " ) In t r a n s i t i o n t6a and t 6 b , a l though both n e i t h e r span de f- i tDFPs nor r e q u i r e use- i tDFPs , they c o n t a i n p-uses of the v a r i a b l e d r . i n . d i s c . r e a s o n . The e f f e c t s of these p-uses can be v e r i f i e d by obse r v i ng tha t when the parameter i s equa l to " u s e r . i n i t , " an a d d i t i o n a l output parameter e x i s t s f o r the output p r i m i t i v e t d i n d . Both t r a n s i t i o n s t6a and t6b must be e x e r c i s e d to t e s t and v e r i f y the p-uses w i t h i n . They are thus i n c l u d e d i n the above l i s t . The c o r r e c t n e s s of these p-uses are a u t o m a t i c a l l y v e r i f i e d when both t r a n s i t i o n s t6a and t6b are e x e r c i s e d d u r i n g t e s t i n g s i n c e the p-uses are comple te l y s p e c i f i e d . Domain t e s t i n g u s i n g b o u n d a r y - i n t e r i o r va lues i s not a p p l i c a b l e he re . For each of the v a r i a b l e s t ha t have been d e f i n e d but not used , a d e f - f r e e da ta f low path (def- i tDFP) has to be 111 The Hybrid Technique genera ted to connect i t t o i t s usage and, i f p o s s i b l e , to extend i t to a t r a n s i t i o n t ha t can v e r i f y i t s c o r r e c t n e s s . S i m i l a r l y f o r the uses of those v a r i a b l e s whose d e f i n i t i o n s do not r e s i d e i n the same t r a n s i t i o n . A d e f - f r e e pa th has to connect a def of each v a r i a b l e to i t s usage (use-i tDFP) and t h e n , i f p o s s i b l e , to a t r a n s i t i o n which can v e r i f y i t s c o r r e c t n e s s . The f o l l o w i n g l i s t s the t r a n s i t i o n s c o n t a i n i n g the de f s and uses of each v a r i a b l e l i s t e d above. Those v a r i a b l e s d e f i n e d w i thout a use i n the same t r a n s i t i o n are l i s t e d w i th "de f " f i r s t ; the "use " l i s t t h a t f o l l o w s i s e x t r a c t e d from a l l the t r a n s i t i o n s i n the rNFS t h a t c o n t a i n uses of the v a r i a b l e . Those v a r i a b l e s used w i thou t a def i n the same t r a n s i t i o n are l i s t e d w i th "use " f i r s t ; the " de f " l i s t t ha t f o l l o w s i s a l s o e x t r a c t e d from the e n t i r e rNFS. The " d " i n the n o t a t i o n (d,u) i n d i c a t e s t ha t the usage i s d i r e c t l y preceded by a def o f the v a r i a b l e i n the same t r a n s i t i o n ; hence, no d e f - f r e e path e x i s t s f o r any de f of t ha t v a r i a b l e o c c u r r i n g i n another t r a n s i t i o n i n o rde r to r each t h a t use . The " u " i n the n o t a t i o n i n d i c a t e s t h a t i t i s an unobservab le use . r e m o t e . r e f e r : def - t 3 a , t3b use - t 7 , t 8 , t9 t p d u . s i z e : def - t 3 a , t 3 b , t 5 a , t5b use - t 5 a ( d , u ) , t 5 b ( d , u ) , t7 112 The Hybrid Technique i n . b u f f e r : def - t 5 a , t 5 b , t7 use - t l 2 . t l 3 ( d ) o u t . b u f f e r : def - t 5 a , t 5 b , t7 use - t l O . t l l ( d ) r e m o t e . r e f e r : use - t 7 , t8 t9 : def - t 3 a , t3b c a l l i n g . t . a d d r : use - t7 def - t 3 a , t 3 b c a l l e d . t . a d d r : use - t7 def - t 3 a , t 3 b t p d u . s i z e : use - t7 def - t 3 a , t 3 b , For the p r e d i c a t e s , they are not i n c l u d e d i n the above l i s t but they are e x t r a c t e d and the t r a n s i t i o n s t ha t they enab le are compared and the d i f f e r e n c e s are l i s t e d as f o l l o w s . By o b s e r v i n g the d i f f e r e n c e s , when p o s s i b l e , the p-uses can be v e r i f i e d . c r . i n . m a x . t p d u . s i z e : <> n i l -> t p d u . s i z e := c r . i n . m a x . t p d u . s i z e : = n i l -> t p d u . s i z e : = . . . ; c c . i n . m a x . t p d u . s i z e : <> n i l -> t p d u . s i z e := c c . i n . m a x . t p d u . s i z e : = n i l -> 113 The Hybrid Technique t p d u . s i z e := . . . ; d r . i n . d i s c . r e a s o n : = " u s e r . i n i t " -> t d i n d . o u t . t s . u s e r . r e a s o n := d r . i n . a d d . c l r . r e a s o n : <> " u s e r . i n i t " -> ~ ( t d i n d . o u t . t s . u s e r . r e a s o n ) As can be seen above, the l a s t p-use can be v e r i f i e d e x t e r n a l l y wh i l e the f i r s t two are v e r i f i a b l e o n l y i f the def of the v a r i a b l e " t p d u . s i z e " can be v e r i f i e d e x t e r n a l l y . For each of the l i s t e d v a r i a b l e s , a d e f - f r e e pa th has to be formed to b r i n g i t s def to a use . Note t h a t f o r the v a r i a b l e r e m o t e . r e f e r , s i n ce i t s u n v e r i f i e d usages appear on l y i n t 7 , t8 and t9 and i t s u n v e r i f i e d de fs appear i n o n l y t3a and t 3 b , on l y th ree d e f - f r e e paths are r e q u i r e d connec t i ng t3a to t 7 , t3b to t8 and t3a to t9 i n o rde r to v e r i f y a l l the de f s and the uses of t ha t v a r i a b l e . The reason i s because a use t ha t i s used to v e r i f y a de f d u r i n g t e s t i n g i s i t s e l f v e r i f i e d i n the p r o c e s s ! The f o l l o w i n g d e f - f r e e paths are formed, based on the augmented EFSM t a b l e , f o r each of the v a r i a b l e s l i s t e d above, r e m o t e . r e f e r : (def- & use-i tDFP) t 3 a . t 7 (def- & use-i tDFP) t 3 b . t 8 (use-itDFP) t 3 a . t 9 t p d u . s i z e : (def- & use-i tDFP) t 3 a . t 7 (def- & use-i tDFP) t 3 b . t 7 114 The Hybrid Technique c a l l i n g . t . a d d r : (use-itDFP) t 3 a . t 7 c a l l e d . t . a d d r : (use-itDFP) t 3 a . t 7 For the t p d u . s i z e v a r i a b l e , i t s de f s i n t r a n s i t i o n s t5a and t5b cannot r each the use i n t7 w i thout be ing r e - d e f i n e d f i r s t ; hence , the de fs i n these t r a n s i t i o n s cannot be e x t e r n a l l y observed and v e r i f i e d . T h i s a l s o i m p l i e s the e f f e c t o f the p-uses of the i n p u t parameter c c . i n . m a x . t p d u . s i z e at t r a n s i t i o n s t5a and t5b a l s o cannot be e x t e r n a l l y observed and v e r i f i e d . N e v e r t h e l e s s , s i n c e the v a r i a b l e t p d u . s i z e , i s used i n the same t r a n s i t i o n t h a t i t i s d e f i n e d i n , i t s use can s t i l l be e x e r c i s e d d u r i n g t e s t i n g by s imp ly execu t i ng the t r a n s i t i o n . The converse i s t r ue f o r the t p d u . s i z e v a r i a b l e d e f i n e d i n t r a n s i t i o n s t3a and t3b . These de fs can be d e f i n e d by t r a n s i t i o n t 7 . As a r e s u l t , the p-uses of c r . i n . m a x . t p d u . s i z e i n these t r a n s i t i o n s are a l s o v e r i f i e d . The de fs of the v a r i a b l e s i n . b u f f e r and o u t . b u f f e r are not used ; hence, they cannot be v e r i f i e d . However, s i n c e t h e i r de f s a s s i g n them va lues t h a t do not s a t i s f y the e n a b l i n g c o n d i t i o n s f o r the spontaneous t r a n s i t i o n s , the absences of the outputs produced by these spontaneous t r a n s i t i o n s d u r i n g t e s t i n g i n d i c a t e the de fs are c o r r e c t . Whenever neces sa r y , the de f- i tDFPs are s e l e c t e d to be i d e n t i c a l to the use- i tDFPs so tha t the f i n a l t e s t sequence 115 The Hybrid Technique may be r educed . The r e s u l t i n g i tDFPs to be v e r i f i e d i n the da ta f low t e s t i n g procedure are t 3 a . t 7 , t 3 b . t 8 , t 3 a . t 9 and t 3 b . t 7 ; t ha t i s , c r (opt ion=ok, max. tpdu . s i z e o n i l ) / t c i n d . t c r e s ( q t s . r e q < = q t s . e s t i m a t e ) / c c (def- & use- i tDFP ) c r ( op t i on=ok , m a x . t p d u . s i z e = n i l ) / t c i n d . t e r e s ( q t s . r e q > q t s . e s t i m a t e ) / d r , t d i n d , (def- & use-i tDFP) c r (opt ion=ok, max. tpdu . s i z e o n i l ) / t c i n d . t d r eq/d r (use-itDFP) c r ( op t i on=ok , m a x . t p d u . s i z e = n i l ) / t c i n d . t e r e s ( q t s . r e q < = q t s . e s t i m a t e ) / c c (def- & use- i tDFP ) For the d e f - i t D F P s , t h e i r da ta f low t e s t subsequences are formed by u s i n g p r e v i o u s l y used preambles to b r i n g the EFSM to each of t h e i r f i r s t t r a n s i t i o n s , then a postamble i s used to b r i n g the EFSM back to IDLE each t ime . I f any o f the i tDFPs i n c l u d e s t r a n s i t i o n s t ha t are e . t r a n s i t i o n s , a s p e c i a l preamble need to be formed to ensure e x e c u t a b i l i t y . T h i s preamble , i f not used be fo re i n the EFSM t e s t i n g p rocedu re , shou ld have i t s t a i l s t a t e v e r i f i e d p r i o r to i t s use . T h i s i s to ensure t ha t the de f- i tDFP indeed o r i g i n a t e d a t the c o r r e c t t r a n s i t i o n . For the use- i tDFPs , t h e i r t e s t subsequences are formed as f o l l o w s . For each use- i tDFP , the EFSM i s brought to i t s 116 The Hybrid Technique f i r s t t r a n s i t i o n aga in u s i n g a p r e v i o u s l y used preamble whenever p o s s i b l e , then the use- i tDFP i s conca tena ted to i t . The EFSM i s then brought back to the IDLE s t a t e u s i n g a postamble . The path formed by the preamble and the use-i tDFP , e x c l u d i n g the p o r t i o n t ha t beg ins at the t r a n s i t i o n hous ing the usage to be examined, must a l s o have i t s t a i l s t a t e v e r i f i e d to ensure the use examined indeed r e s i d e s a t the c o r r e c t t r a n s i t i o n . The f o l l o w i n g da ta f low t e s t subsequences are formed from the above fou r i t D F P s . DFTP: c r (opt ion=ok, max . t pdu . s i z e o n i l ) / t c i n d . t e r e s ( q t s . r e q < = q t s . e s t i m a t e ) / c c . t d r e q / n d r e q c r (opt ion=ok, max. tpdu . s i z e o n i l ) / t c i n d . t e r e s ( q t s . r e q < = q t s . e s t i m a t e ) / c c . t d r e q / n d r e q c r ( op t i on=ok , m a x . t p d u . s i z e = n i l ) / t c i n d . t e r e s ( q t s . r e q > q t s . e s t i m a t e ) / d r , t d i n d c r ( op t i on=ok , m a x . t p d u . s i z e = n i l ) / t c i n d . t e r e s ( q t s . r e q > q t s . e s t i m a t e ) / d r , t d i n d c r (opt ion=ok, max. tpdu . s i z e o n i l ) / t c i n d . t d r eq/d r c r ( op t i on=ok , m a x . t p d u . s i z e = n i l ) / t c i n d . t e r e s ( q t s . r e q < = q t s . e s t i m a t e ) / c c . t d r e q / n d r e q c r ( op t i on=ok , m a x . t p d u . s i z e = n i l ) / t c i n d . t e r e s ( q t s . r e q < = q t s . e s t i m a t e ) / c c . t d r e q / n d r e q 117 The Hybrid Technique S ince a l l the de f- i tDFPs beg in a t IDLE, a preamble i s not r e q u i r e d i n t h i s example. S ince the f i r s t t r a n s i t i o n a t each use- i tDFP has a l r e ady been used as a preamble from IDLE to WFTR i n t e s t i n g the EFSM p o r t i o n , t h e i r t a i l s t a t e s need not be v e r i f i e d a g a i n . Some of the sequences are d u p l i c a t e d because they r e p r e s e n t a de f- i tDFP as w e l l as a u se- i tDFP . A l l the paths end e i t h e r a t IDLE or DATA. For the l a t t e r ones , the postamble td req/ndreq i s used to b r i n g the EFSM from DATA back to IDLE. Added to the above t e s t subsequences are the f o l l o w i n g two subsequences f o r t e s t i n g t r a n s i t i o n s t6a and t 6 b . t c r e q ( q t s . r e q = o k , d i s c . r e a s o n = " u s e r . i n i t " ) / c r . d r / n d r e q , t d i n d t c r e q ( q t s . r e q = o k , d i s c . r e a s o n o " u s e r . i n i t " ) / c r . d r / n d r e q , t d i n d Length of the t e s t sequence f o r the da ta f low t e s t i n g procedure i s 22. A f t e r o p t i m i z a t i o n i n which d u p l i c a t e subsequences are removed, the l e n g t h i s reduced to 14 t e s t i n p u t s . I f these subsequences were compared to those i n the EFSM t e s t i n g procedure and the d u p l i c a t e s were removed, the number of t e s t i npu t s i n t h i s procedure would be f u r t h e r reduced to 7. 118 The Hybrid Technique 5.5 CHAPTER SUMMARY Th i s chapte r shows how the h y b r i d t echn ique can be a p p l i e d to the t e s t i n g of p r o t o c o l s implemented a c c o r d i n g to t h e i r E s t e l l e s p e c i f i c a t i o n s . In the t e s t i n g p rocedure , the spontaneous t r a n s i t i o n s are appended to those i npu t t r a n s i t i o n s t ha t enab le them. T h i s i s p o s s i b l e s i n ce t h e i r spon tane i t y s t i l l r e q u i r e t h a t t h e i r s t a r t i n g TSSs be s a t i s f i e d , which i n t u r n are enab led by the a p p r o p r i a t e i npu t t r a n s i t i o n s to which they are appended. I f the spontaneous t r a n s i t i o n s do not have C.TSSs t h a t can be enab led by any i npu t t r a n s i t i o n , then they shou ld not be appended to any i npu t t r a n s i t i o n . For the C l a s s 0 T r anspo r t P r o t o c o l example, the h y b r i d t echn ique would generate an op t im ized t e s t sequence of l e n g t h 83, where 76 t e s t i n p u t s are f o r t e s t i n g the EFSM s t r u c t u r e and 7 are f o r t e s t i n g the f low of d a t a . The l e n g t h of the f i n a l t e s t sequence v a r i e s a c c o r d i n g to the UIOSs chosen i n the EFSM t e s t i n g p rocedure . 119 6 EVALUATION AND COMPARISON OF THE HYBRID TECHNIQUE The h y b r i d techn ique i s a conformance t e s t sequence g e n e r a t i o n method tha t i s a p p l i c a b l e to t e s t i n g p r o t o c o l s implemented a c c o r d i n g to t h e i r E s t e l l e s p e c i f i c a t i o n s . The p r i n c i p l e s beh ind the method a r i s e from l e s sons l e a r n t from FSM t e s t i n g , where merely e x e r c i s i n g the f e a t u r e s i n an IUT a c c o r d i n g to i t s s p e c i f i c a t i o n i s not enough; whenever p o s s i b l e , those f e a t u r e s t ha t are not e x t e r n a l l y obse r vab l e shou ld be v e r i f i e d by o the r means. The i n t e r a c t i v e na tu re of p r o t o c o l s l end themselves w e l l to t h i s method of t e s t i n g . T h i s chapter p rov ides a gene ra l e v a l u a t i o n of the h y b r i d t echn ique as w e l l as a gene ra l compar ison o f t h i s method to o the r no tab l e t e s t sequence gene r a t i on t e c h n i q u e s . 6.1 EVALUATION 6.1.1 Fau l t Coverage S ince the h y b r i d techn ique i s a combina t ion of two t e s t i n g methods, i t s f a u l t d e t e c t i o n c a p a b i l i t y or f a u l t coverage i s a l s o a combinat ion of the f a u l t coverages produced by the two methods. F a u l t coverage of the h y b r i d t echn ique can be expressed i n terms of an er roneous E s t e l l e s p e c i f i c a t i o n . P ro v i ded no e x t r a STATE and statement e x i s t s i n the er roneous E s t e l l e 120 Evaluat ion and comparison s p e c i f i c a t i o n , the h y b r i d techn ique i s capab le of d e t e c t i n g a l l STATE e r r o r s , I/O p r i m i t i v e e r r o r s , e r r o r s i n those def and usage statements whose e f f e c t s are e x t e r n a l l y obse r vab l e and v e r i f i a b l e , and p o s s i b l y e r r o r s i n those de f and usage statements whose e f f e c t s are not v e r i f i a b l e or they c o n t a i n mathemat ica l e x p r e s s i o n s . These e r r o r s are d e t e c t a b l e i n a l l e r roneous IUTs tha t can be d e s c r i b e d by the e r roneous E s t e l l e s p e c i f i c a t i o n . 6.1.2 Executab i l i ty In the h y b r i d approach , s i n ce e n a b l i n g c o n d i t i o n s are taken i n t o c o n s i d e r a t i o n i n the p rocess of g e n e r a t i n g t e s t sequences , the r e s u l t i n g t e s t sequences are a l l e x e c u t a b l e . Ensu r i ng e x e c u t a b i l i t y i m p l i e s some t e s t da ta s e l e c t i o n has to be per formed d u r i n g the sequence g e n e r a t i o n p rocedu re . The d i sadvantage i s t ha t comp lex i t y i s added to the p roces s of sequence gene r a t i on and at t imes , computat ion may be r e q u i r e d . E x e c u t a b i l i t y r e q u i r e s t ha t the p r e s e n t a t i o n o f the r e s u l t i n g sequence of t e s t i npu t s be augmented by any s p e c i a l i n p u t va lue r e q u i r e d . Tes t da ta s e l e c t i o n can aga in be based on the b o u n d a r y - i n t e r i o r va lue c r i t e r i o n or done by choos ing the most commonly used va lues i n a r e a l imp lementa t i on . 121 Evaluat ion and comparison 6.1.3 App l i cab i l i t y The t e s t sequences genera ted by the h y b r i d t echn ique are t a i l o r e d f o r d e t e c t i n g e r r o r s i n an IUT which can be d e s c r i b e d by an erroneous E s t e l l e s p e c i f i c a t i o n . The t e s t sequences are e s p e c i a l l y s u i t e d to IUTs implemented a c c o r d i n g to E s t e l l e s p e c i f i c a t i o n s , but they can a l s o be a p p l i e d to any IUT independent of the type o f s p e c i f i c a t i o n from which i t i s genera ted . For IUTs tha t are not implemented a c c o r d i n g to E s t e l l e s p e c i f i c a t i o n s , the t e s t sequences are s t i l l capab le of d e t e c t i n g e r r o r s i n the da ta f low of the p r o t o c o l . These i n c l u d e f low paths t ha t would e x i s t w i t h i n a g i v en E s t e l l e t r a n s i t i o n as w e l l as those tha t would be a c ross sequences of E s t e l l e t r a n s i t i o n s . What the t e s t sequences may not d e t e c t i s an er roneous sequence of I/Os executed i n the IUT. The reason i s as f o l l o w s . R e c a l l t h a t i n a p r o t o c o l , I/Os not on l y assume c e r t a i n va lues (data f l o w ) , they a l s o assume c e r t a i n sequences ( c o n t r o l f l o w ) . I f the c o n t r o l s t r u c t u r e of an IUT had been implemented as a t r e e , then an e r roneous branch of the t r e e may not be de t e c t ed by sequences genera ted by the h y b r i d t e chn ique . The h y b r i d t echn ique takes advantage of the EFSM c o n t r o l s t r u c t u r e of a p r o t o c o l and a p p l i e s FSM-based t e s t i n g techn iques to check t h i s c o n t r o l s t r u c t u r e . Check ing the c o n t r o l s t r u c t u r e of such 122 Evaluat ion and comparison an IUT thus r e q u i r e s l e s s work; however, i t does r e q u i r e knowing tha t the s t r u c t u r e i s mode l led by an EFSM. An a l t e r n a t i v e to t e s t i n g IUTs whose c o n t r o l s t r u c t u r e s are unknown would be to span a t r e e a c c o r d i n g to the FSM i n the E s t e l l e s p e c i f i c a t i o n and t e s t the IUT f o r each branch i n the t r e e . However, when loops are encountered or i f the FSM i s o f c o n s i d e r a b l e s i z e , the r e s u l t i n g t e s t sequence cou ld be ho r r endous l y l o n g . Hence, knowing tha t the c o n t r o l s t r u c t u r e i s mode l led by an FSM and t a k i n g advantage of i t can c o n s i d e r a b l y reduce a t e s t sequence w i thout r e d u c i n g the f a u l t coverage p r o d u c i b l e . 6.1.4 Test Data Select ion The t e s t sequences generated s imp ly i n d i c a t e the sequences of I/Os t h a t shou ld be cons ide r ed d u r i n g t e s t i n g . Any s p e c i a l va lue r e q u i r e d f o r a t e s t i n p u t i s a l s o i n d i c a t e d i n a t e s t sequence generated by the h y b r i d t e c h n i q u e . Dur ing t e s t da ta s e l e c t i o n , a t e s t subsequence may need to be d u p l i c a t e d s i n ce more than one t e s t va lue may be used i n o rde r to t e s t the c o r r e c t n e s s of v a r i a b l e usages , r a t h e r than t h e i r e f f e c t s . The s e l e c t i o n of i n p u t v a lues c o u l d e i t h e r be based on b o u n d a r y - i n t e r i o r va lues or a chosen se t o f most f r e q u e n t l y used va lues i n a r e a l imp lementa t ion . I f the l a t t e r i s not a v a i l a b l e , the former 123 Evaluat ion and comparison can be used ; e l s e , the l a t t e r shou ld take p recedence . For p-uses, s i n ce i t can g e n e r a l l y be assumed t h a t a l l p o s s i b i l i t i e s are comple te l y s p e c i f i e d , each p o s s i b i l i t y would a l r e a d y be i n c l u d e d i n the t e s t sequence and need not be f u s sed over d u r i n g da ta s e l e c t i o n . T h i s a l s o a p p l i e s to c o n d i t i o n s w i th the keyword AND. I f "a AND b" were s p e c i f i e d , t hen , "NOT b" and "NOT a" would a l s o be s p e c i f i e d and t e s t da ta s e l e c t i o n does not have to take these a l t e r n a t i v e s i n t o c o n s i d e r a t i o n . 6.1.5 Tes tab i l i t y A p r o t o c o l can be made more e a s i l y t e s t a b l e w i th the a d d i t i o n of " s t a t u s " messages [Aho88, S a r i 8 4 ] . The " r ead s t a t e " message i s an i npu t which r e q u i r e s the IUT to r e p o r t the STATE tha t i t i s c u r r e n t l y a t . The a d d i t i o n o f t h i s f e a tu r e i m p l i e s UIOSs w i l l always e x i s t , each of which i s o f l e n g t h one. In a d d i t i o n , i f s y n c h r o n i z a t i o n were a problem [ S a r i 8 4 ] , then these s t a tus messages can be used t o a i d s y n c h r o n i z a t i o n i n the t e s t i n g of OSI p r o t o c o l s by r e q u i r i n g t h a t the IUT r e p o r t i t s c u r r e n t s t a t e to both upper and lower t e s t e r s as a means of s y n c h r o n i z i n g the two. Another way of i n c r e a s i n g t e s t a b i l i t y i s by comp le t i ng an i n c o m p l e t e l y s p e c i f i e d s p e c i f i c a t i o n [Sar i84] w i th one of the Completeness Assumpt ions . A "DEFAULT" f e a t u r e can be 124 Evaluat ion and comparison added to E s t e l l e s i m i l a r to the "PROVIDED o the rw i se " f e a t u r e t o s p e c i f y a Completeness Assumpt ion . For i n s t a n c e , , i f " o the rw i se " i s used to group a l l the u n s p e c i f i e d i n p u t p r i m i t i v e s t o g e t h e r , and "ANY_STATE" groups a l l the s t a t e s t o g e t h e r , then DEFAULT: WHEN otherw ise FROM ANY_STATE TO SAME BEGIN END; s p e c i f i e s the assumpt ion t ha t any i npu t not s p e c i f i e d f o r a s t a t e i s i gno red and the machine remains at i t s c u r r e n t s t a t e and no output i s genera ted . On the o the r hand, DEFAULT: WHEN otherwise FROM ANY_STATE TO ERROR BEGIN OUTPUT i n p u t _ e r r o r ( ) ; END; the above d e f a u l t sends the p r o t o c o l to the ERROR s t a t e a f t e r i t outputs a message comp la in ing of an i n p u t e r r o r [Sar i84] upon r e c e p t i o n of an u n s p e c i f i e d i n p u t . A t the 125 Evaluat ion and comparison ERROR s t a t e , a l l f u r t h e r i npu t s would be i gno red u n t i l a d i s c o n n e c t or r e s e t i npu t i s r e c e i v e d , a t which t ime the p r o t o c o l w i l l r e t u r n to the i n i t i a l IDLE s t a t e . These DEFAULT t r a n s i t i o n s are d e f a u l t s and shou ld be s p e c i f i e d as the l a s t t r a n s i t i o n s i n an E s t e l l e s p e c i f i c a t i o n , s i m i l a r to where "PROVIDED o the rw i se " i s s i t u a t e d i n a group o f r e l a t e d PROVIDED c l a u s e s . I f any m o d i f i c a t i o n to the s p e c i f i c a t i o n i s done so t ha t an u n s p e c i f i e d i npu t becomes a s p e c i f i e d one, no m o d i f i c a t i o n would be r e q u i r e d at the DEFAULT t r a n s i t i o n s . 6.2 COMPARISON The h y b r i d t echn ique i s compared to the FSM t e s t i n g t echn iques and those deve loped by U r a l [Ural88] and S a r i k a y a [Sar i87] i n t h i s s e c t i o n . These methods are compared based on t h e i r a p p l i c a t i o n s to t e s t i n g IUTs implemented a c c o r d i n g to E s t e l l e s p e c i f i c a t i o n s . In comparing the h y b r i d techn ique w i th FSM t e s t i n g t e c h n i q u e s , the h y b r i d techn ique i s o b v i o u s l y more comprehensive i n terms of f a u l t coverage because FSM t e s t i n g t echn iques examine on l y the c o n t r o l s t r u c t u r e of p r o t o c o l s wh i l e the h y b r i d techn ique a l s o examines i t s da ta f l ow . In a d d i t i o n , the t e s t sequences generated by the FSM t e chn iques 126 Evaluat ion and comparison may not be execu tab le wh i l e those generated by the h y b r i d t echn ique a r e . In comparing the h y b r i d techn ique w i th t h a t o f U r a l , s i n ce the da ta f low p o r t i o n of the p r o t o c o l i s a l s o t e s t e d i n the h y b r i d techn ique i n a d d i t i o n to the c o n t r o l s t r u c t u r e o f the IUT, the h y b r i d techn ique a l s o ach i eves b e t t e r coverage than tha t produced by U r a l . An example i s as f o l l o w s u s i n g the C l a s s 0 T r anspo r t P r o t o c o l . I f the c o n t r o l s t r u c t u r e of an erroneous implementa t ion o f the T r anspo r t P r o t o c o l were mode l led by an EFSM w i th on l y th ree STATES, f o r i n s t a n c e , the WFTR and WFCC s t a t e s were e r r o n e o u s l y merged i n t o a s i n g l e STATE; then U r a l ' s approach would not have been ab le to d e t e c t t h i s e r r o r . The r eason i s because the er roneous EFSM spans a t r e e p a r t o f which con t a i n s the t r e e spanned by the c o r r e c t EFSM. As a r e s u l t , a l l the da ta f low paths i n a c o r r e c t imp lementa t ion o f the p r o t o c o l would a l s o be p resen t i n the er roneous IUT. S ince U r a l ' s approach examines on l y the da ta f low p a t h s , i t would not have been ab le to d e t e c t the s t a t e e r r o r , but the h y b r i d approach would . Merging STATES WFCC and WFTR i s an e r r o r because , among the many e x t r a branches the er roneous EFSM spans , one of them i m p l i e s the 10 sequence c r / t c i n d . c c / t c c o n i s v a l i d which i s o b v i o u s l y i n c o r r e c t . I f t h i s e r r o r were not d e t e c t e d , the IUT cou ld go to i t s da ta t r a n s f e r s t a t e 127 Evaluat ion and comparison upon r e c e i v i n g a connect r eques t and a connect c o n f i r m a t i o n one a f t e r another from the peer p r o t o c o l w i thou t any response from i t s u s e r . The merged STATE i s thus an e r r o r and shou ld be c ap tu r ed . In terms of e x e c u t a b i l i t y , s i n ce the h y b r i d t echn ique takes e x e c u t a b i l i t y i n t o c o n s i d e r a t i o n d u r i n g i t s sequence g e n e r a t i o n p r o c e s s , the sequences i t genera tes would be execu tab le wh i l e those generated by U ra l may not be . In comparing the h y b r i d techn ique to t ha t of S a r i k a y a , the same erroneous T r anspo r t P r o t o c o l example can be used . S a r i k a y a ' s method aga in would not d e t e c t the u n d e r l y i n g er roneous EFSM because i t spans a t r e e t ha t i n c l u d e s the one spanned by the c o r r e c t EFSM. As a r e s u l t , a l l the subtours p resen t i n the c o r r e c t EFSM would a l s o be p resen t i n the er roneous EFSM; and a l l the data f lows p r e sen t i n the co r r e spond ing c o r r e c t IUT would a l s o be p resen t i n the er roneous IUT. Hence, the h y b r i d t echn ique p r o v i d e s b e t t e r coverage i n t h i s sense . In terms of t e s t d e r i v a t i o n comp l ex i t y , the h y b r i d t echn ique i s more complex than those f o r t e s t i n g FSMs and tha t of U r a l because i t has to do more than any one o f them does and, as w e l l , i t has to take e x e c u t a b i l i t y i n t o c o n s i d e r a t i o n . However, i n compar ison to the approach taken by S a r i k a y a , the h y b r i d techn ique seems s imp l e r because i t 128 Evaluat ion and comparison does not have to generate the complex da ta f low g raphs . The t e c h n i q u e , however, does r e q u i r e t a k i n g va lues i n t o c o n s i d e r a t i o n to ensure e x e c u t a b i l i t y and t e s t da ta may have to be s e l e c t e d d u r i n g the sequence gene r a t i on p rocedu re . In a d d i t i o n , i n the v e r i f i c a t i o n of p-uses, d i f f e r e n c e s among the e f f e c t s of the p-uses have to be i d e n t i f i e d so t h a t they may be used to v e r i f y the p-uses. Hence, the h y b r i d t echn ique demands t h a t more a t t e n t i o n be g i v en to the semant ics of the s p e c i f i c a t i o n than S a r i k a y a ' s does . In t h i s sense , the h y b r i d t echn ique i s more complex than t h a t o f S a r i k a y a . 129 7 CONCLUSIONS T h i s s e c t i o n b r i n g s t h i s t h e s i s to a c l o s e w i t h a summary of i t s achievements and a d i s c u s s i o n o f p o s s i b l e f u t u r e work i n the a rea of conformance t e s t i n g . 7.1 THESIS SUMMARY C o n t r i b u t i o n s of t h i s t h e s i s l i e i n th ree main a r e a s : the development o f the UlOv-method, the developments o f the eUIOv-method and the da ta f low t e s t i n g p r o c e d u r e , the f o rma t i on of the h y b r i d techn ique and i t s a p p l i c a t i o n to E s t e l l e . T h i s t h e s i s began by examining no tab l e FSM t e s t i n g t echn iques t h a t can be a p p l i e d to the conformance t e s t i n g o f p r o t o c o l s mode l led by FSMs. I t found , c o n t r a r y t o a p r e v i ous c l a im [S idh89 ] , t ha t the most r e c e n t l y deve loped UlO-method (U-method) does not p rov ide f u l l f a u l t coverage i n the t e s t i n g of comp le te l y s p e c i f i e d p r o t o c o l s . I t proposed add ing a v e r i f i c a t i o n p rocedu re , ~Uv, t o the U-method so t ha t the r e v i s e d U-method, or UlOv-method, a ch i eves f u l l f a u l t coverage i n s t rong conformance t e s t s . In weak conformance t e s t s , i t i s a l s o capab le of d e t e c t i n g f a u l t y IUTs p rov ided the number of s t a t e s i n these IUTs do not exceed tha t which i s i n the s p e c i f i e d FSM. The D-method 130 Conclusions and the W-method were found to be s p e c i a l cases o f the UIOv-method. T h i s t h e s i s a l s o proposed the concept of Unique Tes t Sequences (UTSs) to capture the p rope r t y a t e s t sequence shou ld have i n o rde r to ach ieve f u l l f a u l t cove rage . An UTS i s a sequence of I/Os tha t i s unique to the FSM from which i t i s genera ted so tha t any IUT tha t passes a t e s t u s i n g an UTS con t a i n s a s k e l e t o n FSM tha t i s i d e n t i c a l to the s p e c i f i e d FSM. As a r e s u l t , i f the number of s t a t e s i n the IUT does not exceed t h a t which i s i n the s p e c i f i c a t i o n FSM, then a l l f a u l t y IUTs can be captured by t e s t s employ ing UTSs. The UlOv-method generates such t e s t s . T h i s t h e s i s extended the UlOv-method to an eUIOv-method t o generate t e s t sequences f o r t e s t i n g p r o t o c o l s t h a t can be mode l l ed by EFSMs. The generated t e s t sequences are execu tab l e s i n ce the t o t a l s t a t e of the system i s taken i n t o c o n s i d e r a t i o n d u r i n g the gene r a t i on p r o c e s s . The t o t a l system s t a t e i s v e r i f i e d the same way a s t a t e i s i n an FSM. Hence, a l l e lements i n an EFSM t r a n s i t i o n are e x e r c i s e d and v e r i f i e d , whenever p o s s i b l e , d u r i n g t e s t i n g . T h i s t h e s i s deve loped a da ta f low t e s t i n g p rocedure based on s t a t i c da ta f low a n a l y s i s and l e s s o n s l e a r n t from FSM t e s t i n g . The procedure extends the b a s i c e x e r c i s i n g of def-use da ta f low paths to v e r i f y i n g , whenever p o s s i b l e , 131 Conclusions t h a t each def i s c o r r e c t , each use i s c o r r e c t and each p-use i s w i t h i n the c o r r e c t domain. T h i s t h e s i s r e f i n e d and r e fo rma t t ed the normal form o f an E s t e l l e s p e c i f i c a t i o n so t h a t i t s t r a n s i t i o n s are i n t rue normal form and i t s new format , the rNFS, s e p a r a t e l y b r i n g s out the u n d e r l y i n g EFSM and da ta f low from an E s t e l l e s p e c i f i c a t i o n . Dur ing EFSM t e s t i n g , redundant EFSM t r a n s i t i o n s t ha t appear i n an NFS are e l i m i n a t e d . The da ta f low t e s t i n g procedure i s combined w i th the eUIOv-method to form a h y b r i d techn ique t h a t i s a p p l i c a b l e to g e n e r a t i n g conformance t e s t sequences f o r p r o t o c o l s implemented a c c o r d i n g to t h e i r E s t e l l e s p e c i f i c a t i o n s . The r e s u l t i n g t e s t sequences d e t e c t f a u l t y IUTs t h a t e i t h e r have er roneous EFSM c o n t r o l s t r u c t u r e s or e r roneous 10 o p e r a t i o n s . The f a u l t coverage ach ieved by the h y b r i d t echn ique i s a combinat ion of those ach ieved by the eUIOv-method and the da ta f low t e s t i n g p rocedure . A c o r r e c t sequence of I/Os i s e q u a l l y impor tan t i n a p r o t o c o l as i t s I/O va lues a r e . T e s t i n g of a p r o t o c o l shou ld thus c o n s i d e r both of these a s p e c t s . FSMs can model the c o n t r o l s t r u c t u r e of some p r o t o c o l s e f f e c t i v e l y . S ince these models l end themselves w e l l to t e s t i n g , t h i s shou ld be taken advantage of when t e s t i n g such p r o t o c o l s so t h a t i t s c o n t r o l s t r u c t u r e as w e l l as i t s da ta f low aspec t can both 132 Conclusions be examined d u r i n g t e s t i n g . The h y b r i d t echn ique was deve loped to do j u s t t ha t f o r t h i s type of p r o t o c o l s . The h y b r i d techn ique was t a i l o r e d f o r p r o t o c o l s w i th u n d e r l y i n g EFSM c o n t r o l s t r u c t u r e s , t h i s t echn ique i s thus capab le of d e t e c t i n g f a u l t y IUTs w i th er roneous EFSMs t h a t would o therw ise be missed by the techn iques deve loped by U r a l and S a r i k a y a . S ince the h y b r i d t echn ique a l s o i n c l u d e s da ta f low t e s t i n g , i t i s capab le of d e t e c t i n g c e r t a i n t ypes of da ta f low e r r o r s i n an IUT tha t would o therw ise be missed by FSM t e s t i n g t e c h n i q u e s . The h y b r i d techn ique i s more complex than t h a t of U r a l and those f o r t e s t i n g FSMs; however, i t guarantees t h a t the r e s u l t i n g t e s t sequences are execu tab le and i t i s g e n e r a l l y l e s s complex than t h a t deve loped by S a r i k a y a . Tes t da ta s e l e c t i o n f o r the h y b r i d t echn ique e i t h e r employs a f i n i t e se t o f most f r e q u e n t l y used va lues f o r the i n p u t parameters o r , i f u n a v a i l a b l e , b o u n d a r y - i n t e r i o r va lues would be chosen. To ensure e x e c u t a b i l i t y , t e s t da ta s e l e c t i o n i s sometimes combined w i th t e s t sequence s e l e c t i o n . Tes t sequences generated by the h y b r i d t e chn ique are a l s o a p p l i c a b l e to IUTs not implemented a c c o r d i n g to t h e i r E s t e l l e s p e c i f i c a t i o n s . The f a u l t coverage ach i eved would 133 Conclusions be l i m i t e d to f a u l t s i n the I/Os; sequenc ing f a u l t s may o r may not be c ap tu red . 7.2 FUTURE WORK A t o o l i s be ing deve loped i n another s tudy to implement the h y b r i d t echn ique deve loped i n t h i s t h e s i s so t h a t i t can be e a s i l y a p p l i e d to more complex E s t e l l e p r o t o c o l s p e c i f i c a t i o n s . E x i s t i n g implementa t ion t echn iques f o r the UlO-method and s t a t i c da ta f low a n a l y s i s can be coup led w i th symbol i c e x e c u t i o n to implement the h y b r i d t e c h n i q u e . T h i s t h e s i s has emphasized on the f a u l t coverages ach ieved by the t e s t sequences; more r e s e a r c h i s r e q u i r e d to op t im i ze the r e s u l t i n g t e s t sequences such tha t t h e i r f a u l t d e t e c t i o n c a p a b i l i t i e s are ma in ta ined and the UTSs remain un ique . For t e s t da ta s e l e c t i o n , a l i s t o f commonly used parameter va lues shou ld be compi led so tha t they may be used as i n p u t s d u r i n g t e s t i n g . In the t e s t i n g of OSI p r o t o c o l s , more than one p r o t o c o l l a y e r may have been implemented as a s i n g l e u n i t so t h a t an IUT may be embedded w i t h i n a l a r g e imp lementa t ion . How such an IUT can be t e s t e d s t i l l needs to be i n v e s t i g a t e d . Perhaps the E s t e l l e s p e c i f i c a t i o n f o r each of the l a y e r s can be combined i n a manner s i m i l a r to t ha t o f an NFS so t h a t a 134 Conclusions s i n g l e s p e c i f i c a t i o n e x i s t s f o r the m u l t i - l a y e r imp lementa t ion . T h i s s p e c i f i c a t i o n may then be used to deve lop t e s t sequences to t e s t the m u l t i - l a y e r imp lementa t ion e i t h e r as a whole or one l a y e r a t a t ime . 135 BIBLIOGRAPHY [Aho88] Aho, A . V . , Dahbura, A . T . , Lee , D. and Uyar , U .M. , "An O p t i m i z a t i o n Technique f o r P r o t o c o l Conformance Tes t Gene ra t i on Based on UIO Sequences and Rura l Ch inese Postman T o u r s , " Proc. Eighth International Symposium on Protocol Specification, Testing, and Verification, A t l a n t i c C i t y , N . J . , 1988. [Chan89a] Chan, W .Y . L . , Vuong, S. and I t o , M.R., "On Tes t Gene ra t i on f o r P r o t o c o l s , " Proc. Ninth International Symposium on Protocol Specification, Testing and Verification, The Ne the r l ands , June 1989. [Chan89b] Chan, W .Y . L . , Vuong, S .T . and I t o , M.R., "An Improved P r o t o c o l Tes t Genera t ion Procedure Based on U IOs, " Proc. ACM Sigcomm '89 Symposium, Communications Architectures and Protocols, A u s t i n , Texas , September 1989 [Chan89c] Chan, W .Y . L . , Vuong, S .T . and I t o , M.R., "The UIOv-Method For P r o t o c o l T e s t i n g , " P roc . Second I n t e r n a t i o n a l Workshop on P r o t o c o l T e s t i n g , B e r l i n , Germany, October 1989. [Chow78] Chow, T. , " T e s t i n g Software Des ign Mode l l ed by F i n i t e S ta te Mach ines , " IEEE Transactions on Software Engineering, v o l SE-4, no. 3, 1978, pp. 178-187. 136 Bibl iography [Gone70] Gonenc, G . , "A Method f o r the Des ign of F a u l t D e t e c t i o n Expe r imen t s , " IEEE Transactions on Computers, v o l . C-19, no. 6, June 1970. [Hech77] Hecht , M.S. , Flow A n a l y s i s o f Computer Programs, New York : No r th-Ho l l and , 1977. [IS088] ISO/TC97/SC21/WGl/Subgroup B, " E s t e l l e - A Formal D e s c r i p t i o n Technique Based on an Extended S ta te T r a n s i t i o n M o d e l , " IS 9074, 1988. [Kou87] Kou, T . , "Conformance T e s t i n g o f OSI P r o t o c o l : The C l a s s 0 T r anspo r t P r o t o c o l As An Example , " Master T h e s i s , Dept . of Computer S c i e n c e , the U n i v e r s i t y o f B r i t i s h Co lumbia , August 1987. [Nait81] N a i t o , S. and Tsunoyama, M. , " F a u l t D e t e c t i o n f o r S e q u e n t i a l Machines by T r a n s i t i o n T o u r s , " Proc. of IEEE Fault Tolerant Computing Conference, 1981. [Rapp8 5] Rapps, S. and Weyuker, E . J . , " S e l e c t i n g Sof tware Tes t Data Us ing Data Flow I n f o r m a t i o n , " IEEE Transactions on Software Engineering, v o l . SE-11, no. 4, A p r i l 1985, pp. 367-375. [Rayn86] Rayner, D. , " S t a n d a r d i z i n g Conformance T e s t i n g f o r OS I , " Protocol Specification, Testing and Verification, V, M.D iaz , E d . , No r th-Ho l l and , Amsterdam, The Ne the r l ands , 1986. 137 Bibl iography [Sabn88] Sabnan i , K.K. and Dahbura, A . T . , "A P r o t o c o l Te s t Gene ra t i on P ro cedu re , " Computer Networks, v o l . 15, no. 4, 1988, pp. 285-297. [Sar i82] S a r i k a y a , B. and Bochmann, G . v . , "Some Expe r i ence w i th Tes t Sequence Gene ra t i on f o r P r o t o c o l s , " Protocol Specification, Testing and Verification, C. Sunsh ine , E d . , No r th-Ho l l and , 1982, pp . 555-567. [Sar i84] S a r i k a y a , B. and Bochmann, G . v . , " S y n c h r o n i z a t i o n and S p e c i f i c a t i o n Issues i n P r o t o c o l T e s t i n g , " IEEE Transactions on Communications, v o l . COM-32, no. 4, A p r i l 1984, pp. 389-395. [Sar i86] S a r i k a y a , B. and Bochmann, G . v . , " O b t a i n i n g Normal Form S p e c i f i c a t i o n s f o r P r o t o c o l s , " Computer Network Usage: Recent Experiences, L. Csaba , K. Tarnay and T . S z e n t i v a n y i ( E d s . , ) , No r th-Ho l l and , 1986, pp . 601-612. [Sar i87] S a r i k a y a , B., Bochmann, G . v . , and Cerny , E . , "A Tes t Des ign Methodology f o r P r o t o c o l T e s t i n g , " IEEE Transactions on Software Engineering, v o l . SE-13, no . 5, May 1987, pp. 518-531. [Sidh88] S i dhu , D. and Leung, T . , " Expe r i ence w i t h T e s t Gene ra t i on f o r Real P r o t o c o l s , " Proc. ACM Sigcomm '88 Symposium, Communications Architectures & Protocols, S t a n f o r d , C A . , August 1988, pp . 257-261. 138 Bibl iography [Sidh8 9] S i dhu , D.P. and Leung, T . K . , "Formal Methods f o r P r o t o c o l T e s t i n g : A D e t a i l e d S tudy , " IEEE Transactions on Software Engineering v o l . 15, no. 4, A p r i l 1989, pp . 413-426. [Ural88] U r a l , H. , Yang, B. and P r o b e r t , R . L . , "A Tes t Sequence S e l e c t i o n Method f o r P r o t o c o l s S p e c i f i e d i n E s t e l l e , " T e c h n i c a l Repor t , TR-88-18, The U n i v e r s i t y o f Ottawa, June 1988. [Vuon88a] Vuong, S . T . , Chan, R.I. and Chan, W .Y . L . , "An E s t e l l e - C Compi le r f o r Automat ic P r o t o c o l Imp lementa t ion , " Proc. Eighth International Symposium on Protocol Specification, Testing, and Verification, A t l a n t i c C i t y , New J e r s e y , USA, June 1988. [Vuon88b] Vuong, S .T . and Chan, W .Y . L . , " V a l i d a t i o n Of The F e r r y C l i p L o c a l T e s t i n g System Us ing An E s t e l l e - C C o m p i l e r , " Forte '88, First International Conference on Formal Description Techniques, the U n i v e r s i t y o f S t i r l i n g , September 1988. [Weiss85] We iser , M.D. , Gannon, J . D . and M c M u l l i n , P.R. , "Compar ison of S t r u c t u r a l Tes t Coverage M e t r i c s , " IEEE Software, March 1985, pp. 80-85. 139 Bibl iography [Zimm80] Zimmermann, H . , "OSI Reference Model - The ISO Model o f A r c h i t e c t u r e f o r Open Systems I n t e r c o n n e c t i o n , " IEEE Transactions on Communication, v o l . COM-28, no. 4, A p r i l 1980. 140 APPENDIX A NFS OF CLASS 0 TRANSPORT PROTOCOL WHEN t c r e q ( t o . t . a d d r , from t . a d d r , q t s . r e q ) FROM i d l e PROVIDED t c r e q . i n . q t s . r e q = ok TO wfcc t l : BEGIN l o c a l . r e f e r : = . . . ; t p d u . s i z e := . . . ; c r . o u t . c a l l i n g . t . a d d r := t c r e q . i n . f r o m . t . a d d r ; c r . o u t . c a l l e d . t . a d d r := t c r e q . i n . t o . t . a d d r ; OUT c r ( l o c a l . r e f e r , " n o r m a l " , c a l l i n g . t . a d d r , c a l l e d . t . a d d r , t p d u . s i z e ) ; END; WHEN t c r e q ( t o . t . a d d r , f r o m . t . a d d r , q t s . r e q ) FROM i d l e PROVIDED t c r e q . i n . q t s . r e q <> ok TO i d l e t 2 : BEGIN t d i n d . o u t . t s . d i s c . r e a s o n := . . . ; t d i n d . o u t . t s . u s e r . r e a s o n := . . . ; OUT t d i n d ( t s . d i s c . r e a s o n , t s . u s e r . r e a s o n ) ; END; WHEN c r ( s o u r c e . r e f , o p t i o n , c a l l i n g . t . a d d r , c a l l e d . t . a d d r , m a x . t p d u . s i z e ) FROM i d l e PROVIDED c r . i n . m a x . t p d u . s i z e <> n i l AND c r . i n . o p t i o n = ok TO w f t r t 3 : BEGIN r e m o t e . r e f e r := c r . i n . s o u r c e . r e f ; t p d u . s i z e := c r . i n . m a x . t p d u . s i z e ; c a l l i n g . t . a d d r := c r . i n . c a l l i n g . t . a d d r ; c a l l e d . t . a d d r := c r . i n . c a l l e d . t . a d d r ; q t s . e s t i m a t e := . . . ; OUT t c i n d ( c a l l e d . t . a d d r , c a l l i n g . t . a d d r , q t s . e s t i m a t e ) ; END; 141 NFS OF CLASS 0 TRANSPORT PROTOCOL WHEN c r ( s o u r c e . r e f , o p t i o n , c a l l i n g . t . a d d r , c a l l e d . t . a d d r , max . tpdu . s i z e ) FROM i d l e PROVIDED c r . i n . m a x . t p d u . s i z e = n i l AND c r . i n . o p t i o n = ok TO w f t r t 4 : BEGIN r e m o t e . r e f e r := c r . i n . s o u r c e . r e f ; t p d u . s i z e : = . . . ; c a l l i n g . t . a d d r := c r . i n . c a l l i n g . t . a d d r ; c a l l e d . t . a d d r := c r . i n . c a l l e d . t . a d d r ; q t s . e s t i m a t e := . . . ; OUT t c i n d ( c a l l e d . t . a d d r , c a l l i n g . t . a d d r , q t s . e s t i m a t e ) ; END; WHEN c r ( s o u r c e . r e f , o p t i o n , c a l l i n g . t . a d d r , c a l l e d . t . a d d r , m a x . t p d u . s i z e ) FROM i d l e PROVIDED c r . i n . o p t i o n <> ok TO i d l e t 5 : BEGIN d r . o u t . d e s t . r e f e r := c r . i n . s o u r c e . r e f ; d r . o u t . d i s c . r e a s o n := . . . ; OUT d r ( d e s t . r e f e r , d i s c . r e a s o n ) ; END; WHEN c c ( d e s t . r e f , s o u r c e . r e f , c a l l i n g . t . a d d r , c a l l e d . t . a d d r , m a x . t p d u . s i z e ) FROM wfcc PROVIDED c c . i n . m a x . t p d u . s i z e <> n i l TO da ta t 6 : BEGIN t p d u . s i z e := c c . i n . m a x . t p d u . s i z e ; q t s . e s t i m a t e := . . . ; i n . b u f f e r := n i l ; o u t . b u f f e r := n i l ; o u t . b u f f e r . s e t . m a x . s i z e ( t p d u . s i z e ) ; OUT t c c o n ( q t s . e s t i m a t e ) ; END; 142 NFS OF CLASS 0 TRANSPORT PROTOCOL WHEN c c ( d e s t . r e f , s o u r c e . r e f , c a l l i n g . t . a d d r , c a l l e d . t . a d d r , m a x . t p d u . s i z e ) FROM wfcc PROVIDED c c . i n . m a x . t p d u . s i z e = n i l TO data t 7 : BEGIN t p d u . s i z e := . . . ; q t s . e s t i m a t e := . . . ; i n . b u f f e r := n i l ; o u t . b u f f e r := n i l ; o u t . b u f f e r . s e t . m a x . s i z e ( t p d u . s i z e ) ; OUT t c c o n ( q t s . e s t i m a t e ) ; END; WHEN d r ( d i s c . r e a s o n , a d d . c l r . r e a s o n ) FROM wfcc PROVIDED d r . i n . d i s c . r e a s o n = " u s e r . i n i t " TO i d l e t 8 : BEGIN n d r e q . o u t . d i s c . r e a s o n := d r . i n . d i s c . r e a s o n ; t d i n d . o u t . t s . d i s c . r e a s o n := d r . i n . d i s c . r e a s o n ; t d i n d . o u t . t s . u s e r . r e a s o n := d r . i n . a d d . c l r . r e a s o n ; OUT n d r e q ( d i s c . r e a s o n ) ; OUT t d i n d ( t s . u s e r . r e a s o n , t s . d i s c . r e a s o n ) ; END; WHEN d r ( d i s c . r e a s o n , a d d . c l r . r e a s o n ) FROM wfcc PROVIDED d r . i n . d i s c . r e a s o n <> " u s e r . i n i t " TO i d l e t 9 : BEGIN n d r e q . o u t . d i s c . r e a s o n := d r . i n . d i s c . r e a s o n ; t d i n d . o u t . t s . d i s c . r e a s o n := d r . i n . d i s c . r e a s o n ; OUT n d r e q ( d i s c . r e a s o n ) ; OUT t d i n d ( t s . d i s c . r e a s o n ) ; END; 143 NFS OF CLASS 0 TRANSPORT PROTOCOL WHEN t e r e s ( q t s . r e q ) FROM w f t r PROVIDED t e r e s . i n . q t s . r e q <= q t s . e s t i m a t e TO da ta t l O : BEGIN l o c a l . r e f e r := . . . ; i n . b u f f e r := n i l ; o u t . b u f f e r := n i l ; o u t . b u f f e r . s e t . m a x . s i z e ( t p d u . s i z e ) ; OUT c c ( r e m o t e . r e f e r , l o c a l . r e f e r , c a l l i n g . t . a d d r , c a l l e d . t . a d d r , t p d u . s i z e ) ; END; WHEN t e r e s ( q t s . r e q ) FROM w f t r PROVIDED t e r e s . i n . q t s . r e q > q t s . e s t i m a t e TO i d l e t i l : BEGIN d r . o u t . d i s c . r e a s o n := . . . ; d r . o u t . a d d . c l r . r e a s o n : = . . . ; t d i n d . o u t . t s . d i s c . r e a s o n := . . . ; OUT d r ( r e m o t e . r e f e r ; d i s c . r e a s o n , a d d . c l r . r e a s o n ) ; OUT t d i n d ( t s . d i s c . r e a s o n ) ; END; WHEN t d r e q ( t s . u s e r . r e a s o n ) FROM w f t r TO i d l e t l 2 : BEGIN d r . o u t . d i s c . r e a s o n := . . . ; d r . o u t . a d d . c l r . r e a s o n := t d r e q . i n . t s . u s e r . r e a s o n ; OUT d r ( r e m o t e . r e f e r , d i s c . r e a s o n , a d d . c l r . r e a s o n ) ; END; WHEN t d a t r ( t s d u . f r a g m e n t ) FROM da ta TO da ta t l 3 : BEGIN i n s e r t ( o u t . b u f f e r , t d a t r . i n . t s d u . f r a g m e n t ) ; END; 144 NFS OF CLASS 0 TRANSPORT PROTOCOL FROM data PROVIDED o u t . b u f f e r <> n i l TO da ta t l 4 : BEGIN r e m o v e ( o u t . b u f f e r , d t . o u t . u s e r . d a t a ) ; OUT d t ( u s e r . d a t a ) ; END; WHEN d t ( u s e r . d a t a ) FROM da ta TO da ta t l 5 : BEGIN i n s e r t ( i n . b u f f e r , d t . i n . u s e r . d a t a ) END; FROM data PROVIDED i n . b u f f e r <> n i l TO da ta t l 6 : BEGIN r e m o v e ( i n . b u f f e r , t d a t i . o u t . t s d u . f r a g m e n t ) ; OUT t d a t i ( t s d u . f r a g m e n t ) ; END; WHEN t d r e q ( t s . u s e r . r e a s o n ) FROM da ta TO i d l e t l 7 : BEGIN n d r e q . o u t . d i s c . r e a s o n := t d r e q . i n . t s . u s e r . r e a s o n ; OUT n d r e q ( d i s c . r e a s o n ) ; END; WHEN nd ind ( ) FROM da ta TO i d l e t l 8 : BEGIN t d i n d . o u t . t s . d i s c . r e a s o n := . . . ; OUT t d i n d ( t s . d i s c . r e a s o n ) ; END; 145 NFS OF CLASS 0 TRANSPORT PROTOCOL WHEN n r i n d ( ) FROM data TO i d l e t l 9 : BEGIN t d i n d . o u t . t s . d i s c . r e a s o n := OUT t d i n d ( t s . d i s c . r e a s o n ) ; END; 146 APPENDIX B RNFS OF CLASS 0 TRANSPORT PROTOCOL t l : WHEN t c r e q ( q t s . r e q = ok) FROM i d l e TO wfcc OUT c r BEGIN l o c a l . r e f e r := . . . ; c r . o u t . s o u r c e . r e f e r := l o c a l . r e f e r ; c r . o u t . o p t i o n := " n o r m a l " ; t p d u . s i z e := . . . ; c r . o u t . m a x . t p d u . s i z e := t p d u . s i z e ; c r . o u t . c a l l i n g . t . a d d r := t c r e q . i n . f r o m . t . a d d r ; c r . o u t . c a l l e d . t . a d d r := t c r e q . i n . t o . t . a d d r ; END; t 2 : WHEN t c r e q ( q t s . r e q <> ok) FROM i d l e TO i d l e OUT t d i n d BEGIN t d i n d . o u t . t s . d i s c . r e a s o n := . . . ; t d i n d . o u t . t s . u s e r . r e a s o n := . . . ; END; t 3 a : WHEN c r ( o p t i o n = ok) FROM i d l e TO w f t r AND q t s . e s t i m a t e := . . . ; OUT t c i n d PROVIDED ( c r . i n . m a x . t p d u . s i z e <> n i l ) BEGIN r e m o t e . r e f e r := c r . i n . s o u r c e . r e f ; t p d u . s i z e := c r . i n . m a x . t p d u . s i z e ; c a l l i n g . t . a d d r := c r . i n . c a l l i n g . t . a d d r ; t c i n d . o u t . f r o m . t . a d d r := c a l l i n g . t . a d d r ; c a l l e d . t . a d d r := c r . i n . c a l l e d . t . a d d r ; t c i n d . o u t . t o . t . a d d r := c a l l e d . t . a d d r ; q t s . e s t i m a t e : = . . . ; t c i n d . o u t . q t s . p r o := q t s . e s t i m a t e ; END; 147 rNFS OF CLASS 0 TRANSPORT PROTOCOL t3b : WHEN c r ( o p t i o n = ok) FROM i d l e TO w f t r AND q t s . e s t i m a t e := . . . OUT t c i n d PROVIDED ( c r . i n . m a x . t p d u . s i z e = n i l ) BEGIN r e m o t e . r e f e r := c r . i n . s o u r c e . r e f ; t p d u . s i z e := . . . ; c a l l i n g . t . a d d r := c r . i n . c a l l i n g . t . a d d r ; t c i n d . o u t . f r o m . t . a d d r := c a l l i n g . t . a d d r ; c a l l e d . t . a d d r := c r . i n . c a l l e d . t . a d d r ; t c i n d . o u t . t o . t . a d d r := c a l l e d . t . a d d r ; q t s . e s t i m a t e : = . . . ; t c i n d . o u t . q t s . p r o := q t s . e s t i m a t e ; END; t 4 : WHEN c r ( o p t i o n <> ok) FROM i d l e TO i d l e OUT dr BEGIN d r . o u t . d e s t . r e f e r := c r . i n . s o u r c e . r e f ; d r . o u t . d i s c . r e a s o n := END; t 5 a : WHEN cc FROM wfcc TO da ta AND BEGIN i n . b u f f e r := n i l ; o u t . b u f f e r := n i l ; q t s . e s t i m a t e := . . . ; END; OUT t c con PROVIDED ( c c . i n . m a x . t p d u . s i z e <> n i l ) BEGIN q t s . e s t i m a t e := . . . ; t c c o n . o u t . q t s . e s t i m a t e := q t s . e s t i m a t e ; i n . b u f f e r := n i l ; o u t . b u f f e r := n i l ; t p d u . s i z e := c c . i n . m a x . t p d u . s i z e ; o u t . b u f f e r . s e t . m a x . s i z e ( t p d u . s i z e ) ; END; 148 rNFS OF CLASS 0 TRANSPORT PROTOCOL t 5 b : WHEN CC FROM wfcc TO data AND BEGIN i n . b u f f e r : = n i l ; o u t . b u f f e r := n i l ; q t s . e s t i m a t e := . . . ; END; OUT t c con PROVIDED ( c c . i n . m a x . t p d u . s i z e = n i l ) BEGIN q t s . e s t i m a t e := . . ; t c c o n . o u t . q t s . r e s := q t s . e s t i m a t e ; i n . b u f f e r := n i l ; o u t . b u f f e r := n i l ; t p d u . s i z e := . . . ; o u t . b u f f e r . s e t . m a x . s i z e ( t p d u . s i z e ) ; END; t 6 a : WHEN dr FROM wfcc TO i d l e OUT nd req , t d i n d PROVIDED ( d r . i n . d i s c . r e a s o n = " u s e r . i n i t " ) BEGIN n d r e q . o u t . d i s c . r e a s o n := d r . i n . d i s c . r e a s o n ; t d i n d . o u t . t s . d i s c . r e a s o n := d r . i n . d i s c . r e a s o n ; t d i n d . o u t . t s . u s e r . r e a s o n : = d r . i n . a d d . c l r . r e a s o n ; END; t 6 b : WHEN dr FROM wfcc TO i d l e OUT ndreq , t d i n d PROVIDED ( d r . i n . d i s c . r e a s o n <> " u s e r . i n i t " ) BEGIN n d r e q . o u t . d i s c . r e a s o n := d r . i n . d i s c . r e a s o n ; t d i n d . o u t . t s . d i s c . r e a s o n := d r . i n . d i s c . r e a s o n ; END; 149 rNFS OF CLASS 0 TRANSPORT PROTOCOL t 7 : WHEN t e r e s ( q t s . r e q <= .q t s . e s t ima te ) FROM w f t r TO data AND BEGIN i n . b u f f e r := n i l ; o u t . b u f f e r := n i l ; END; OUT CC BEGIN l o c a l . r e f e r := . . . ; c c . o u t . d e s t . r e f e r := r e m o t e . r e f e r ; c c . o u t . s o u r c e . r e f e r := l o c a l . r e f e r ; c c . o u t . c a l l i n g . t . a d d r := c a l l i n g . t . a d d r ; c c . o u t . c a l l e d . t . a d d r := c a l l e d . t . a d d r ; c c . o u t . m a x . t p d u . s i z e := t p d u . s i z e ; i n . b u f f e r := n i l ; o u t . b u f f e r := n i l ; o u t . b u f f e r . s e t . m a x . s i z e ( t p d u . s i z e ) ; END; t 8 : WHEN t e r e s ( q t s . r e q > q t s . e s t i m a t e ) FROM w f t r TO i d l e OUT d r , t d i n d BEGIN d r . o u t . d e s t . r e f e r := r e m o t e . r e f e r ; d r . o u t . d i s c . r e a s o n := . . . ; d r . o u t . a d d . c l r . r e a s o n := . . . ; t d i n d . o u t . t s . d i s c . r e a s o n := . . . ; END; t 9 : WHEN t d r e q FROM w f t r TO i d l e OUT dr BEGIN d r . o u t . d i s c . r e a s o n := . . . ; d r . o u t . a d d . c l r . r e a s o n := t d r e q . i n . u s e r . r e a s o n ; d r . o u t . d e s t . r e f e r := r e m o t e . r e f e r ; END; 150 rNFS OF CLASS 0 TRANSPORT PROTOCOL t l O : WHEN t d a t r ( t s d u . f r a g m e n t ) FROM data TO data AND i n s e r t ( o u t . b u f f e r , t d a t r . i n . t s d u . f r a g m e n t ) BEGIN i n s e r t ( o u t . b u f f e r , t d a t r . i n . t s d u . f r a g m e n t ) ; END; t i l : FROM da ta AND o u t . b u f f e r <> n i l TO da ta AND r e m o v e ( o u t . b u f f e r , d t . o u t . u s e r . d a t a ) OUT d t BEGIN r e m o v e ( o u t . b u f f e r , d t . o u t . u s e r . d a t a ) ; END; t l 2 : WHEN d t FROM data TO data AND i n s e r t ( i n . b u f f e r , d t . i n . u s e r . d a t a ) BEGIN i n s e r t ( i n . b u f f e r , d t . i n . u s e r . d a t a ) ; END; t l 3 : FROM data AND i n . b u f f e r <> n i l TO da ta AND r e m o v e ( i n . b u f f e r , t d a t i . o u t . t s d u . f r a g m e n t ) OUT t d a t i BEGIN r e m o v e ( i n . b u f f e r , t d a t i . o u t . t s d u . f r a g m e n t ) ; END; t l 4 : WHEN t d r e q FROM data TO i d l e OUT ndreq BEGIN n d r e q . o u t . d i s c . r e a s o n : = t d r e q . i n . t s . u s e r . r e a s o n ; END; 151 rNFS OF CLASS 0 TRANSPORT PROTOCOL t l 5 : WHEN nd ind FROM data TO i d l e OUT t d i n d BEGIN t d i n d . o u t . t s . d i s c . r e a s o n := . . . ; END; t l 6 : WHEN n r i n d FROM da ta TO i d l e OUT t d i n d BEGIN t d i n d . o u t . t s . d i s c . r e a s o n := . . . ; END; 152 

Cite

Citation Scheme:

        

Citations by CSL (citeproc-js)

Usage Statistics

Share

Embed

Customize your widget with the following options, then copy and paste the code below into the HTML of your page to embed this item in your website.
                        
                            <div id="ubcOpenCollectionsWidgetDisplay">
                            <script id="ubcOpenCollectionsWidget"
                            src="{[{embed.src}]}"
                            data-item="{[{embed.item}]}"
                            data-collection="{[{embed.collection}]}"
                            data-metadata="{[{embed.showMetadata}]}"
                            data-width="{[{embed.width}]}"
                            async >
                            </script>
                            </div>
                        
                    
IIIF logo Our image viewer uses the IIIF 2.0 standard. To load this item in other compatible viewers, use this url:
https://iiif.library.ubc.ca/presentation/dsp.831.1-0064927/manifest

Comment

Related Items