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 U n i v e r s i t y of B r i t i s h Columbia, 1987 A THESIS SUBMITTED IN PARTIAL FULFILMENT OF THE REQUIREMENTS  FOR THE DEGREE OF  MASTER OF APPLIED SCIENCE in THE FACULTY OF GRADUATE STUDIES (DEPARTMENT OF ELECTRICAL ENGINEERING)  We accept t h i s t h e s i s as conforming t o the r e q u i r e d standard  THE UNIVERSITY OF BRITISH COLUMBIA August 198 9 ©  Wendy Yuen-Ling Chan, 1989  In  presenting this  degree at the  thesis  in  partial  fulfilment  of  the  requirements  University  of  British  Columbia,  I agree that the  freely available for reference and study. I further agree that copying  of  department  this thesis for scholarly or  by  his  or  her  purposes may be  representatives.  It  is  for  an  Library shall make it  permission for extensive  granted by the understood  head of my  that  publication of this thesis for financial gain shall not be allowed without permission.  Department of  ELECTRICAL ENGINEERING  The University of British Columbia Vancouver, Canada Date  DE-6 (2/88)  1989  AUGUST 10  advanced  copying  or  my written  ABSTRACT This thesis applicable  to  UlOv-method, The  developed three  the  the  passes to  UlOv-method  its  the  tests  eUIOv-method modelled  by  procedure is  parameters  to  is  protocols  and t h e  for  FSM.  The  extended  FSMs  (EFSMs).  b a s e d on s t a t i c  developed  in  and v a r i a b l e s  this in  applicable  to  The  technique  EFSM c o n t r o l  structures  state  conformance  machines,  machines,  data  unique flow,  testing,  fault  ii  flow  testing and  FSM of  This  procedure  is  hybrid  testing  technique  of  complex  their  Estelle  protocols  with  c a n n o t be d e t e c t e d  protocols,  coverage,  be  flow  captures  input/outputs,  can  the  e x i s t i n g t e s t i n g methods d e v e l o p e d by S a r i k a y a  KEYWORDS:  the  test  to  that  to  that  analysis  form the  according  that  identical  extended  flow to  the  protocols  is  data  a protocol. to  implemented  A  thesis  eUIOv-method  directly  that  protocols  data  the  Any p r o t o c o l  is  are  technique.  simple  UlOv-method complex  that  protocols:  hybrid  (FSMs).  more  (DFTP)  of  testing  test  specifications. erroneous  testing  s t a t e machines  augmented w i t h t h e which  is  techniques  p o s s e s s e s an FSM s k e l e t o n  specified  testing  conformance  eUIOv-method  m o d e l l e d by f i n i t e  testing  and  protocol  Ural.  Estelle,  extended  by  finite  finite state  specification.  TABLE OF CONTENTS  Abstract Table of  ii Contents  List  of  Figures  List  of  Tables...  iii vi vii  Acknowledgement  viii  1 Introduction 1.1 P a s t T e s t G e n e r a t i o n E f f o r t 1. 2 T h e s i s G o a l 1.3 T h e s i s C o n t r i b u t i o n s 1.4 T h e s i s O r g a n i z a t i o n  1 3 3 5 7  2 The UIOv-Method 2.1 The F i n i t e S t a t e M a c h i n e Model 2.2 FSM T e s t i n g T e c h n i q u e s 2 . 2 . 1 The T-Method 2 . 2 . 2 The W-Method 2 . 2 . 3 The D-Method 2 . 2 . 4 The U-Method 2 . 2 . 5 Comments on t h e F o u r Methods 2.2.5.1 A p p l i c a b i l i t y 2 . 2 . 5 . 2 F a u l t Coverage 2.3 The S h o r t c o m i n g o f t h e U-Method 2.3.1 Assumptions 2 . 3 . 2 The UIOS P r o b l e m 2 . 3 . 3 The S t a t e S i g n a t u r e P r o b l e m 2.4 The UIOv-Method 2.4.1 Uniqueness Problem A n a l y s i s 2 . 4 . 2 ~Uv 2.4.3 IO(S,K)s 2 . 4 . 4 C o m p a r i n g t h e UIOv-Method w i t h t h e O t h e r s 2.5 U n i q u e T e s t Sequences 2.6 FSM T e s t i n g 2.7 C h a p t e r Summary  8 9 11 11 11 12 13 14 14 15 18 18 19 23 25 26 27 28 31 33 37 38  3 T e s t i n g Extended F i n i t e S t a t e Machines 3.1 B a c k g r o u n d 3.2 The EFSM T a b l e 3.3 E x t e n s i o n o f t h e UIOv-Method 3.3.1 UIOSs S e l e c t i o n i n an EFSM  41 41 42 44 45  iii  Table o f C o n t e n t s 3 . 3 . 2 V e r i f i c a t i o n o f TSS V a r i a b l e s 3 . 3 . 2 . 1 V e r i f i c a t i o n o f N.TSSs 3.3.2.2 V e r i f i c a t i o n of C.TSSs 3 . 3 . 2 . 3 UIOSs f o r TSSs 3 . 3 . 3 The eUIOv-Method 3 . 3 . 4 An Example 3 . 3 . 5 Summary o f t h e eUIOv-Method 3.4 F a u l t C o v e r a g e 4 Data 4.1 4.2 4.3 4.4 4.5 4.6 4.7  Flow T e s t i n g S t a t i c Data Flow A n a l y s i s Data Flow Paths D a t a Flow T e s t i n g The D a t a F l o w T e s t i n g P r o c e d u r e An Example C h a p t e r Summary Comments on t h e DFTP  48 49 51 53 54 57 61 62 64 65 66 67 70 72 75 77  5 The H y b r i d T e c h n i q u e 5.1 B a c k g r o u n d 5.1.1 E s t e l l e 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 5 . 1 . 2 . 1 Example o f an NFS 5.2 R e f i n i n g t h e NFS 5.2.1 C a n o n i c a l T r a n s i t i o n s 5 . 2 . 2 R e f o r m a t t i n g t h e NFS 5 . 2 . 2 . 1 E x e c u t a b i l i t y Problems 5 . 2 . 2 . 2 The R e f o r m a t t e d NFS 5 . 2 . 2 . 3 The E n a b l i n g C o n d i t i o n s 5 . 2 . 2 . 4 The Def S t a t e m e n t s 5 . 2 . 2 . 5 Format o f t h e rNFS 5.3 E s t e l l e EFSM T e s t i n g 5.3.1 S p o n t a n e o u s T r a n s i t i o n s 5 . 3 . 2 T e s t i n g t h e EFSM i n t h e COTP 5.4 E s t e l l e D a t a f l o w T e s t i n g 5.4.1 D a t a F l o w T e s t i n g f o r t h e COTP 5.5 C h a p t e r Summary  80 82 82 84 85 87 87 89 89 90 91 91 92 94 96 97 105 107 119  6 E v a l u a t i o n and C o m p a r i s o n o f t h e 6.1 E v a l u a t i o n 6.1.1 F a u l t Coverage 6.1.2 E x e c u t a b i l i t y 6.1.3 A p p l i c a b i l i t y 6 . 1 . 4 T e s t Data S e l e c t i o n 6.1.5 T e s t a b i l i t y 6.2 C o m p a r i s o n  120 120 120 121 122 123 124 126  7 Conclusions  Hybrid Technique  130  iv  7.1  7.2  T h e s i s Summary  F u t u r e Work . . .  Bibliography 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 2.2 A f a u l t y  IUT  o f t h e FSM i n F i g u r e  2.3 An FSM w i t h no UIOS f o r 2.4 A f a u l t y  20  state  2.1  C  i m p l e m e n t a t i o n o f t h e FSM i n F i g u r e  2.5 A s i m p l e FSM w i t h  an i n h e r e n t UTS  vi  21 24 2.3  25 35  LIST OF TABLES 2.1  U-method t e s t  sequence f o r  the  FSM i n F i g u r e  2.2  D-method t e s t  sequence f o r F i g u r e  2.3  U-method t e s t  s e q u e n c e f o r FSM i n F i g u r e  2.4  UlOv-method t e s t  sequence f o r  the  FSM i n F i g u r e  2.1...28  2.5  UlOv-method t e s t  sequence f o r the  FSM i n F i g u r e  2.3...30  2.1  21 22  2.3  3 . 1 An EFSM t a b l e for  2.1  24  44  5.1  EFSM t a b l e  the C l a s s  5.2  Augmented EFSM t a b l e  0 Transport Protocol  for Class  vii  0 Transport  95  Protocol..109  ACKNOWLEDGEMENT I w o u l d l i k e t o t h a n k D r . Son Vuong f o r h i s g u i d a n c e and f o r h i s c o n s t a n t e n c o u r a g e m e n t s t h a t I p u b l i s h my w o r k . I w o u l d l i k e t o t h a n k D r . Mabo I t o f o r h i s c a r e f u l r e a d i n g o f t h i s t h e s i s and f o r h i s h e l p i n i m p r o v i n g my w r i t i n g tremendously. I w o u l d l i k e t o t h a n k D r . Sam C h a n s o n 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 m o r a l support during d i f f i c u l t times. A l s o , a very s p e c i a l thank you t o D r . G u n t h e r S c h r a c k , w i t h o u t h i m , I w o u l d n o t have b e e n a b l e t o become a g r a d u a t e s t u d e n t . I would like to thank the Natural Sciences 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 s u p p o r t i n the., form o f an U n i v e r s i t y and I n d u s t r y Cooperative Research Grant. L a s t l y , many h e a r t f e l t t h a n k s t o my p a r e n t s f o r t h e i r i m m e a s u r a b l e l o v e and u n d e r s t a n d i n g ; and e s p e c i a l l y t o my brother, Ramsey, and my fiance, Dawson, for their c o n t i n u o u s m o r a l s u p p o r t and t h e i r immense f a i t h i n me; w i t h o u t t h e m , t h i s work w o u l d n o t have been p o s s i b l e .  viii  Introduction D u r i n g conformance t e s t i n g , under  test  since  its  is  carried  out of  protocol  is  source  sequence  via  (IUT)  typically  code  is  using  test  received  IUT  is  The  its  output  ability IUTs  sequence  used.  received  much  particular,  of  control  extended aspect  of  a  during  the  test  sequences  interest  in this  structure  of  finite  state  the  protocol  of  statements.  detect  depends  the  thesis  machine is  sequence  by  is  from  a the  to  the  IUT  the  IUT  are  If  with they  the  match,  non-conforming solely  sequence  on  formal  described  is  in  formal  In  Estelle,  modelled  while  the  data  by  set  of  a  has  specification  Estelle.  protocol (EFSM)  the  or test  community;  from  is  the  generation  research  The  the  Testing  compared  generated  protocols.  box"  specification.  test  from  "black  applied  sequence.  to  testing  attention  of  the  are  and  test  a  derived  generated  port  Recently,  specification  the  in  as  accessible.  pairs  outputs  implementation  A test  inputs  s a i d to conform to  erroneous  language  Test  The  corresponding outputs the  (I/O)  port.  via  not  sequences.  input/output  input  protocol  considered  generally  specification.  its  the  as  an flow  Pascal  Introduction  1.1 PAST TEST GENERATION Recent Estelle  work  on  protocol  [Sari87]  aspect  form  Estelle  sequence  of  protocol  testing  finite  [Sabn88,  and b o t h  These  specifications  Sidh89],  the  Aho88].  the  of  examine o n l y  structure  interaction problems these  primitive  when  methods  parameters  applied are  to  Estelle  directly  simple p r o t o c o l s that  from  for  and  W-method  the  U-method  conformance  T h e s e methods  face  they  ignore  executability  specifications.  c a n be m o d e l l e d by  Sari82,  the  of p r o t o c o l s ;  to  test  developed  to p r o t o c o l  applicable  normal  to  [Nait81];  and may  data  applicable  [Kou87,  [Sidh89].  on  Sarikaya  notable  those  [Gone70],  Their applications  control  are  (FSMs)  studied in  the  Other  include  t e s t i n g were e x t e n s i v e l y  of  whom work  that  T-method  D-method  based  whom e m p h a s i z e t h e  machines  include  those  [Sari86].  techniques  state  generation  include  both of  specifications  generation  Sidh89].  sequence  [Ural88],  protocols  Estelle  [Chow78,  test  specifications  and U r a l  flow  EFFORT  the  However, testing  of  FSMs.  1.2 THESIS GOAL The techniques  goal for  of the  this  thesis  conformance  t h a t maximum f a u l t  coverage  is  thesis  defined in this  is  to  testing  develop of  can be a c h i e v e d .  a c c o r d i n g to the  3  testing  protocols Fault  such  coverage  specifications  of  Introduction the  protocols  primary test  used.  concern  in  here:  in  sequences g e n e r a l l y optimization.  test  two  issues  sequence  sequence. of  generation  fall  into  to  coverage  achieve  deals  two  desirable follow.  with  test,  it  fault  coverage  This issue  is  deals  a  thesis  to  in  secondary  thus  test  with  of and  to  focuses  on  the  their  followed.  testing  Open System upper  available  may be e a s i l y  the  IUT  of  Interconnection  tester i n .this  and  a  thesis  t h e u p p e r and l o w e r  a  protocol  (OSI)  lower  to provide  interfaces  4  test  reduce Only  the  when  a  optimization important  Some  sample  n o t o p t i m i z e d so  that  are  control  of the  generate  given  more  Reference tester  and  coverage,  to  sequence g e n e r a t i o n .  that  In  a  should  are  to  fault  coverage.  thesis  intents  how  necessary  achieved  test  coverage  optimize  sequences generated i n t h i s  at  not  conformance  particular  how  is  of  test  an  are  optimization  categories:  Although optimization i s a  coverage  the  While  sequences  optimization  cost  following  architecture. Problems  test  The  IUT.  belongs Model  the  [Zimm80],  assumed and  to  to  be  observation  Introduction  1.3 THESIS  CONTRIBUTIONS  This  thesis  generating their  contributes  conformance  specifications This  thesis  inadequate  and  i n the  modified  all  Its  detection  fault  I/O  cases  developed  in  this  applicability advantage  the  for  so  protocols  U-method  it  as  state  is  now  thesis  where of  the  D-method  U-method  the  to  be of  [Chan89b]. to  those  of  actually  (UlOv-method)  UlOv-method  W-method  while  from  capable  errors  now e q u i v a l e n t  modified  of  ways.  that  is  problem  The D-method and W-method a r e the  the  the  original  as w e l l  advantage  of  following  capability  of  solving  sequences  it  errors  t h e W- and D-method. special-  test  found  detecting  to  enjoys  and  providing  the  the  length  full  fault  coverage. This sequences specified passes  a  thesis  introduced  (UTSs). FSM  These  from w h i c h  test  using  are  test  they  are  an  UTS FSM.  identical  to the  specified  This  thesis  extended  eUIOv-method  for  the  testing  the  concept  of  sequences  unique  generated.  possesses  that  can  to  Any'FSM  a  UlOv-method  protocols  unique . t e s t  FSM  to be  the that  skeleton  produce modelled  the by  EFSMs. This  thesis  b a s e d on s t a t i c  developed data  flow  a  data  analysis  5  flow where  testing  procedure  each d e f i n i t i o n  and  Introduction usage  of  whenever  a  variable  possible,  This  thesis  technique  by  testing  the  data  are  implemented  is  flow;  the  its  format  data  flow The  it  that  refined its  detecting  otherwise  be  Ural  and S a r i k a y a .  data  flow  testing,  flow errors  by FSM t e s t i n g  and r e f o r m a t t e d  was  out  in  the  as w e l l  to  IUTs  to as  that  transition  i n the  in  transition  possible. the  normal  form  of  canonical  form  and  underlying  EFSM  and  missed  by  the  for  this  IUTs w i t h  Since the is  tailored  structures,  faulty  it  are  flow  specifications.  each  statement  data  applicable  a protocol  for  generation  the  is  Estelle  checked Each  technique  capable  data  is  with  applicable  their  and,  specification.  EFSM c o n t r o l  of  to  brings  underlying  would  directly  transitions  i n an E s t e l l e  of  sequence  technique of  testing  well.  as v e r i f i e d whenever  explicitly  hybrid  as  test  structure is  IUT  during  eUIOv-method  specification.  thesis  so  hybrid  hybrid  according  e x e r c i s e d as w e l l  Estelle  verified  a  This  hence,  testing,  This  are  EFSM c o n t r o l  its  Estelle  exercised  augmenting the  procedure.  its  they  created  testing  During  are  protocols  technique  erroneous  techniques  hybrid technique  capable  i n an IUT  of  detecting  6  is  thus  EFSMs  that  developed also  by  includes  certain  t h a t would o t h e r w i s e  techniques.  with  types  be m i s s e d  Introduction Test also  sequences  applicable  Estelle  to  to  faults  may o r may n o t be  1.4 THESIS The Chapter  remainder  3,  the a  a  how t h e  it.  In  technique  according  coverage  of  data;  technique  with  applicable Chapter of  to  are  to  their  achieved  would  sequencing  the  to  as t h e EFSMs  of  modelled static  faults  is  to  by  data  flow  technique  is  existing Estelle  test  protocol  Chapter  7  of  and  a  developed  from  discussed Protocol  of  the  generation  this  thesis  testing.  and as  hybrid  techniques  are  discussion  conformance  7  and  specifications  concludes  contributions area  comparison  4  analysis  0 Transport  sequence  a  Chapter  hybrid  a  by  EFSMs.  the  and  followed  In  eUIOv-method  is  Class  techniques  the  procedure  the  follows.  UTS c o n c e p t .  testing  using  as  generation  UlOv-method  evaluation  work i n t h e  organized  flow  5,  6. its  is  sequence  protocols  data  An  thesis  introduction  review  Estelle  example.  future  flow  FSM t e s t  of  chapter to  this  extending  brief  shows  summary  the  fault  UlOv-method as w e l l  testing  provides  in  of  brief  d i s c u s s i o n of the  hybrid  implemented  The  in  the  captured.  2 discusses  chapter  an  not  by  ORGANIZATION  and p r e s e n t s  applied  IUTs  specifications.  be l i m i t e d  for  generated  of  presented with  a  possible  2 THE UIOV-METHOD Test finite  sequence  state  conformance  machines  test  Sidhu  on  Four  paper:  method  the  U-method.  its  undesirable  because  generates. of  the  full is  fault  coverage.  more w i d e l y  Fault in  problems;  test  [Sidh89].  that  a recent  to  while  lengthy other it  than the  p r o d u c e d by t h e  test  the  Wis  W-method  is  sequences  it  h a n d , has n e i t h e r  one  cannot  method,  achieve  the  U-method,  D-method and i t  generates  g e n e r a t e d by t h e  W-method.  U-method was  The U-method t h u s  were  D-method  the  generally  The most, r e c e n t  test  methods  the  general,  be  done  conformance  In  the  can  study  D-method,  sequences than those  coverage  protocols  for  generate  T-method, the  however,  applicable  to  generation  applicability  of  developed  used  looks at  The T - m e t h o d , on t h e  above  shorter  those  test  the  limited  be  approach  notable  that  hampered by  for  this  compared i n and  may  This chapter  [Sidh89]  generation.  techniques  (FSMs)  sequences  m o d e l l e d as FSMs. by  generation  f o u n d t o be  seemed t o be t h e  best  full  of  the  f o u r methods. This achieve  full  with the detection addition  chapter  shows  fault  U-method  a  the  coverage;  [Chan89b]  capability. of  that  it  that  U-method points  procedure  8  out  a  not  always  shortcoming  sometimes hampers i t s  The U-method i s  verification  does  fault  then r e v i s e d w i t h  the  in  the  here  to  form  The UlOv-method  [Chan89b]  produces f u l l method i s it  fault  still  generally  which  coverage  the  each t i m e .  more w i d e l y  produces  corrects  test  problem  The r e s u l t i n g  applicable  shorter  UIOv-Method  than the sequences  and UIOv-  D-method and than  the  W-  method d o e s . All  test  sequences  generated  and UlOv-method p o s s e s s their  full  these  fault  IUT  exceed t h a t of  to  and i t  provided  UTSs i s  property  coverages.  sequences  [Chan89b],  a  be  unique  the  which i s  the  number o f  i n the  a l s o reviewed  the  D-method,  that  This  guarantees  that  by  is  responsible  property test  sequences  detection  of  states  the  in  for  distinguishes  any  FSM s p e c i f i c a t i o n .  in this  W-method  (UTSs)  erroneous  IUT  does  This  not  concept  chapter.  2.1 THE FINITE STATE MACHINE MODEL A  finite  F={S,I,0,T,A} the  set  the  state  based  of  on  denotes  where  inputs,  machine  the  the  FSM  transitions  current can  the  O denotes  the  function  current  action  (FSM)  S denotes  transition  a g a i n on t h e An  state  state  function state  also  be  can set  set  which  and which  and t h e  the  be  of of  represented  states,  I  denotes  outputs,  T  denotes  produces current  produces current  represented  as  by  an  a  new  input, output  state and  A  based  input. a  collection  of  e a c h o f w h i c h p e r f o r m s an o u t p u t o p e r a t i o n and a  9  The state  transition  received  at  the  representation format. state row  In  to  is  the  machine  and E  of  transitions. transition  identified  by  set is  Each and  the  a  of  ends  nodes of  at  its  final  event  that  be c o m p l e t e l y  FSM whose  set  of  it  M is input  Each its  transition  output is  denoted the  starting  state.  is  operation  representing  the  Each  by  states the  set  state  of  Each  arc  is  the  transition  as t h e  set of  has  the  I  specified.  for  is  are  assumed t o  machine,  on t h e  number o f  of  set  The M e a l y m a c h i n e i s  does n o t have e q u i v a l e n t  specified i f each  A Mealy  dependent  inputs.  smallest  completely in  it  thesis  c o n n e c t e d M e a l y m a c h i n e s t h a t may o r  outputs  or reduced, i m p l i e s is,  l a b e l l e d by a  output event produced.  be m i n i m a l and s t r o n g l y  as w e l l  graphical  transition.  triggered  The FSM models c o n s i d e r e d i n t h i s  may n o t  a  This  or  representing  arcs  correctly  state.  format  starts  at  input  by  graphical  set  arc  is  tabular  operation.  of  a  event  e a c h column i s  identified  The a  in  state  input  entry  N is  of  and t h e  an  input  starting  format,  state.  where  an  presented  starting  by  a table  next  G=(N,E),  the  the  labelled  the  be  tabular  denote  that  appropriate  can  the  d e n o t e d by and  provided  UIOv-Method  states  an o u t p u t  the  10  states  is in  M, of  is  states  minimal,  states;  possible.  A  that  Machine  specified for S.  an  each  strongly  The connected  machine  traverses  between  possesses  any two  an  states  input  UIOv-Method  sequence  i n the  machine.  test  sequence  which  2.2 FSM TESTING TECHNIQUES There  are  techniques  four  for  notable  FSMs:  the  T-method,  method and t h e most r e c e n t  the  method, the  generation  W-method,  the  D-  U-method.  2.2.1 The T-Method The  T-method  methods.  This  connected  every  transition  the  test The  existence  of  each  by  is  is  at  two d i s a d v a n t a g e s  transition  are  a  test  least  it  the  state errors;  to  it  the  any  to  four  strongly  sequence,  called  an  FSM  may  test  As  a  until  once.  contain  only  a  that  result,  detects  One  redundant  checks  does n o t v e r i f y  correct.  of  t o u s i n g the T-method.  generated  being  simplest  random i n p u t s  traversed  other  the  applicable  applying  transitions;  may n o t d e t e c t  is  generates  sequences  inputs.  in  It  tour,  There are is  method  FSM.  transition  [Nait81]  for  the  the  only output  the  states  T-method errors.  2.2.2 The W-Method The in  original  [Sidh89]  to  PW-method form  the  [Chow78] W-method,  11  was  slightly  which  is  a  modified checking  The experiment  that  uses  checking experiment each  input  output  is In  part  the  final  a  is  set  pair  that  can  state  a  the  chosen  also  input  states  and  sequences.  methods, It  is  number  specified  states  i n the  at  state  Every  W-method  that  in  I/O  In  the  the  FSM  sequence.  operation  FSM  and  verified.  characterization is  A  expected  state.  FSM a r e  set.  composed o f ,  least  specified  not  the  e a c h I/O  which  FSM,  of  next  each  the  them.  capable  of  as  sequences  the  verifies  characterizing  known  completely  which  correct  experiment,  i n the  identification.  produces  experiment,  of the  is  of  of  four  a  for  distinguish  connected  with  procedure  FSM t o  a  state  a test  checking  using  W-set  a  the  W-set f o r  s t a t e i n each t r a n s i t i o n  every  Of  the  second p a r t  The It  of  identified the  is  specified  and t a k e s  first  the  UIOv-Method  for  one i n p u t  sequence  minimal,  strongly  possesses  produces  the  a  W-set.  longest  test  detecting  all  faults  in  an  FSM  exceeding  that  which  is  in  the  FSM.  2.2.3 The D-Method The uses  a  D-method set  of  [Gone70]  is  a  distinguishing  checking sequences  experiment  which  (DSs)  state  for  identification. An DS where  there  can  be  thought  exists  only  of one  12  as  a  special  sequence  of  case  of  inputs.  a  W-set This  The sequence  produces  different  starting  minimal  and  method,  when  faults equal  in to  a different state.  strongly  an that  sequence  Not  every  connected  FSM  applicable,  is  FSM  number  with  i n the  a  of  also  specified  outputs  for  completely  possesses  capable of  UIOv-Method  states  specified,  an  of  every  DS.  This  detecting  smaller  all  than  or  FSM.  2.2.4 The U-Method The with  U-method  the  [Sabn88]  exception,  input/outputs  that  (UIOs)  is  also  it  to  a  uses  a  identify  checking  experiment  sequence  of  the  states  unique in  each  transition. An UIO not  sequence  exhibited  state  in  UIOS,  a  an  by  FSM  state a  distinguishes  the  An  does  order that  set  possess a  the  U-method  minimal,  to  of  state not  an  state in  UIOS.  is  to  be  UIOSs. a  produced specified test  fault  and  the  I/O  Not  is each  [Sidh89],  strongly  of  of  the  it  by  FSM.  was  in  found  capability  D-method  connected  whose  an  which  specified  detection and  every  formed  state in  W-  behavior  absence  which  sequences  13  the  completely In  by  an FSM.  sequences,  from one o t h e r  of  is  the In  used  input  possesses  generates  a  state  have  set  those  completely  U-method  other  possesses  to  equivalent  The  any  for  signature  concatenating  FSM  (UIOS)  lengths  for FSMs. are  The comparable  to  lengths  generally  are  those  generated shorter  by  the  UIOv-Method  D-method.  than those  Their  p r o d u c e d by t h e  W-  method. Both applicable  the  U-method  to  completely  and  but  being  condition  the  W-method  necessary,  for  the  completely while  U-method  are  strongly  connected  specified  it  is  generally  is  a  and  necessary  sufficient,  but  not  [Sidh89].  Comments On The F o u r Methods  2.2.5  2.2.5.1 In factor  Applicability deciding to  achievable  be  fault  sequence  were  applicable latter  because  of  methods, lengthy  on  which  considered  test  the  W-method  specified,  m i n i m a l FSMs, for  the  to  their  test  among t h e  sequences.  use,  the  applicability,  then  comes  If  method  finally,  all  T-,  a particular  methods better  to  and  produced.  t h e W-method i s  frequently  is  coverage,  three  test  test  is  W-,  D-  FSM,  preferred  fault  the  coverages.  length and  then  over  the  of  the  U-methods  any  the  first  one  T-method  Among t h e  three  t h e most u n d e s i r a b l e b e c a u s e o f Since  t h a n DSs d o , t h e  UIOSs  generally  U-method seems t o  three.  14  of  occur  stand out  its more from  The In  fact,  DSs a r e  sequences  for  algorithm  presented  if  the  all  special  the  resulting  UIOSs  in  W-set  are  UIOSs have  is  to  DSs  of  for  t o as  In  finding  identical  as  UIOSs where  identical.  [Sabn88]  t h e y w o u l d a l s o be r e f e r r e d The  cases  the  signatures  are  u s e d when UIOSs  W-set s h o u l d be u s e d o n l y when t h e lengthy  method.  test  From t h i s  having  the  frequently  The  its  that  it  four  FSM  are  to  UIOSs.  as t h a t are  in  the  absent,  the  absent because  of  can r e s u l t  from u s i n g t h e  W-  the  UIOSs  or  the  constraints,  DSs o r t h e W-set does i n  test  FSMs.  signatures, occur  more  FSMs.  are  those of  implementation solely  directly protocols  a test under  relies  applicable that  can  sequence t o test  upon t h e  (IUT) range  to be  decide  conforms of  faults  detect.  The f o u r transitions  of  The a b i l i t y  specification can  methods  testing  a protocol  verifying  then  Coverage  m o d e l l e d as  to  UIOSs,  DSs a r e  restrictive  than the  conformance  whether  viewpoint,  least  2.2.5.2 Fault  the  sequences t h a t  search  DSs.  DSs.  the  the  input  sequences,  same i n p u t c o n s t r a i n t  signatures  the  minimum  input  The W-set p o s s e s s e s t h e While  UIOv-Method  methods work  and,  that  with  the  the  states  by c h e c k i n g exception in  15  each  for of  the the  transition  existence  of  T-method,  by  are  correct.  The In  this  IUT  sense,  can  be  However,  conformance its  possesses  specification of  whether  and e r r o n e o u s  detected,  according to IUT  missing  a  skeleton  other  W-,  for  protocols.  merely  it  states  or  D- and U-method Their  specified  "what you see FSMs  as  core  pairs,  FSM is  model  Those  edges a  error  edges  state  is  that  its  following  may  are  defined at  two  conformance t o generates  the  levels: its  the  l o n g as  an  to  outputs  As a  result,  test  methods  the  IUT  must is  are  completely referred  of  used  where  a null  assumed t o an  error  for  those  all  test  the  output  enter  an  message. specified  Conformance can t h u s An IUT  to  state-input  an i n c o m p l e t e l y  if,  in  guarantee  be  produce  and weak.  as  16  be  is  generation  strong  not  can  specified.  its  independent  unspecified  assumed t o  specification  same  as  longer  specified  The C o m p l e t e n e s s A s s u m p t i o n a l l o w s FSM t o become c o m p l e t e l y  as  testing.  s t a t e or i t  the  behaves  that  no  during  Assumption  current  IUT  conformance  states  an  cannot.  identical  is  in  t h a t exceeds t h a t which  For  either  an  exist.  limitation  extra  [Sabn88].  p r o t o c o l machine  as  protocols  Completeness  and r e m a i n i n  transitions  states  since  is  I/Os  I/Os  implies  that  suffice  only  and  that  This  and  be a c o n f o r m i n g IUT  what you g e t "  that  specified.  states  requires  FSM  would  n o t p o s s e s s a number o f the  extra  specification.  FSM,  the  but  states  UIOv-Method  has  strong  inputs,  specified  be  in  it its  The specification. specification  if  incompletely edges,  An  IUT  the  IUT  specified  the  IUT  has  has has  whose  in  [Sidh89]  coverage  of  the  method  is  method  only  the  fault  W-,  fact  that  sequence  that  state  on  I/O  the  can  transition following  the  states  of  the  T-method  at of  other  three  methods  Sidhu  detect  all This,  section w i l l  I/O  claims  I/O  however,  show.  17  the  U-  since  the  T-  transition  conformance identical is  verify  the The  are  that  of  is  as not  well the  are  based states former  experiments  sequences each  as test  and  again  checking  errors  fault  for  methods d o .  are  were  The  each  The l a t t e r not  that  each t r a n s i t i o n  strong  does  characterizing  errors.  T-method  operations  T-method.  three  identification.  methods  the  D- and U-method a r e  the  all  different  of  those  specified;  coverages  test  d u r i n g t e s t i n g w h i l e the based  fault  implies  possible.  conformance  coverages  the  is  its  non-core  for  completely  methods.  the  than that of  except  are  out o n l y  its  as  This  test  U-method v e r i f i e s  sequences, f o r  is  FSMs  the  four  than  checks  The  the  of  weak  better  w h i l e the  on  For  c a n be c a r r i e d  to  behavior  behavior.  summarizes t h e  reported  better  I/O  o n l y weak c o n f o r m a n c e t e s t i n g  The f o l l o w i n g  well.  same  unspecified  specification  otherwise,  the  conformance  FSM s p e c i f i c a t i o n .  s t r o n g conformance t e s t i n g IUTs  weak  UIOv-Method  used  for  the  three  as  state  case  as  the  The In four  general,  methods  a test  is  not  s e q u e n c e g e n e r a t e d by any one o f  unique.  more t h a n one t r a n s i t i o n set  of  The  choice  on t h e  UIOSs' o r of  DSs,  which  UIOv-Method  The  tour,  or  it  reason  and i t  may  FSM  has  may have more t h a n  one  have  characterizing  being  more  an  the  than  sequence  to  one use  W-set. depends  tester.  2.3 THE SHORTCOMING OF THE U-METHOD The U-method  appeared to  be t h e  g e n e r a t i o n method f o r FSMs where of  t h e W-method i s and,  detection  capability.  was  found  capability  of  the  UIOSs c h o s e n .  This  compares t h e U-method  in  the  same  time,  U-method  in  section is  U-method w i t h t h e  does  not  it  have  as  possesses this  is  the  fault  that fact  depends  extracted  advantage  on  from  fault  of  the  full  fault  the  case.  not  D-method and i t  strong  sequence  l e n g t h advantage  Unfortunately, [Chan8 9b]  test  applicability  combined w i t h t h e  D-method,  It  at  the  ultimate  detection the  set  of  [Chan89b].  It  shows why  the  coverage  as  the  D-  state  an  IUT  is  method d o e s .  2.3.1 Assumptions In  the  assumed t o to the  following have  initial  a idle  discussion,  reset  input,  state;  r,  each which  no o u t p u t i s  18  takes  in the  IUT  g e n e r a t e d by t h e  back IUT  The UIOv-Method in  response  labelled at  the  as  a  as  to  r.  r/-;  initial  it  correct  but  i n the  state.  and  for  this  exercised  as  feature  a starting arc  well  each arc  would  be  state  and end  s h o u l d be  treated  as  will  verified  during  be assumed t o  be  following discussion. sequences g e n e r a t e d i n t h i s  optimized to better sequences  subsequences  denote  E a c h r/-  simplicity,  Sample t e s t  These  to  would b e g i n a t  idle  transition  testing,  An a r c  illustrate  can  that  be  are  the r o l e  o p t i m i z e d by completely  s e c t i o n are  not  of each subsequence.  eliminating  contained  in  those  test  other  test  subsequences.  2.3.2  The UIOS Problem T e s t i n g of  shown  in  method i s  Figure  the  simple  2. 1  shows  FSM e x t r a c t e d the  not always i d e n t i c a l  19  fault  to that  from  coverage of  [Chan89b] for  the  t h e D-method.  and U-  The UIOv-Method  F i g u r e 2.1: An FSM s p e c i f i c a t i o n . The  test  sequence  generated  Table 2 . 1 , cannot d e t e c t  the f a u l t y  Figure  2 . 2 , o f t h e FSM i n F i g u r e  states  1,  2 and 3 i n t h a t  b/l.a/1 r e s p e c t i v e l y . not d e t e c t  by t h e  test  shown  in  i m p l e m e n t a t i o n , shown  in  2.1.  The UIOSs c h o s e n f o r  s e q u e n c e a r e a / 1 , a / 0 . a / 1 and  The r e s u l t i n g  the erroneous t a i l  U-method,  state  20  test  sequence  f o r t h e b/1 e d g e .  could  The UIOv-Method  Table 2.1:  r/r/r/-  a/1 a/1.a/0.a/1 a/l.b/1.b/l.a/1  r/r/r/r/r/r/-  a/1.a/0.a/1 b/1.b/l.a/1 a/1.a/0.a/1 a/1.b/1.b/1.a/1 a/1.b/1.a/0.a/0.a/1 a/1.b/1.b/1.a/1  U-method t e s t sequence f o r the FSM i n F i g u r e 2.1.  b/1  F i g u r e 2.2:  A f a u l t y IUT o f the FSM i n F i g u r e 2.1.  21  The UIOv-Method However,  the  shown i n  Table  The  chosen  DSs  a/1.a/0,  test  2.2  is  sequence capable  for  states  of 1,  generated  by  detecting  this  2  and  3  the  D-method  faulty  are  IUT.  respectively  a / 0 . a / 1 and a / 0 . a / 0 . r/r/r/-  a/1.a/0 a/1.a/0.a/1 a/1.b/1.a/0.a/0  r/r/r/r/r/r/-  a/1.a/0.a/1 b/1.a/0.a/0 a/1.a/0.a/1.a/0 a/1.b/1.a/0.a/0 a/1.b/1.a/0.a/0.a/1 a/1.b/1.b/1.a/1.a/0  Table 2.2:  D-method t e s t sequence f o r F i g u r e 2.1.  The detect the  reason  the  but i t  is  states  1 and  is  As a r e s u l t ,  the  b/1.a/1  state  set  1,  unique  I/O  UIOSs  IUT  would  behaviors  were state be  for  faulty  3  IUT  the in  the  Figure  22  Both  the  UIOS,  generate  This  non-  the  IUT.  testing  of  either  state  1 or  2 and a / 0 . a / 0 as IUT.  If,  instance, for  these  state UIOSs  FSM,  2.2.  test.  for  not  because  specification  the  chosen,  faulty  could  edge i s  during, testing.  detected  i n the  b/1  could  in  in  sequence  the  IUT  during  c o u l d be  observed  test  unique i n  faulty  detected  a/0.a/1 f o r  faulty  the  state  IUT  is of  the  for  not  state  UIOSs i s  3 in  chosen  uniqueness  the  of  U-method  tail  not unique i n  b/1. a/1,  another  the  erroneous  chosen set  when  why  state  3  however, a/1  for  3,  then  are  also  The The  problem w i t h  the  U-method  b a s e d on t h e  assumption that  when i n  t h e y may n o t b e .  FSM  specification.  states in  fact  i n the  the  faulty  unless  IUT,  UIOSs  may  of  another  state.  uniqueness It  may  to  be  duplicate  of  Figure  state  has  no  generated  for  it.  state  state  C  C;  IUT  c h o s e n b a s e d on  the  of  the  identifying identify  in  the  Hence,  UIOSs  are  problem even  may  be  unique 4 in  IUT. the  In  that  a  U-method  unique  UIOS  also  inherent  that  also  exist  since  [Chan8 9 b ] .  [Chan89b] .  UIOSs.  is  same  states  in  the  IUT.  As  if  it  is  belongs  to  Problem  Note B  the  used  the  c o u l d escape d e t e c t i o n  producing exactly  required  UIOSs  are  UIOSs i n  cannot  unique.  if  state  2.3.3 The S t a t e S i g n a t u r e  not  be  UIOSs  t h e n t h e y must a l s o be u n i q u e i n t h e  capable  signatures.  also  capable  also  that  an e r r o n e o u s  The  are  but they  are not  assumes  specification, a result,  they  thus  UIOSs a r e  are  specification,  IUT  incorrectly  They  they  is  UIOv-Method  A  23  shows  signature  capable  sequence.  It  of  state  signatures  Figure  signature,  the  for  an  are  2.3  is  a  FSM  whose  0/0.0/1.1/0,  is  is  to  not unique  generating  this  I/O  The UIOv-Method  0/1  0/0  F i g u r e 2.3: A test is are  shown i n 0/1  1/0  An FSM w i t h no UIOS f o r s t a t e C.  sequence f o r Table  and 1/1  0/0  2.3.  this  FSM g e n e r a t e d by t h e  The UIOSs c h o s e n f o r  U-method  states  A and B  respectively.  Table 2.3:  r/r/r/-  0/1 1/0. 1/1 0 / 1 . 0/0 .. 0 / 1 . 1/0  r/r/r/r/r/r/-  1/0. 1/1 0/1 . 0/0,. 0 / 1 . 1/0 1/0. 0/0,.0/1 1/0. 1/1,. 0 / 0 . 0 / 1 . 1 / 0 0/1 . 0/0,.0/1 0 / 1 . 1/0. . 1/1  U-method t e s t sequence f o r FSM i n F i g u r e 2.3.  This  test  in  Figure  2.4.  at  state  the  test  B  in  sequence The edge the  sequence  cannot 1/1  faulty in  Table  detect  the  from s t a t e  IUT, 2.3.  24  but  this  faulty  IUT  shown  B incorrectly  ended  is  The r e a s o n  not is  detected  by  because  the  The state  signature  result,  that  verify  state  signature  when t h e  generated unlike  used to  the is,  it  c o u l d have UIOSs,  this  specification  state is  be  As  the  in  state  This  state  also  that  problem,  signatures;  exist  erroneous  1/0  )  B.  the  As a  in  final  the state  testing.  0/0  f c  could  a result,  a l s o escapes d e t e c t i o n during  0/1  C or  inherent  non-uniqueness  not unique.  observed,  been e i t h e r  could  FSM.  C is  UIOv-Method  0/0  1/0  1/1  F i g u r e 2.4:  A f a u l t y implementation o f the FSM i n F i g u r e 2.3.  2.4 THE UIOV-METHOD This a  section  verification  revises  the  procedure  U-method w i t h to  problems.  25  eliminate  the its  addition  of  uniqueness  The  UIOv-Method  2.4.1 Uniqueness Problem A n a l y s i s The u n i q u e n e s s p r o b l e m w i t h t h e UIOSs  is  not  reason i s set  are  the  evident  because the  identical  first  with  things:  the  according to  first  the  the  the  possibility  in a  as w e l l ,  the  more t h a n  identification  sequences  which  responds w i t h the  possesses  the  for  different  but  it  cannot  an UIOS  sequence d i f f e r s  states.  UIOS  as  certainly that  does  belongs  from t h a t  26  of  may  to its  does  state. state  as not  This in  the  U-method,  the  have  different  As a r e s u l t ,  expected output  expected  specification, produce  procedure  two  sequence.  a c h e c k i n g e x p e r i m e n t g e n e r a t e d by t h e state  that  W-set  state  one  same c h a r a c t e r i z i n g I/O  state  or  belongs to another that  checking  implies  DS  W-  During  a  sequence correct  The  DSs and t h e  W-method,  output  possesses  the  i n a g i v e n FSM.  or  its  W-method.  procedure  D-  correct  input  input  states  specification;  may p r o d u c e t h e In  the  an DS o r W-set t h a t  eliminates IUT  state  by  the  sequences f o r  identification  the  the  D-method o r  input  generated  responds  the  for a l l  state  experiment  generate  in  U-method c o n c e r n i n g  a  state  sequence  implies  according  to  not  that  imply  another own UIOS.  state  it its it  whose  The  UIOv-Method  problem  concerning  2.4.2 ~Uv The way the  UIOSs i s  to  eliminate  thus  to ensure  a s p e c i f i e d FSM i s the uniqueness of be  achieved  to  their  the  also the  t h a t the  a set  of  during  uniqueness  testing  [Chan89b].  be r e f e r r e d  identification  procedure i n the  Uv  will  f r o m now  on.  different implied  input in  A and B i n response be  of  observing this  is  In that  if the  B  ~Uv,  the  belong  to  the  for  the  generates  the  show t h a t  B  reduces  the  emphasis other  g e n e r a t e d by d i f f e r e n t  is  A is  states  can  UIOSs  prior  usual  addition  of  whose  state  of  to ~Uv  UIOSs  states,  given  is  subsequence  cannot  is  input  two  states and  1.0.0,  a / 1 . b / 1 . a/0  have  ~Uv  partial  the  then  by  B  merely  a/l.b/0  since  generate'a/1.b/1.a/0.  the  hence,  final not  test  sequence.  generating  identical  i n response to the  27  This  a/1.b/1.a/0  a.b.a  on s t a t e s  states,  is,  be r e f e r r e d  a  instance,  cost of  that  verification  the  other ~Uv,  sequence  absence  for  UlOv-method.  the  UIOS f o r  input  the  the  UIOSs  IUT;  This  states  For  enough t o  This p a r t i a l i t y  those  sufficient.  for  that  with  During  B to  tested  for  of  of  IUT.  U-method w i l l  [Chan89b].  an FSM,  the  ~Uv w h i l e  t o as t h e  sequences;  Uv  as  U-method  required only  s e q u e n c e may be  can  The  to  h e n c e f o r t h be r e f e r r e d ~Uv i s  UIOSs i n  the  procedure w i l l  as  chosen set  UIOSs a l s o h o l d s i n t h e  by v e r i f y i n g  uses  uniqueness  same  UIOSs  outputs inputs  The are it  acceptable; implies  example Table  i n Uv, t h i s  test  sequence  using  t h e UlOv-method  2.4 f o r t h e FSM i n F i g u r e to  that  ~Uv i s a d d e d .  faulty  IUT  b/l.a/1  w o u l d n o t be a l l o w e d  one UIOS i s g e n e r a t e d by more t h a n one s t a t e .  equivalent that  whereas  UIOv-Method  in  shown Note  Figure  instead;  belongs to state  Table  This 2.1  is,  fails  since  state  An  is  produced  in  test  sequence  is  with  the  t h a t a t s u b s e q u e n c e r/-  2.2  that  in  2.1.  as  state  1 generates  exception  b/1.a/0  the  1 displays  r/-  the  UIOS  that  in  state  3.  Table 2.4:  r/r/r/-  a/1 a/1 .a/0 .a/1 a/1 .b/1 .b/1 .a/1  r/r/r/r/-  a/1 a/1 b/1 a/1  .b/1 .a/0 .b/1 .a/0 .a/0 .a/0 .b/1 .a/0  r/r/r/r/r/r/-  a/1 b/1 a/1 a/1 a/1 a/1  .a/0 .a/1 .b/1 .a/1 .a/0 .a/1 .b/1 .b/1 .a/1 .b/1 .a/0 . a / 0 . a / 1 .b/1 .b/1 .a/1  UlOv-method t e s t sequence f o r t h e FSM i n F i g u r e 2.1.  2.4.3 IO(S,K)s To  correct  the  signatures,  [Chan89b]  in  a  place  IO(S,K)s  of  state  inherent  uniqueness  problem  proposed the use o f a s e t o f signature.  Each  member  in  i s a sequence o f I/Os t h a t d i s t i n g u i s h e s 28  IO(S,K)s  the the  set of state,  The S,  t o which  state,  K,  the  IO(S,K)s  i n t h e FSM.  with the exception for  different  sequences  This  that  states  is  from  somewhat  the input  at  least  similar  sequences  may be d i f f e r e n t  one  other  t o t h e W-set  i n the  IO(S,K)s  and t h e number  of  i n e a c h s e t o f I O ( S , K ) s may a l s o v a r y d e p e n d i n g on  s t a t e S. the  S  belongs,  UIOv-Method  The s i z e  of the set of IO(S,K)s  minimum r e q u i r e d  to distinguish  for a state  S from a l l o t h e r  S  is  states  i n t h e FSM. Each set  is  is,  each  the  ~Uv  treated  testing. checking will  is  IO(S,K)s  and  must  as t h o u g h i t  verified Uv  be u n i q u e  is  in  prior  each  I/O  set  of  their  S.  equals  2.5 f o r t h e FSM i n F i g u r e 2 . 3 .  uses  Each that  with  tail  of the state  t o t h e number o f  An example  is  in  during  Tt, portion  operation  IO(S,K)s.  29  to  testing,  a number o f t i m e s its  state  i n t h e same way UIOSs a r e v e r i f i e d  procedures  experiment,  to  an UIOS d u r i n g t e s t i n g ;  During the t r a n s i t i o n  be t e s t e d  sequences Table  set of  shown  S I/O in  The r/r/r/r/-  0/1 1/0. 1/1 0 / 1 . 0/0 0 / 1 . 1/0  r/r/r/r/r/r/r/r/-  1/0 1/0 0/1 0/1. 0/1. 1/0. 1/0. 1/0.  r/r/r/r/r/r/r/r/-  1/0. 1/1 1/0. 0/0 . o/i 0 / 1 . 0 / 0 . 0/1 o/i. 1/0. 1/1 0 / 1 . 0/0 0 / 1 . 1/0 1/0. 1/1. 0/0 1/0. 1/1. 1/0  Table 2.5: For two B  state  C,  sequences are  d u r i n g . ~Uv.  absent. Hence,  In  identify 1/1  state  from  second  B,  is  time.  possesses  the  specified  FSM.  edge  1/1  is  is  0/0 and I O ( C , B )  checked f o r t h e i r state  state  IO(C,A)  0/0 1/0 1/1 0/0 0/0  UlOv-method t e s t sequence f o r the FSM i n F i g u r e 2.3.  IO(C,A)  In  B,  A, 0/0  and I O ( C , B ) C.  Each  checked  is  same s e t  of  together  is but  30  These  states  A and  present,  is  uniquely  1/0  1/0  0/0  c a n be u s e d t o C,  1/0  first IUT  UIOSs and I O ( C , K ) s  IO(C,B).  in  1/0.  absent.  faulty  the  is  is  ends a t  using  the  a result,  d e t e c t e d by  1/0  present  twice  that  absences  although  edge t h a t  Note  As  UIOv-Method  erroneous  f r o m A and  then  0/0  the  in  Figure  2.3  as  that  in  the  state  for  final  The While sets the  can  the  be  former  DSs  are  viewed has  must  number  of  sequences  identical.  As w e l l ,  the  be  cases  special  cases  additional identical in  the  of  UIOSs,  the  all  W-set  the  for  the  IO(S,K)s  constraints for  each  of  that  where  the  states  W-  input  and  the  each  state  must  be  for  every  state  in  t h e W-set must e x i s t  FSM. In  are  as  the  sequences  special  UIOv-Method  the remainder of  referred  to,  it . is  UIOSs and v e r i f i a b l e  this  thesis,  assumed  when UIOSs o r  that  these  are  IO(S,K)s  verifiable  IO(S,K)s.  2.4.4 Comparing The UIOv-Method With The Others The  fault  coverage  better  than  that  states  such  as  are  p r o d u c e d by those  now d e t e c t a b l e .  is  now i d e n t i c a l  is  as  the  illustrated  . The  fault  to those of  by  the  UlOv-method  U-method. in  the  coverage  Erroneous  previous of  the  is tail  sections  UlOv-method  t h e W- and D-method.  The p r o o f  follows. First  checking  of  verification. of  how t h e  all,  the  experiments  different  cases  produced  the ~Uv  W-,  with  Dthe  characterizing  I/O  Secondly,  DSs  UIOSs  and  procedure  the the  for  a  and  UlOv-method  exception sequences and t h e  IO(S,K)s  W-set  state  is  all  they  use  for  state  are  special  respectively.  particular  31  that  are  Recall  implied  in  its  Uv  procedure  belonging  to  UIOS.  this  the  In  other  checking  accomplish method.  the  both  As a r e s u l t ,  of  the  obviously  transition  comparison  generated  fault  test  by  ~Uv  be  than  are  W-method tested  of  to  D-method,  the  a  the  Tt  for  sequences it  UIOSs, DSs. FSM  which If  and  the the  the less  produce UIOvDSs  test  in  own of  D-method the  the  UIOv-  W-,  D-  and  Uv  the  is  likely  that  state the  shorter  than  32  equals  ~Uv  to In  as  the FSMs.  is  likely  identification subsequence  shorter  generally  the  the  requires  different  and  U-  W-set.  in  conditions in are  the  difficult  and D-method were b o t h  are  times  to  UIOv-  than  latter  the  more  However,  restrictive UIOSs  the  according  D-method.  of  method b e c a u s e o f  differ  is  corresponding to  the  portion  in  shorter  number o f  subsequence c o r r e s p o n d i n g to that  may  I/O  since  The  procedure  and  p r o d u c e d , by  generally,  number  than  its  procedures  W-  of  of  UIOSs  p r o d u c e d by t h e  those  lengths  longer  that  the  coverages  sequence test  the  accomplish  sequences  longer  by t h e  fixed  to  for  identification  the  sequences d e r i v e d  the  state  and  they,  each  identical  Uv  however,  that  sequences  UIOv-Method  identical.  The l e n g t h  method;  input are  experiments  what  are  the  states  sense,  UlOv-method a r e  method  when  The  the  UIOv-  forming shorter  applicable  UIOSs,  for  then  the than  to  an  the  D-  The method  should  be  used;  otherwise,  both  UIOv-Method  methods  need  to  be  examined. In widely  terms  of  applicability,  applicable  than  o b v i o u s due t o t h e DSs and W-set. g i v e n FSM i s In  machine  being  necessary  general,  applies  and  necessary  set,  a  i n the  to  which  stems  UlOv-method  completely  or  is  a  or  an  This  is  formation of  the  a set  of  UIOSs  connected  sufficient of  the  is  UIOSs  in  set.  or  Mealy  but  not  W-  and  D-,  that  a  the  FSM  The  same  specified  machines:  so  a completely  specified  FSM  o f DSs o r a W-set c a n be p r o d u c e d ,  a  set  would  be  applicable  for  more  DSs e x i s t s  strongly  incompletely  from w h i c h a s e t  of  condition  W-set  is  W-methods.  the . a p p l i c a t i o n  s u c h a machine p o s s e s s e s  methods a r e is  DSs  and  specified  for  The  condition  from  and  than t h a t  a.minimal  condition  an  or  lower  completely  possesses  skeleton  UlOv-method  The l i k e l i h o o d t h a t a s e t  UlOv-method.  l o n g as  D-  added c o n s t r a i n t s  generally  W-set.  both  the  to  of  UIOSs,  applicable. any  respective Hence,  FSM i n d e p e n d e n t  incompletely  r e q u i r e d c h a r a c t e r i z i n g I/O  the  specified  sequences e x i s t  as  D-,  all  three  of whether long  i n the  W-  as  it the  FSM.  2.5 UNIQUE TEST SEQUENCES All  test  meth.ods a c h i e v e  sequences full  generated  fault  coverage  33  by in  the the  D-,  W-  testing  and  UIOv-  of  FSMs.  The A  property  that  captured  in  proposed  in  in  is  the  common  concept  [Chan89b].  this  thesis  implies  missing  states  and  sequence t h a t not  exist  any  transitions, sequence passes  a  that  in  that  UTSs  uses  are  the  of  is  to an  defined  an  IUT  that  transitions  in  in  FSM  provided  greater  or  equal  to  in  a  those  that  the  to  to  IUT  that  testing  be  of  M.  test  there  does  states  the  An  only  the  test  I/O  IUT  thus  the.  specified any  IUT  FSM.  no  IUT  greater  This  also  possess in  extra  the  a number o f is  IUT  faulty  is  may  which  and  an  if  specified has  and  a  specification.  such  to  of  detecting  states  the  addition  of  FSM  M, i f  and  identical  passes  specification,  UTS. i f  (UTSs)  producing  UTS  is  erroneous  same number  the  capable  in  all  capable . of  number o f is  than  UTS  the  M  identical  which  implies  An  sequences  sequences  coverage  detection  FSM. s k e l e t o n  provided that than  the  test  test'  fault  FSM w i t h  that  test  implies  unique  Full  I/Os.  other  as  a  of  these  u n i q u e t o a s p e c i f i e d FSM,  that . is  possesses This  is  among  UIOv-Method  in  FSM  states  the  FSM  specification. An  UTS  accurately  can  their  formed  describe  specification; is,  be  that  starting  characterizing  I/O  is, and  by  using  each  a  sequence  transition  each  I/O  final  sequences.  34  in  operation  states This  are  of  is  the  that  to FSM  described  described  implies  I/Os  as  by  their  if  there  The exists  a program which  generates  FSM g r a p h s  given  I/O  s e q u e n c e and a g i v e n number o f  given  I/O  s e q u e n c e were an UTS,  only  one  graph  sequence.  that  An FSM  can  It by  the  that  was  found i n  D-method and  accurately  given  FSM;  W-method  that  is  a  method  describes  generally of  the  also  without does  not  each  case  only  the  f o l l o w i n g type  F i g u r e 2.5:  test  the  of  w o u l d be one  and  UTS  UTSs  simple  the  sequences  in  D-method  its FSMs  35  of  specified  and  with  the  Since  the  the  inside  states,  this  the  FSMs.  I/Os  in  Since  A simple FSM w i t h an i n h e r e n t UTS.  on  produced  sequences  operations to  given  depending  g e n e r a t i n g UTSs.  reference  produce  the  produced UTSs.  I/O  a  selected.  transition  of  to  then i f  from  one  UlOv-method were  capable of  any  than  that  b o t h methods  special  it  transition  is  [Chan89b] the  is,  generated  more  according  states,  there  sequence i s  described  method,  be  may have  w h i c h c h a r a c t e r i z i n g I/O  then  UIOv-Method  UIOvthe  T-  each method  exception  The In  the  begin at tour  s i m p l e FSM,  the  initial  possible  there  is  exists  having capable  tail  end a t  state  state  the  2;  DSs, any  FSM  are  the  that  tour  state  to  a/3  both  =  FSMs,  {a},  in  a/3  at  arc  end  1,  2.5  a/3  arc  state  3.  an UTS  the  is to  Figure its  state  each  that  One FSM has  to  because  identical  completely  a  set  FSM,  will  since  only  state  UIOSs r e s p e c t i v e l y .  a  FSM it  be  test  that  W-  possesses  skeleton  an  and a  This  identical  completely  using  incompletely  D-,  of  an  FSM  the  any  whether  pass  since  and  to  possesses  specification  I  a/1.a/2.a/3.a/1 i s  of  UTS  specified  from t h a t  its  transition  an  sequence  arc.  has  not  set  I/O  a/3  other  applicable  specified,  an  s e q u e n c e must  shortest  is  input  specifications  a W-set o r IUT  the  This  an  test  a/1.  apply  specified method  the  tail  generates UTSs  of  1,  FSMs d i f f e r  transition  bounds t h e  that  and  T h e s e two  by t h e  state  the  completely  generating  a/1.a/2.a/3.  it  other  states  of  However,  state,  a/1, a/2, a/3.  two  three  assuming t h a t  UIOv-Method  or  UTS  UIOvset  of  implies to  the  incompletely based  on  the  specification. One generated  question test  test  correctly  that  passes  that  is  sequence  is  represents  that  test  often  correct;  the  must  brought  up  that  is,  specification conform  36  to  is  the  whether whether  so t h a t  any  a the IUT  specification.  The UIOv-Method One  way  to  generate test. one  all  If  FSM,  that  verify  possible  the  test  with  the  i n the  that  a  given  FSMs  uses  that  an UTS,  same number  specification,  test  is  correspond  then there of  that  correct  states  to  is  the  to  given  would e x i s t  only  and t r a n s i t i o n s  as  c a n be g e n e r a t e d .  2.6 FSM TESTING Much c a n be l e a r n t transitions  are  generally  only  software  once.  a  exercising  errors  directly states this I/O  the  test;  where  that  are  or is,  on  different sequence. testing  a  finite  value This,  where  This  is  of  be  however,  a set  of  I/O  in  clear  do  not  that  each s t a t e  elements for  with i t s  because  possible  may  not  be  possible values  37  the  values.  characterized  is  criterion  that  by  are  for  a  not  instance, FSMs  the  solve  characterizing variable well,  different  possible for  merely  detection.  that  As a  least  constitute  may e s c a p e  operations;  possible  set  can  branches,  method  exercised at  checking experiments  p r o b l e m by v e r i f y i n g  takes  T-method,  coverage  becomes  found  i n the  This  it  some e r r o r s  those  an FSM.. . The  sequence.  fault  each branch i s  T-method,  observable  in  the  during t e s t i n g .  partial,  statements,  sufficient  In  p r o d u c e d by t h e b r a n c h c o v e r a g e  testing,  From  These  exercised  achieves  comparable t o t h a t in  f r o m FSM t e s t i n g .  STATE each I/O  in  software  a given  variable  The may be  infinite.  externally different does  observable values  show  improved  As w e l l ,  of  that fault  there  events  a  that  variable.  exercise  may can  over  be  a  sequence  differentiate  Nevertheless,  along  coverage  not  with  that  UIOv-Method  FSM  among testing  verification  produced  of  by  gives  exercise  alone.  2.7 CHAPTER SUMMARY In  summary,  capable to  an  of  detecting  FSM  method, their  checking all  experiments states  specification.  checking  limited  of  the  applicable  without  the  testing  errors advent  on DSs  while  lengthy  UlOv-method,  the  based  applicabilities  were h a n d i c a p p e d by t h e i r advent  and I/O  . Before  experiments  for  test  as of  were  those  UIOv-  hampered on  a  by  W-sets  sequences. " With  of  are  according the  based  checking experiments  disadvantage  FSMs  became  lengthy  the more test  sequence. The  UlOv-method  UlO-method w i t h solution IUT This  is  uniqueness  of  a verification  independent  of  which  solution  provided  the  use  [Chan89c];  that  the  solves  it  solves  permits it  is  UIOS  is  problem procedure.  non-unique  t h e p r o b l e m by a t t a c k i n g  any  minimum  verifiable;  38  length  in  UIOS  hence,  it  its to  the This  in  the  cause. be  used  does  not  The considerably for  add  to  the  UIOSs g i v e n i n Checking  unique  to  passes  such to  additional  generate  specified a  of  the  search  algorithm  [Sabn88].  experiments  the  identical  complexity  UIOv-Method  test the  FSM.  As  possesses specified  transitions  test a  an  result, FSM  FSM;  that  sequences any  not  are  IUT  skeleton  however,  do  that  that  that  it  is  may  have  to  the  belong  specification. In  terms  generally strongly or  of  applicable connected.  incompletely  has  a  set  of  DSs  can  to  Mealy  . Whether  specified  completely  UIOSs,  applicability,  be  machines a  is  specified  checking  Mealy  not  or  from FSM t e s t i n g  transitions  alone  Exercise  transitions  of  possible, In  the  remainder of  to  as  D-method  "UIOSs" possible  refer  will since  to  the  for  is  fault  this  to  DSs  are  thesis,  UlOv-method,  long  a  as  W-set o r  stems  a  it a  set  of  mere e x e r c i s i n g  of  uncover  all  verification,  faults. whenever  the  "UlOv-method"  the  W-method,  This  UIOSs  as  merely  UIOSs  39  completely  coverage.  simplicity.  refer  so  and  applicable.  that  with  are  minimal  is  which  from w h i c h  cannot  along  produce a b e t t e r  be u s e d the  generally  are  machine  for  a c h e c k i n g e x p e r i m e n t w o u l d be  One r e s u l t  that  important,  skeleton  generated,  experiments  well  implies as  whose  DSs. input  will  as . w e l l the This  term is  sequences  The UIOv-Method must be i d e n t i c a l the  term  latter  for  "IO(S,K)s" are  identical  really for  consistently  all  all  will  the  states  also refer  IO(S,K)s the  states  numbered among t h e  40  i n an FSM. t o t h e W-sets  whose and  Similarly,  input whose  states  since  sequences members  i n an FSM.  must  the are be  3 TESTING EXTENDED FINITE STATE MACHINES Techniques  for  simple  protocols  models,  however,  may r e q u i r e the  use  testing  that  can  be  large  sequence  of  in  state  the  space e x p l o s i o n problem.  A  remedy  to  the  u s i n g an e x t e n d e d f i n i t e specification techniques  of  are  more  space  state  to  to  testing  FSMs.  value.  These  explosion  models,  instance,  is  known  problem  (EFSM)  which  introduces  This  protocols.  such  For  protocol  machine  complex  applied  the r e s u l t i n g t e s t  possible  state  by  states.  a  different state  applicable  f o r complex p r o t o c o l s  number  numbers  f o r each  are  modelled  are i m p r a c t i c a l  a very  of  FSMs  is  a as  by  model f o r t h e  When FSM  testing  executabilities  s e q u e n c e s a r e no l o n g e r g u a r a n t e e d .  of This  chapter  d i s c u s s e s how t h e UlOv-method c a n be e x t e n d e d t o t h e  testing  o f p r o t o c o l s m o d e l l e d by EFSMs so t h a t  of  the  final  coverage  test  sequence  i s achieved within  is  guaranteed  executability  and maximum  the l i m i t a t i o n s  of  fault  testing.  3.1 BACKGROUND An  EFSM  variables.  an  These  conditions required  is  the  the  variables  i n the t r a n s i t i o n s  in  transitions  FSM w i t h  underlying  addition  form  of  minor  additional  enabling  t o r e d u c e t h e number o f FSM.  As  a  result,  state  states  different  may o c c u r i n r e s p o n s e t o t h e same c o m b i n a t i o n o f  41  T e s t i n g Extended F i n i t e S t a t e Machines input an  event  EFSM  and s t a r t i n g  may  conditions: boolean  be  triggered  the  input  expression now  consists  operation,  the  state  no  variable minor  alone  state  but  event,  of  A transition  types  the  minor  and  The  value  belonging  it  refers  to  the  values  The  "state"  to  output  of  alter  an EFSM  the  STATE  belonging to of  (TSS)  a  Each  that  "state"  the  system s t a t e  and  the  operations  variables.  total  state  operations:  in  enabling  variables.  to  t o as i t s  of  current state  three  v a r i a b l e s . as w e l l .  be r e f e r r e d  an EFSM. three  transition  of the minor s t a t e  longer . refers  in by  involving  transition  values  state  an EFSM  the will  f r o m now o n .  3.2 THE EFSM TABLE Test  sequences  according to constructed need t o test  thus  for  be  in  an  cluttered better  EFSMs;  are  however, as  well  for  FSMs  in  minor  EFSMs t o when  graph, to  use.  representing  used i n here  as a t o o l  procedure.  42  are  generally  A similar  since  executable,  EFSM d i r e c t e d  suited  from  graphs.  and d i f f i c u l t  p u r p o s e s and i s generation  directed  considered  sequences  included very  their  generated  the  graph can  state  the  can  The t a b u l a r EFSMs for  the  final  variables  graph  be  variables  ensure  these  done  are  become  format  is  for  testing  test  sequence  T e s t i n g Extended F i n i t e S t a t e Machines Columns i n TSSs  of  the  labelled table  the  by  the  entry  final  records  the  output  operations  By  Table  When c TSS,  is  the  the  is  taken  only  absent it  starting  EFSM t a b l e  are  and  can  t*,  or  labelled  by  input  and  the The  semantics instead,  be  Each  EFSM  table  and s y n t a x  of  consideration  syntax during  of  an  alone, the  test  process.  shows one  the  transition.  both, into  in  by t h e  EFSM t r a n s i t i o n s .  identifier,  considering  3.1  N.TSS,  of  transition  within  sequence g e n e r a t i o n  is  a  labelled  Rows  i n f o r m a t i o n on t h e  executability  There  TSSs  transition  contains  EFSM.  are  EFSM t r a n s i t i o n s .  either  thus  EFSM t a b l e  a  minor at  the  indicates  simple state  example  of  an  variable,  c,  in  current  TSS,  C.TSS,  c c a n assume any  43  or  value.  EFSM the at  table.  example. the  next  T e s t i n g Extended F i n i t e S t a t e Machines  ^^"^^^TSS  Si  si  c<2  N.TSS  sl  c=2  s2  s2 c<2  s2 c=2  a/0  si  c : =c + 1  b/-  si  a/3  s2  c:=0 s2  a/b/0  s2  c : =c+1 b/3  si  c:=0 Table 3.1  An EFSM t a b l e .  3.3 EXTENSION OF THE UIOV-METHOD The  UlOv-method  applied to minor  preambles,  extended  EFSM t e s t i n g .  state  applicable  is  variables, to  testing  .however,  executability  An EFSM i s hence, its  must  problems  in  FSM  be  in  the  UlOv-method  portion.  carefully the  final  s i n c e minor s t a t e  variables  they  also  the  be v e r i f i e d  i n FSM t e s t i n g .  44  section  an FSM w i t h  addition, must  this  The  selected test  be  additional  is  directlyUIOSs  to  and  prevent  sequence.  contribute  same way  to  to the  STATE v a r i a b l e s  In TSS, are  T e s t i n g Extended F i n i t e S t a t e Machines 3.3.1 UIOSs S e l e c t i o n In An EFSM For  simplicity,  starting be  TSSs  involve  referred  to  discussion. referred Table  3.1,  as  not  a/0,  of  the  executability all  transitions  a/3,  the  a pure is  E.transitions columns state  are  variables. .  Although advantage UIOSs.  is  that  This any  preambles  method  UIOS.  can  will  simply  be  referring  to  I/Os  are  UIOSs  in  the  EFSM  The  search  the  c h o s e n UIOSs  way  chosen table  is  to  transitions variables  a  in  may  consisting  produce  no  is  special will  considerably  be  increase  45  table.  under of  simply i g n o r e d d u r i n g the not  table  [Sabn88]  the  found  are  "remove"  form  to  if  prevent  to  algorithm  applicable  to  p r a c t i c e , . the, e . t r a n s i t i o n s  As  will  enabling conditions  uncomplicated  executability  implies  whose  subsequent  following  i n the  the  w i t h . TSS In  the  not  the  and t h e i r  directly all,  in  EFSM  variables  example,  in  removed b u t a r e this  with  An  FSM.  now  labelled  physically  enable  UIOSs.  e. t r a n s i t i o n s  f o r . . UIOSs  For  an  state  do  p r o b l e m s may e x i s t  problems  representing  that  in  b/0 and b/3.<  contain.e.transitions part  minor  "e.transitions"  transitions  Executability they  of  "transitions."  those  e.transitions:  transitions  p-uses  as  Those  to  those  the minor  are  not  search.  minimum  UIOSs,  its  guaranteed  within  the  preamble seen the  is  later final  required on, length  to  special of  the  T e s t i n g Extended F i n i t e S t a t e Machines test  sequence  and  may  be  problematic  in  the  testing  of  e.transitions. If  t h e r e s u l t i n g FSM t a b l e  UIOSs  which  applicable involve to  are  to  UIOSs  other  states  preambles  must  UIOSs  to  ~Uv  These  preambles  ensure  executable  ~Uv  testing will  the  EFSM  state.  table  that  executable  by  preamble.  which  If,  the the  be  problem  if  in  the  If  within  in  an  the  there  the must  may have exists  ~Uv  must  preambles  tail  states  their  of  respective  for  the  correct  state.  for  the  purpose  of  an  during  does n o t have an UIOS,  used  however,  The e t  The  not  preambles.  FSM t a b l e  and  UIOS b e l o n g s  special  using  to  find  an  resulting the  UIOS  e.transition  a l s o . w i t h i n . the  then  then  are  The Uv and ~Uv p r o c e d u r e s  itself  UIOS,  can o c c u r . a  is  ~Uv.  only  special  to  variable  transition  within  has  sequences  require  verified  procedure.  attention.  state  may  a r e . formed  non-verifiable  verification,  performed  The e . t r a n s i t i o n s  following minor  is  i n the  input  during  be  use t h e s e  a state  for  This  executability  these  If  whose  e.transitions.  permit  produces only  does  UIOS, not  UIOS  the is  p-use  then  the  require  for  its  more t h a n  46  the a  UIOS  is  special  et,  is s,  not  the  state,  Two  possibilities  ending s t a t e . one  the  by  a  preamble  s as  that  of  enabled  transition,  et.  for  UIOS r e q u i r e  enabling  include  then  This  incoming arc  to  to  is s.  T e s t i n g Extended F i n i t e S t a t e Machines This  implies  states  of  the  the  UIOS  other  cannot  been e n a b l e d .  Another  have  t o be u s e d f o r  state  be u s e d f o r a  state  to  than  be f o r m e d from t h e def-free.paths  s,  f o r . the  . The  UIOS  for  preambles  have  must  at  the  this  all  incoming s  the  its  correct  of  can  is  there  tail  arcs  to used  before  it  is  the  ends  at can  et,  and  each of  the  complete  s.  checked  one  UIOS may  provided  to  would  preamble  to s  not  only  et  EFSM t o  preamble  state  state  the  a partial  be  is  then the  incoming arcs  tail  the  IO(s,k)s  that  the  partial  for  of  UIOS,  case  state  verify  however, the  which  initial  preambles e x i s t  arrives  in  joining  states  preambles.  a set  The o t h e r p o s s i b i l i t y  other  starting  If,  enables  to  b e c a u s e t h e UIOS w o u l d  UIOS o r  s.  s and i t  s.  used  incoming arcs  have  incoming arc  be  the these  Each o f to  used  the  ensure  it  in  Tt  the  procedure. Using ending  s p e c i a l . preambles  states  executability. well, be  a  penalty  problems...  may n o t be m i n i m a l .  tested  is  included in both the exist, may  is  in  an  the  perhaps  be  The In  preamble,  case an  having  to  pay  when  to  resulting addition,  e. t r a n s i t i o n  e.transition which  and  which  then the  and t h e  UIOS.  another  UIOS  executable  47  set  test if  the  requires  preamble  verify  their  UIOSs  have  sequence,  as  transition  to  an  et  to  be  needs  to  enable  Such a p r e a m b l e may n o t has of  to  be  IO(s,k)s  found. for  There state  s  T e s t i n g Extended F i n i t e S t a t e Machines that  would  and  produce  technique  reduce a  the  number  shorter  s u c h as  that  of  special  test  sequence.  used i n  [Shen89]  preambles An  required  optimization  would  f i n d the  best  alternative. For  the  constitute Since  example  UIOSs  they  in  for  are  Table  the  not  3.1,  states  transitions s2  and  e.transitions,  s p e c i a l preambles to enable  si  they  a/-  and  b/-  respectively.  do  not  require  them.  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 • • The  UlOv-method  UIOS.  Similarly,  variables so t h a t the  that  the  verifies in  an  contribute  TSS  is  state  EFSM,  t o the  verified,  not  in  an  values  TSS  FSM  of  with  minor  s h o u l d a l s o be  just  the  its state  verified  STATE v a r i a b l e  in  EFSM.  that  In  the  same way  is  unique to  sequence  that  possible  to  there  it,  that  i s - unique  verify  may n o t e x i s t  that  C.TSS  reason i s may n o t  as  the  state  is  verified  by  c a n a l s o be v e r i f i e d it. TSS  However, as  so t h a t  an I/O  48  may  not  that  be  to  begins  verification.  variables  I/O  instance,  identical  for a particular  the minor s t a t e  UIOS  by t h e  For is  the  sequence t h a t  can perform the  The C . T S S  it  a unit.  a t r a n s i t i o n whose C . T S S  follows. all  to  whole  transition  involve  a  an TSS  t h e N.TSS t o be v e r i f i e d at  a  The  transition appear  in  T e s t i n g Extended F i n i t e S t a t e Machines all  the  allowed  C.TSSs to  transition not of  exist all  EFSM.  may  verifiable  not  be  for  with  variables  would  transition  be  a/3  be  after  a/3  the  final  STATE  to  the  cannot is  verify  at  separately.  s2.  of  that  definition  of  final  variables  Each  STATE can  path  is  used  t r a n s i t i o n whose C . T S S  to  This  for  the  0.  The  STATE v a r i a b l e - Hence, it  can  variable  be  at  exercising  verify  thus  each v a r i a b l e  TSSs,  contributes the  c  reset  c.  An  has  that to  be  i n v o l v e d may  N.TSSs  be  to  or N.TSSs,  definition  to  the  variable  the  to  may be  of  N.TSS  has  verified  v e r i f i e d i n the UlOv-method. I/O  the  p-uses  3.1.  N.TSS  a  does  N.TSS.  Table  c  for  there  the  the  although  The  if  are  separately.  I/O . s e q u e n c e s .  variable  in  N.TSS  contains  to  verify  For C.TSSs,  3.3.2.1 V e r i f i c a t i o n of Verification  c  an  which  a/-  that  variables  a whole  variable  requires  a l s o have t o be v e r i f i e d  an  as  says n o t h i n g about the v a r i a b l e  verified  STATE  result,  contributed  used has  a/- m e r e l y  a/-  a  transition  which  it  As  an C.TSS  that  the  cannot  s2,  using  Unspecified  value.  a transition  transition  C.TSS  the  assume any  the  example  in  a as  be same  minor well  contains  49  the  defined  a predicate  state as  the  verified. way  For the minor s t a t e  lead  achieved  The  they  are  variables,  variable which uses  to  a  that  T e s t i n g Extended F i n i t e S t a t e Machines variable  definition.  variable  can  ,begins at  then  that  Referring where  the  None o f  be  verify  back  to  the C.TSSs  that  has  using  the  is  final  is  identical  that  c was c by  reached  0 to  been  N.TSS  c is  2  after  begin with,  that  two  to  c was  reset  to  to  1.  is  When i t  identical  to  at  that  to  a/3 is  however,  STATE i s  transition  that  transition reset  to  0.  the C.TSS  s2  at  STATE at  I/O  to  that  is  and  increments  c to  not  possible  As  Hence,  a  the  the  2 if  it  that  at  s2,  above at  the  and  sequence  can  for  it  and t h e  to  0,  the  50  it  then  situation  is  sequence c has  correctly.  b/3  the  that  b/0.b/3  incremented c o r r e c t l y . 2,  were had  s2 and t h a t  sequence  the  c  c c a n be v e r i f i e d setting  unless  result,  Similarly  incremented  s2,  s2 and c i s  b/0  b/3 w o u l d v e r i f y  STATE i s  at  Each e x e c u t i o n o f is  initially  as ban  0 correctly.  by  s2;  C.TSS  incremented c to  0 and STATE i s  0 correctly  1 and  state  sequence  and c  increments.  mentioned  b/0.b/0.b/3 v e r i f i e s  that  the  0. b/3  The v a r i a b l e  correctly  at  for  minor  2 and STATE i s  2 correctly.  incremented  is  I/O  s2  not at  and t h e  s2 and c = c + l .  set  to  1 and t r a n s i t i o n  is  both  the  an  to i t ;  indeed reset  incremented  verify  TSS  set  s u b s e q u e n c e b / 0 . b / 0 w o u l d have at  of  s e q u e n c e b / 0 . b / 0 . b / 3 b e g i n n i n g from t h a t  increments c  verified  STATE v a r i a b l e  the  definition  C.TSS.  AND c<2 c a n v e r i f y well,  The  transition  been  When c verifies The  b/0  checks  T e s t i n g Extended F i n i t e S t a t e Machines that  c  begin  is  correctly  2.  Hence,  c must  Verification  Verification transition correct  again  any  ,  starting  verifying  to  t h e . Uv  Two  of  of  that  and of  things  the have  predicate  state  variables.  variables  being  distinguished  distinguishing identifies sequence  variable  or  referring transition by  or a.a  the  that the  to a/0  setting  STATE  the  example  is  also or  the  of in  the  UIOv-  somewhat the  correctness.  The  whenever  predicates  involving  is  similar  value  predicate. 3.1,  the  to  by  means  of . the For  The p r e d i c a t e  51  for transition  an  STATE  predicate  sequence  respectively.  of  instance,  c to  the  The  process  for  1 and i n p u t t i n g  the  another.  c a n be d i s t i n g u i s h e d from t h a t 0 or  is  in  predicate  Table  the  identification  the  is  variable  checked  from one  an  a  checked,  This  characterizes  presence  predicate  be  for  variable in  from o t h e r  procedure, i s  state  procedures  to  minor  a/3  1 to  variable  STATE  and  the  STATE  the  effect  to  C.TSS,  minor  be  has  distinguish it  a  or  STATE  to  possible, same  the  of ~Uv  a predicate:  the  TSS,  involving  Verification  verification effect  the  Verification  identical  different.  I/O  at  C.TSSs  predicate  correct.  method.  of  of  requires  and  also  that  have b e e n  with.  3.3.2.2  is  at  for  transition  a/0  a.a. a would  T e s t i n g Extended F i n i t e S t a t e Machines prompt  the  predicate  response  for  0.0.3  transition  for  a/0 by s e t t i n g  the  IUT.  the  predicate  c to  The r e s p o n s e  or  a/3  respectively.  or a.a  to  of  or  if  the  separately  IUT  w o u l d be  Note  the  that  same way t h a t a l l  imply  Checking  transition The I/O  a/3  of  that si  AND c = l , x.  to  test  1,  then  AND c<4  can  IUT  each  in  the  the  si  x,  AND  then si  way  this  the is  could  The I/O be  case.  the  applied  is  its  constitute  an  implies  predicate to  check  result  in  Checking  value  52  capable  has  been  all an  these  extremely  criterion  the  the  the  of  can  be  setting  predicate  characterizes  verify for  AND  were c<100 i n s t e a d  domain o f  to  si  all  c<4 c a n be c h e c k e d by  sequence which  a/3.  predicates.  c<4  this  not for  sequence  AND c = 3 a r e  the p r e d i c a t e  predicate  values  has t o be c h e c k e d f o r  boundary-interior  3 so t h a t  then  UIOSs f o r  that  one  However,  and t h e  established.  check  sequence i f  Instead,  0,  .To  STATE  have  predicate  I/O  AND c = 2 and  correctly,  possibilities.  used here  si  the  the  if  transition  3.-  c h e c k i n g one d o e s  only  thus  instance,  enables  implemented  4.  employ  item a p r e d i c a t e For  enabling  lengthy  also  sequences used are  correctness.  c=0,  correct.  can  The o t h e r  C.TSS  is  3.-.-  both p r e d i c a t e s  Simply  other  that  2 and t h e n i n p u t t i n g a . a . a  have t o be c h e c k e d s e p a r a t e l y . the  The  c a n be d i s t i n g u i s h e d f r o m  were c o r r e c t .  t o be v e r i f i e d  0.3  can  be  C.TSS  si  response  correctness  c  of  the  of  the  T e s t i n g Extended F i n i t e S t a t e Machines predicate  has  to  be  generation  procedure  particular  values  be  implemented  input.  or  the  sequences  are  sequences  must  predicate  can  minor  Table are TSS,  be be  could  have  sequence Table TSS  si  I/O  verify  starting  I/O  if  this  and c<2,  used  too  sequence  variables  at  of the  until  late  since  to  I/Os  to  time  of  the  test  the  I/O  then.  minor  at  verify  state  discussed from For  states,  variables.  specified," as  then above,  another  si  the  2, thus  is  begins  at  If  less  than  be u n i q u e exists  the  any  involving  the  referring  to  AND c=2 and  si  that  TSS  53  value. starting  for  all  TSSs; not  final  must  at  the  is  a  not  otherwise,  to  p r o d u c e d and i t  I/O one  c variable  2 or  the  that  TSSs s i AND c<2 and s i ; observed,  I/O  these so  instance,  TSSs s i AND c<2,  uniqueness a/0  to  s i AND c=2 were u s e d t o v e r i f y  sequence i s been  TSS  procedure  used  sequence t h a t  u s e d must  3.1,  are  variables.  be a l s o p r o d u c i b l e a t when t h e  test  sequences  be  be  distinguished  state  the  UIOSs  unique,  specified,  then  may  the  certain  values  "completely  3.1,.since  all  setting  the  been d e t e r m i n e d by  used to  are  in  TSSs  same way  variables  same  already  UIOSs f o r  here  verification  process  s e q u e n c e s have  . . In  certain  the  selection  3.3.2.3  because  may r e q u i r e  Leaving  data  considered  the  IUT  The  I/O  TSS.  that  In  is,  at  generated  by  T e s t i n g Extended F i n i t e S t a t e Machines any o t h e r checked, for  TSS. prior  the  exists  This to  STATE  i n the  implies  its  the  use,  the  variables,  to  IUT.  If  uniqueness  same way  its  3.3.3 The  si  AND c<2 from s i  UIOSs  uniqueness  also  d i d not  it  AND s i  exist,  does n o t  have  AND c=2.  eUIOv-Method  The e x t e n d e d U l O v - m e t h o d , method t a k i n g It  s h o u l d be the  AND c=2 and s i  t h e n a/0 w o u l d n o t have t o be c h e c k e d s i n c e t o d i s t i n g u i s h TSS  a/0  ~Uv c h e c k s  ensure  TSSs s i  of  consists  of  executability the  o r eUIOv-method,  and t h e  following  TSS  into  is  the  UIOv-  consideration.  procedures.  Uv = p r e a m b l e ( s i ) @ U I O S ( s i ) ~Uv = p r e a m b l e ( s i ) @ ~ U I O S s ( s i ) where p r e a m b l e ( s i ) from  its  denotes  initial  state  concatenation;  UIOS ( s i )  ~UIOSs(si)  UIOSs t h a t  which for  should not each  STATE  determine choice  the  of  subsequent no  are  such  UIOSs  be in  the  preamble  that  takes  state  si;  "@"  to  is  the  UIOS  belong to  producible the  by  of  STATES  for  UIOS(si)  "UIOSs(si)  preamble(si)  s h o u l d be  used  each  exists, or  a  set  54  si  then of  in  all  either  IO(si,k)s  the  denotes si  and  in  the  FSM  ~Uv  procedures  must  are  and  EFSM  to  states  Uv  Both  preamble ( s i ) and  other  si.  EFSM.  minimum number  belonging  the  are  done  together  EFSM.  ensure  The  that  the  executable.  If  another  set  s h o u l d be  of  used.  T e s t i n g Extended F i n i t e S t a t e Machines Uv and  ~Uv must  b o t h be done b e c a u s e  UIOSs w i t h o u t  their  If  used  UIOSs  are  verifications for  verifying  uncertainty  of  as d i s c u s s e d i n C h a p t e r  2.  TSS  u n i q u e n e s s e s must a l s o be v e r i f i e d The  next  testing,  procedure  or  Tt.  r e f e r r e d t o as Tt  = (1).  variables,  their  i n these procedures.  eUIOv-method  testing  then  of  is  transition  e. t r a n s i t i o n s  will  be  t.preamble(si)©transition(si,sf)@UIOS(sf) t.preamble(si)@UIOS(si)  (1) .  the  the  eTt.  + (2) eTt.=  The  in  of  par.preamble(sj)@def-free  path(sj,si)@  e.transition(si,sf)@UIOS(sf) + (2)  par.preamble(sj)@def-free  path(sj,si)@  UIOS(si) If  t . preamble ( s i )  ~Uv,  then  si  again;  by  (2).  at  si  begins  (2)  the  and ends a t at  the  at  path,  is  sj  state  initial  is  a  to  preamble ( s i )  si.  partial  must a l s o have  is  used  its  state  required  that  Par.preamble(sj) and ends a t leads  a  sj  in  The  path its  tail  concatenated state  55  that  to  that  Def-free that  houses the def total  with  verified  the  be  begins  a path  sj.  and  indicated  transition  That t r a n s i t i o n at e.transition.  Uv  state as  is  state  from  in  tail  denotes a t r a n s i t i o n  sf.  path  appearing the  to  verification  Transition(si,sf)  p-use  which  equal  not r e q u i r e d to v e r i f y  otherwise,  path ( s j , si) starts  is  is  of  preamble, def-free  as i n d i c a t e d  in  T e s t i n g Extended F i n i t e S t a t e Machines (2).  This  in  essence  is  e.transition(si,sf).  If  t h e n embedded w i t h i n  the  those  e. t r a n s i t i o n s .  slightly  longer  involved. well  checking  if  they  last  verification transition  minor  in  state  is  have  that  that  preferable  not  may n o t  procedure  of  it  do  a preamble  as e . t r a n s i t i o n ( s i , s f ) The  why  state  for  e.transitions,  p r e a m b l e s must be d e f s is  During eTt,  starting  t h e UIOSs c o n s i s t o f  This  UIOSs  the  enable to  use  e.transitions  enables  UlOS(sf)  as  exist.  the  eUIOv-method  variables  in  the  TSSs  is  the  in  each  .  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 ) @ def-free  path(sf,sk)@I/Os(msvf)  OR p a r . p r e a m b l e ( s j ) @ d e f - f r e e  path(sj,si)  @e.transition(si,sf)@def-free path(sf,sk)@I/Os(msvf) where  I/Os (msvf)  definition  of  is one  transition(si,sf) path(sf,sk) which  leads  houses  Uv  be  unique,  and  ~Uv  uniqueness.  sequence more  of  I/Os  minor  state  involving  the  or e . t r a n s i t i o n ( s i , s f ) . the be  Predicates  verification carried  variables  in  the  56  If  C.TSSs  for are  it  the in  def-free  s t a r t i n g at  sk  definition  in  I/Os(msvf)  procedure  out  verify  The  to the e . t r a n s i t i o n  predicate  to  to  e.transition(si,sf).  from s f  then  has  or  or  the  transition(si,sf) to  the  identical to  also  check verified  has to its in  T e s t i n g Extended F i n i t e S t a t e Machines this  procedure  previous  return  feature  r/-  used  These uses  the  methodology  discussed  in  the  section.  To  be  using  to  is  to  bring  the  of  ensure  verification  initial  not a v a i l a b l e ,  sequences to  the  I/Os  be  back  should  end  done  state,  if  the  then a sequence o f  machine  they  can  idle  at as  be  to  the  initial  verified  the  prior  initial  follows  for  I/Os  state  has  to  state.  to  state.  a  reset  their Their  si  in  the  EFSM. .  preamble(si)@postamble(si)@UIOS(idle) Parameter  interior  value  variation criterion  c a n be u s e d d u r i n g t h e achieve  methods or  test  the  such most  as  the  commonly  boundary-  used  values  sequence g e n e r a t i o n p r o c e d u r e  more t h o r o u g h t e s t i n g ,  in  such c a s e s ,  may be r e p e a t e d t o accommodate t h e v a r i o u s  test  values  to  sequences selected.  3.3.4 An Example The eUIOv-method an e x a m p l e . variable of  is  The  is  initial  assumed t o  to  bring  verification  is  each  state  is  The r e s e t  state  in  assumed t o be  the  to  to  be  0 at  feature  r/-  EFSM  back  correct.  57  EFSM i n T a b l e  taken  be i n i t i a l i z e d  each implementation.  exist  a p p l i e d t o the  si the is to  3.1  and t h e  as c  beginning assumed t o si.  Its  T e s t i n g Extended F i n i t e S t a t e Machines The UIOSs The UIOSs for  for si  separately  in  for  is  the  s2  is  different  c,values  b/3  are  preambles  c<2 a t  the  Uv.  f o r . s2  again,  since  at  the  their  is  their  they  backwards  the  initial  The  are  considered  and  these predicates  The  those  are  to  transitions  are  in  the  = a/0.a/0.a/3  preamble(b/3)  = a/0.a/0.a/3.b/0.b/0  a/0.a/0.a/3.a/-.r/a/O.r/-  58  si.  The  b/0  constitute 1.  and  following  The  whose  preamble(b/0)  b/-  already  verified  a/3,  the  and  verifying  to  preambles to  e.transition N.TSSs  t r a c k e d and i n c l u d e d i n t h e  subsequence  b/0  from each e . t r a n s i t i o n  = a/0.a/0  test  go  require  preamble(a/3)  following  at  n e e d be  Transitions  predicates  p r o c e d u r e f o r t h e EFSM i n T a b l e Uv:  thus  identical  for  executabilities.  f o u n d by t r a v e r s i n g state.  UIOSs  and  verified  share  s2 s t a r t s  required  i s . a/0 . a/0 . a/3 . . and  they  The  are  si  w i t h a/0  uniqueness  same STATES  preamble  ensure  respectively.  starts  c<2 a t  procedure.  e.transitions to  and a/-  STATE s i  procedure  b/3; Uv  No  b/-  T h e i r u n i q u e n e s s need n o t be  ~Uv  in  preamble  are  The UIOSs f o r v e r i f y i n g  c = 2 at  in  and s2  a/3.  confirmed  only  si  verifying  c=2 a t  inputs.  for  the  enable  preambles.  Uv  and  ~Uv  T e s t i n g Extended F i n i t e S t a t e 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  following verifies  the  special  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  following  msvv  procedures.  indicate  the  test. verify  this  TSSs  is  Since  all  Uv  to  and  to  be  carried the  preambles  ~Uv  again.  Tt:  b/-(sl).b/-  Tt,  the  verified  the  transition  in  example,  out with length  the  of  u s e d have they  the  msvv  eTt  procedure  the  final  already  do n o t  procedure  test  to  be  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  under to  whenever sequence.  been v e r i f i e d  have  and  parenthesis  a/0.a/0.a/3.a/-(s2).a/-.r/e T t & msvv:  eTt  in  procedure,  here  the  information  particular  reduce  the  subsequence c o n s t i t u t e s The,  N.TSS  In  possible  the  test  in  verified  T e s t i n g Extended F i n i t e S t a t e 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(sl  AND c = 0 ) . b / - .  a/0{c=l}.a/0{c=2}.a/3.r/Although the used  to  above, c  UIOSs b/-  verify  the  the  STATES  variables  UIOSs_ f o r  are  can a l s o  c c  S T A T E s . . However, they  should  first  they  indeed  have  that  track  the  tracks  the  The  value  transition effect  of  verification  verified to  the  0 first,  well  in  of  of as  it  is  is in  when  parentheses same t i m e  among  ~Uv  to  ensure  of  the  c  recorded i n braces  to  Values  ' For  instance,  {c=2}  c = 2.  Verification  of  the  this  in  the  in of  verified  the are  example  by  one.  is  predicates  60  purpose,  turn,  implied  1.  the  different  this  the  corresponding also  e T t and msvv p r o c e d u r e above where  then to  the  since  b e i n g i n c r e m e n t e d by  definitions the  are  distinguishing  procedure  are  and s2  case  used f o r  procedure.  enabled  Domains  i n the  as  si  the the  capable  UIOSs a r e  while  the  at  capabilities.  predicates of  are  increment,  is  in  particular  t o be v e r i f i e d  c variable  the  variables.  these  have  that  this  verified  verification  of  in  these  be  STATES  be v e r i f i e d  variables if  for  indicated  variables  among..different  variables  STATEs  verified  the  and a/-  implicitly c was  set  T e s t i n g Extended F i n i t e S t a t e Machines The  final  test  those  test  other  subsequences. The  test two  subsequences  sequence  EFSM  number that  of  in  exist  states  the  are  draw  above  t h e n an IUT  extra  can  generated  skeleton  may be  that  c o n c l u s i o n one  states,  an  sequence  that  again  transitions  in  contained  a test  that  that  if  EFSM has  the  be  restricted  This  specified  again  IUT  that  the only  possesses  EFSM.  to  be  not  The  equal  implies are  in  uses  above t e s t  the  the  eliminating  from  to  specification.  by  completely  passes the  identical must  is  reduced  to  there  may  the  EFSM  in  specification.  3.3.5 Summary Of The eUIOv-Method The that  eUIOv-method  checks  an  IUT  specification. method  and t h e y  verify  procedures  I/O of  state  transition. verified  to  be  Uv  essentially each  EFSM  and  ~Uv  a  procedures  minimum number  each  The  transition and f i n a l msvv  of  UIOSs.  that  Whenever  possible, The  61  in  checks  contribute  state  the in  the  eUIOv-  the  EFSM eTt  the  EFSM  by  as w e l l  as  its  the  to  these  minor  in  in  The T t and  STATE v a l u e s  procedure  experiment  given  states  specified  variables  correct.  checking  transition  the uniqueness of the  current  operations. minor  the  check  observing i t s  for  The  establish  is  the  definitions N.TSS  definitions variables  of  a  are that  T e s t i n g Extended F i n i t e S t a t e Machines contribute their  t o the C.TSS of  correctness  checked  by  state  Their  correctness  variables  an i n t e r i o r  that  executability testing  predicates  requires  selection  of  to  generation the  for  effects  involving  C.TSSs  test  domains  require test  that  are  identical  from one  another.  boundary v a l u e s  some  data.  values are  procedure  final  predicate  may  the  and  predicates  whenever  traditionally the  test  out  sequences  These  separately generated  during to  The  as  well  thus  values  tracking as  pre-  couples  data  two  processes software  face  the  ensure  test  in  may  state  chosen  selected.  eUIOv-method  necessary.  carried  and  computations  The  minor  order  sequence are  of  tracked  in  sequence s e l e c t i o n p r o c e s s w i t h the  process  checked  Their  c h e c k e d u s i n g two  contribute  of  procedure  where  are  also  v a l u e t o e s t a b l i s h t h e domains o f  sequence  test  effects.  and STATE v a r i a b l e s  eUIOv-method  variables  for  are  necessary.  The  test  their  distinguishing  minor  whenever  and  a transition  the  selection are  testing  executability  problems.  3.4 FAULT COVERAGE The eUIOv-method produces  a  p r o d u c e d by  fault the  is  b a s e d on t h e  coverage  UlOv-method.  that This  62  UlOv-method; h e n c e ,  includes implies  that the  which  it is  eUIOv-method  T e s t i n g Extended F i n i t e S t a t e Machines is  also  in  an  capable of d e t e c t i n g a l l EFSM p r o v i d e d  t h a t which i s  i n the  I/Os  in  present  referring  to  limitations testing  of  in  the  of  greater  set  of  IUT  will  term  detail  in  the  this  variables  mathematical guaranteed  in  the  even  though  be  no  of  extra  next  then  assigned  their  they  may  issue  will  during  testing.  This  greater  details  i n the next  chapter.  63  are the  also  the  cannot  discussed predicates  expressions, new  values  correctness display  the  for  statements  mathematical  are  given As  If  extra  However,  and  statements  chapter.  than  implies  detected.  extra  errors  greater  acceptable.  again,  N.TSSs  expressions,  is  This also  not  is  c o n s t i t u t i n g the C.TSSs i n v o l v e if  and STATE  "conformance,"  TSS v a r i a b l e s , The e f f e c t s  errors  STATES  specification.  testing,  the  be d e t e c t e d .  the  its  I/O  be  with  may n o t  correct  or  be  values  discussed  in  4 DATA FLOW TESTING While  simple  protocols  can  be  modelled  more complex ones r e q u i r e  EFSMs t o a c c u r a t e l y  functions  EFSM models a l o n e ,  detail one  and b e h a v i o r s .  the  control  primitives at  flow  for  Instead,  the  usage  the  or  another.  reference  functions  of  described  should  their  a  EFSM also  functions  output p r i m i t i v e s  these in  appropriate  variables  ensure  often  however, takes  For  phase and s t o r e d by t h e  separately  and  to  that  are  are  in  data  in  correctly  the  These  testing  embedded parameters  out  correct  except  similar here,  of  the  to  data  the  instead  msvv  of  definition  Each path i s testing  to  of  a  flow  procedure  to i t s  parameter  usage, or  e x e r c i s e d and v e r i f i e d ensure  the  testing in  a path t r a c k i n g  TSS m i n o r s t a t e v a r i a b l e the  to  and  the  parameters. a data  procedure.  An o v e r v i e w process  can  testing  carried  a  phase.  T h i s c h e c k i n g p r o c e s s c a n be a c c o m p l i s h e d by means o f flow  input  form o f  control  during  a c c o m p a n i e d by t h e  input  are  transition  checked  from  and v a r i a b l e s  transition. be  cannot  place  that  another  flow  the their  instance,  IUT  parameters  FSMs,  describe  o f t e n have a c c o m p a n y i n g p a r a m e t e r s  one c o n t r o l  within  information  phase  variable  be  of  by  definition,  64  a  procedure the  the  whenever usage,  a  eUIOv-method,  definition  each d a t a path  variable  or  gives  to  its  a  tracks usage.  possible under  of  during  test  is  Data Flow T e s t i n g correct.  Any  transitions same way flow  predicate  a l s o has i t s  they  are  testing  analysis.  that  whenever  it  observable  effect  verified  in  technique  It  testing  that  is  also  the  based  on t h e  on  data  elements  The  that  data  learnt  alone  is  not  s h o u l d be v e r i f i e d  the data flow  from  not  are  flow  verified  static  lesson  exercising  i n each t r a n s i t i o n  the  msvv p r o c e d u r e .  based  possible,  in  and c o r r e c t n e s s  is  transition is  appears  FSM  enough, directly  as  well.  4.1 STATIC DATA FLOW ANALYSIS Static  data  optimization in  [Rapp85]  testing  flow  [Hech77]. and  is  strategy  input variable produce  definition and t h e during  must have The subsequent  applied  generally  or of  to  in  compiler  software  accepted  data  flow  as  a  analysis  t h r o u g h a program u n t i l  of,  must  was  static  values.  the that  testing.  variable  now  output  usage  It  originated  testing  structural  [Weis85].  Essentially,  to  analysis  reach  a  variable  been p r e v i o u s l y following  is  while  ultimately  a value  between to,  each  on  used the  a  variable  and  examined  each  defined  identified based  each  variable  to  introduced  to  be  used  defined.  definitions  discussions.  of  are  concept use  is  Associations  assignment  The  it  tracks  In  65  are static  data  flow  enhance analysis  Data Flow T e s t i n g terminology,  the  is  called  of  the v a r i a b l e  the  the  result  to  was  was  the  method  the  of  the  the  def  of  a  variable  variable.  called  a p-use. another  more  coverage;  and  The  use  The u s e variable  by  terms  was more c o m p l e t e  apply of  test  of is  in  functional  flow  protocols.  In  The  based  which  terms  this  on  allow  comparison  [Sari87],  tests  data  sequences  results.  Sarikaya  of  static  relationships  test  comprehensive in  to  testing  flow  of  proposed  generates  first  generating  data  interpretation  method  of  is  conformance  rigorously-defined easier  def,  to  [Rapp85].  the a  or  determining  [Ural88]  analysis  assigning a value  in a predicate  in  a c-use  Ural  of  definition,  variable  called  process  with  method  of  structural  coverage,  Sarikaya s 1  [Ural88].  4.2 DATA FLOW PATHS In  a  parameter  or  transitions of  the  contains  the  the  a  variable  where  the  parameter a usage  transitions on  protocol,  are  flow  refers first  or of  data  to  a  and  parameter  or  EFSM m o d e l l i n g  protocol.  66  the  a  particular  of  data  contains the  last  variable.  c o n n e c t e d by a s e q u e n c e o f  underlying  for  sequence  transition  variable  that  path  a  definition transition These  transitions  control  flow  two  based  structure  of  Data Flow T e s t i n g A  data  within the  the  flow  same d a t a  variable  definition. the  path  to  flow  type is  paths  be  or  already  type  not  of  flow  [Chan89a] the  occurs, based  executable variable the  be is  and  and  it  a  that  path  extend  is  path  is,  embodied  the  usage  of  follows  exercised  testing.  covered  occurs,  parameter;  during to  identifying  control be  the  This EFSM  its  whenever  of  sequence  of  sequence  may  testing.  This  "inter-transitional"  the  transition  two  any  the  transition  as  at  at  The  must  re-definition is  the  with  path  definition  which  which  transitions  structure.  is,  EFSM  transition  these  free  that  one  particular  referred  must  from  the  connecting  the  is  immediately  flow  that  first  on  or  of  which  requires  definition  usage path  and  transition;  examined d u r i n g  path  one  executed.  require  transitions may  length  parameter  This  another  flow  or  EFSM t r a n s i t i o n Data  of  of  "live"  a be  the in  connecting path.  4.3 DATA FLOW TESTING In and  testing  parameters  embedded w i t h i n moment  they  are  the  data  that the  flow  appear EFSM  defined  computational purposes  or  of in  a  protocol,  the  data  the  flow  variables transitions  transitions  are  tracked  until  are  used  as  they  predicates.  67  When  from  either  the for  computations  Data Flow T e s t i n g eventually  lead  to  the  parameter,  the path i s  order  the  that  If  verification  be  exercised;  parameter. involved  is  For  observable  further  computations not  they  may  definition  predicate  not  be  events,  in  may be  at  the  enabled  If  by  verification  different observable  checked  verify  value  to  assigned  is  differ  Usages a r e  thus again v e r i f i e d  have which  on  determining  they  verified  appear. during  the  However,  value if  predicates, involved,  with  can  for  selected  of  values  are  externally again  the  would  a  or  these  inputs.  assigned  to  on  the  event. they  order  usages  may  procedure  in be by  The b o u n d a r y the so the  process. that  the  variables  t h e n t h e y must be c o n s i d e r e d  68  be  different  effects the  in  would  observable  required  the  actions  depending  selection  test  parameter  events  instance,  I/Os  or  manifested  a g a i n be u s e d f o r  preambles  may be e n a b l e d ,  the  data  values  criterion  special  for  only  containing  a c c o r d i n g to the  correctness  test  of  where  parameter  would  or  in  correct.  variable  path  are  externally  values The  selecting appropriate interior  an  flow  these  For  output  constitutes  the  terms  and  then  predicate  of  possible,  p-uses.  an  primitive  be  paths  variable  in the  to  the t r a n s i t i o n  events,  the  to  the  case  p-uses  externally  flow  usage  verifiable  o n l y be e x e r c i s e d and s t o p s a t predicate.  output  verified  the  uses,  which  an  extended to t h a t parameter  possible,  stop  of  again  Data Flow T e s t i n g d u r i n g the test  sequence i s It  not  sequence g e n e r a t i o n p r o c e d u r e t o ensure the  should  all  defs  is  a  the  def  executable. be  are  do n o t e x i s t  noted  there  the  there  may  should  purpose  applies  More  be  used i n  which  of  initializing  specification, case  An example o f  not  this a  the  form  verified  as  uses.  than  one  more  than  one  usage  verified  usage  defs by  may  alone  the  at  exist  since  def  of  of  must the  take  usages  these into  variable.  statement,  where  a  variable,  it.  Each  once;  the  single  def  least  for  the  number o f  additional  specific In  def  def same  a  number  defs.  if of  flow  paths  that  paths paths  Hence,  so  of  a  were would  usages  that  appropriate they  can  be  well.  When t h e produce  of  variable  some u s a g e s may n o t be t e s t e d  limited  to  paths  type  have b e e n m i s s e d s h o u l d be t r a c k e d b a c k t o t h e i r defs  flow  used.  more  and  one  hence,  f o r m e d from  protocol  each u s e .  than  variable;  then  be  a  be  exercised  for  is  may  also  be  in  those d e f s .  i n i t i a l i z e d value While  that  necessarily  for  for  final  the  are  p-uses,  values cases,  corresponding  the  search  consideration Similarly, value  of  they  if  the a  for value  p-use  require  that  to  those  a def  of  that were  is to  the  in  the  defs  the  p-  variable  assigned verify  t h e d e f must be c o n s i d e r e d t o  a  to def  ensure  Data Flow T e s t i n g executability. arise  from  When t h e  the  def  usages  statements  sequence g e n e r a t i o n  are  are  c-uses, not  the  values  that  in  the  test  testing  data  critical  process.  4.4 THE DATA FLOW TESTING PROCEDURE As p r e v i o u s l y m e n t i o n e d , t h e p r o c e d u r e f o r flows  (DFTP)  is  method e x c e p t  all  All  flow  paths  the  defs  the  appropriate  of  similar  brings  in  preambles  msvv p r o c e d u r e  and v a r i a b l e s  begin at  variables  the  the  parameters  that  f o l l o w i n g manner. that  to  that to  transition,  form a t e s t  transition,  that  uses or v e r i f i e s ,  The l a t t e r  transition  is  are  considered. for  appended  the  the  def,  p o s s i b l e , the  i n c l u d e d i n the  testing  indicates  houses  if  ,  eUIOv-  subsequence i n  DF p a t h "  which  the  are  transition(si,sf)  The " d e f - f r e e  transition  in  to the  path  to  the  variable.  path.  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  path(transition)@postamble OR par.preamble(sj)@def-free  path(sj,si)@  e.transition(si,sf)@def-free  DF p a t h  (e.transition)@postamble The  same  variables test  applies in  to  the  flow  paths  transition(si,sf)  subsequences they  form a r e  70  or  that  test  the  usages  e.transition(si,sf).  i n the  following  format.  of The  Data Flow T e s t i n g DFTP = p r e a m b l e ( s k ) @ d e f - f r e e  DF  path(sk,si)  ©transition(si,sf)@postamble(sf) OR par.preamble(sj)@def-free @ d e f - f r e e DF  path(sj,sk)@  path(sk,si)@e.transition(si,sf)  @postamble(sf) The  "def-free  includes which  DF  path"  connects  the  transition  transition(si,sf).  and e . t r a n s i t i o n ( s i , s f ) the  perhaps paths  or  these  Tt  and  due  eTt  to  defs  def-free  the  path  transition  The p a t h s t o  that  procedures.  If  new  problems  paths  in  the  "preambles"  variables  must so  to  the  be v e r i f i e d  that  data  (def-itDFPs)  uses  table  in  to  flow  are  verifying  are  used,  def-free  tail  states  transition(si,sf) ensure  paths  used  end  to  at  the  of  at  verify correct  uses of v a r i a b l e s  situated  DF  or  they  spanned f r o m t h e  and p a t h s u s e d t o v e r i f y  are  where  are p r e f e r a b l y those p r e v i o u s l y used  new  state  and  transition(si,sf)  usage r e q u i r e m e n t s , t h e n t h e  transition, itDFPs)  the  due t o  correct of  to  executability  e. t r a n s i t i o n ( s i , s f ) the  is  the t r a n s i t i o n housing the def of the v a r i a b l e ,  usage i s ,  in  here  (use-  correct  transitions. The  EFSM  with  enabling  aid  in  used  conditions  determining  for  the the  executable  eUIOv-method data  flow  flow  paths  is  augmented  transitions between  to two  71  >  Data Flow T e s t i n g selected data is  flow  preceded  variables, form new thus  be  their  predicate p-uses  the  EFSM t a b l e .  added  in  the  augmented  predicates  indicated  specific  the data  flow  involving  and d e f s  in  Those  reflect  a  If  TSSs  be  during  with  then  entries. would  transitions.  that  minor  state  w o u l d be e x t r a c t e d  New  table  transition  columns along  involve  in  the  appropriate  values  are  required  at  or  with  new  input table the  rows  to may  table  parameters entries  time  of  to  input  testing.  4.5 AN EXAMPLE The DFTP. there as are  following  Referring be d a t a  follows. enclosed  is  back  a  simple  example  to  illustrate  the  to  the  EFSM t a b l e  in  Table  let  flow t r a n s i t i o n s The d a t a in  a  EFSM t r a n s i t i o n  is  transition  1:  flow t r a n s i t i o n s  block  delimited  2:  by  are  IN:  a(a.addr)  C.TSS:  S i AND c<2  N.TSS:  S i AND c : = c + l  IN:  O(a.addr) b(b.addr)  C.TSS:  si  N.TSS:  si  72  EFSM  transitions  d e n o t e d by DF and  BEGIN  i d e n t i f i e d by a number,  OUT: transition  added t o t h e  3.1,  ...  END.  Each  Data Flow T e s t i n g OUT: transition  3:  IN:  a(a.addr)  C.TSS:  s i AND c = 2  N.TSS:  S 2 AND c : = 0  DF:  BEGIN  OUT: transition  4:  IN:  address:=a.addr  END  3(a.addr) a(a.addr)  C.TSS:  s2  N.TSS: s 2 OUT: transition  5:  IN:  b(b.addr)  C.TSS:  S 2 AND c < 2  N.TSS:  S 2 AND c : = c + l  OUT: transition  6:  IN:  O(b.addr) b(b.addr)  C.TSS:  s 2 AND c = 2  N.TSS:  S i AND c : = 0  DF:  The parameter simply  flow in  of  executing  EFSM t e s t i n g  3.addr:=b.addr©address  OUT:  3(3.addr)  each  a. addr  transitions  output parameters the  BEGIN  the  1,  3  and and  transitions  b.addr 5  and  can  In  73  be  an  that  are c o r r e c t  transition  3,  output  verified  observing  enclosed i n parenthesis procedure.  to  END  a.addr  by the  during had t o  Data Flow T e s t i n g be remembered by t h e a d d r e s s v a r i a b l e later  in  output  transition  parameter  information particular thus  6 to  be appended t o  3.addr.  may  have  sequence  a p p l i e d here  to  In  been  of  EFSM  transitions  check  this  i n t e r m s o f an I/O  tracks  the  def  its  usage  in  to  compute  variable  in  the  the  the  EFSM  separately  in  6.  If  this  testing the  DFTP  by  EFSM from i t s  t3,  and c o n c a t e n a t i n g t h e  DFTP:  initial  following test  of  the  this  flow  of  it  requires  of  The  data.  Since  the  by  A data 6 is  This  3. a d d r ,  is  the the  building state  a to  preamble t o  it  to  used  of  the  value  of  the  preamble  the  path  def  would  the  flow  3  then  f l o w p a t h were n o t then  is  3.5.5.6.  transition  variable  observing  data  si  in  DFTP  a  included  be  tested  that  brings  TSS  that  enables  data  flow  path  to  subsequence.  a/0.a/0.a/3.b/0.b/0.b/3 The above t e s t  def  form  occur.  variable  process,  the  form the  to  3 to t r a n s i t i o n  parameter  verified  3.addr.  flow  address  output  be  b.addr  since  to  may be u s e d  sequence, a / 3 . b / 0 . b / 0 . b / 3 .  transition  can  variable,  of  it  testing,  ignored  path which connects t r a n s i t i o n or,  so t h a t  of its  c a n be  the  subsequence t e s t s  variable  usage.  In  seen t h a t  used c o r r e c t l y  to  address; addition,  the  input  it  also  from t h i s  parameters  the  correctness of  tests  correctness  test  subsequence,  a.addr  and b . a d d r  form t h e o u t p u t p a r a m e t e r  74  the  the  3.addr.  it are  Data Flow T e s t i n g  4.6 CHAPTER SUMMARY The d a t a f l o w t e s t i n g p r o c e d u r e i s flow is  analysis  different  not  merely  and t h e  from s t a t i c  traced  to  whenever  possible.  but  effect  its  usage i s its  verified  and by  usage,  Similarly,  there  its  are  characterizing IUT.  When  mathematical then  its  sequence,  variable  is  primitive  usage  of  the  effects same  TSS  of  used  is  verify  variable.  are  its  is  well  exercised When  the  c a n be c h e c k e d : can  methods  effects,  its  is  a  c-use  and  or  other  be as  to  i n the next are  verified and  the  of  compared and whenever  75  as  the is  the  it or  in  the  involves variables,  check.  This  follows.  defines  would  of  usage  p-uses  if  its  is  section.  it  parameter  via  existence  parameters  correctness  When  just  as  correctness  verify  c-use  the  among d i f f e r e n t  that  more d i f f i c u l t  a  the  not  to  usages as  verified  variation  observing  details  parameter,  observed to  by  expressions  The e f f e c t s  It  c h a p t e r t o e s t a b l i s h the domain o f  I/O  discussed in greater  testing.  possible.  Its  data  because a def  is  things  parameter  then  correctness  it  whenever  two  and  the  but  correctness.  applying  predicate  from FSM  a usage i s  verified  d i s c u s s e d i n the previous the  learnt  data flow a n a l y s i s  its  also  a p-use,  effect  lessons  b a s e d on s t a t i c  a  be def  When a  an  tracked and t h e  p-use,  and c-use  then  same v a r i a b l e  possible,  output  these  at  the the  effects  Data Flow T e s t i n g are  tracked  to  verify  instance,  if  statement  y:=2,  assignment  statement  to  an  compute  the  and  output  parameter  ensure  that  to  appropriate  the  however,  the  different again  be  until  they  to the  was  y:=4,  y is y  proved p-uses  the  in  another  be  value  to  x.  If,  then  the  effects  externally  non-verifiable  this  corresponding  a p-use,  x,  used  checked  variable  different  f o r the v a r i a b l e  the  y were  value  used i n  are  enables  transition,  its  correct  For  assignment  variable  and  their  they  to  x<>2  if  itself  p-use. the  i n v o l v i n g the  and  until  the  enables  tracked  predicate  tracked  initial  then  a s s i g n e d the  of  of  predicate  parameter  variable  are  x=2  the  w o u l d be  p-uses  effect  predicate  output  y  the  would  observable  by  looping  or  back  i n which case,  the  p-use o f x w o u l d o n l y be e x e r c i s e d . The  DFTP  subsequences  employs as  eUIOv-method. verified data  in  flow  located at usages t h a t in  their  s i t u a t e d at  that The  the  the  same  used  in  result  is  EFSM t e s t i n g  testing  and  the  method the  subsequences  the c o r r e c t  a  procedure preamble  were m i s s e d by t h e test  msvv  that  the expected t r a n s i t i o n .  of  generating procedure  def is  that now  ensures  ensure  transitions.  76  in  the  was  not  verified  in  that  it  is  to  the  The same a p p l i e s  eUIOv-method. that  The the  test  preambles  usages  are  Data Flow T e s t i n g  4.7 COMMENTS ON THE DFTP The  DFTP  can  detect  errors  defs  and  provided  verifiable  and no e x t r a d e f o r usage s t a t e m e n t s  Erroneous  that  cannot  be  defs  or  are  the  variables  IUT.  they  in  externally  usages  externally  of  usages  observable  variables  exist or  of or  in  the  parameters  o b s e r v e d and v e r i f i e d  may  escape  detection. The p o s s i b l e e f f e c t s are  as  follows.  As  tl.t2.t3.t4  where  verified  its  if  the  by IUT  a  use  were  indeed i n t l t3  is  unknown t o  if  the  def  w o u l d have  t4.  redefined  a  a  variable  in  According to  the  implemented,  the  If in  the  the tl  def  in  tl  verification  were  in  gone u n n o t i c e d .  fact If  the  def  in  tl  erroneous  when  in  fact  it  may  may  distort  detected.  77  result  test  be  the  of  to  IUT,  be  is  which  usage i n one  in  positive  then  As and  t4 tl and  the  error  result  were  suspected  results  path  However,  the  were  correct.  IUT  def  it.  verification  would be  is  the  the  erroneous, the  then  statements  instead  an  specification,  in  tester,  in  def-free  then  variable  t3  negative,  extra  statements  consider  and u n e x p e c t e d by t h e  verified  expected.  of  correctly  erroneously  as  example,  def in  e x t r a def  and t h e use i n t 4 i n d e e d v e r i f i e s  if  w o u l d have  an  of  of a  may  being result, not  be  Data Flow T e s t i n g If that  the  all  uses  were  possible  constitutes  p-uses,  conditions  then are  good p r a c t i c e .  it  is  generally  considered  For  instance,  since  if  assumed  this  only  x>3 a p p e a r s  in  an e n a b l i n g c o n d i t i o n , t h e n x<3 and x=3, o r a c o m b i n a t i o n o f the  two,  should  would r e q u i r e well  to  also  that  ensure  correct.  be  x be s e t that  However,  IUT x  If  the  erroneously  could  have  to  the this  s p e c i f i c a t i o n d i d not and x=3.  present;  otherwise,  3 and a v a l u e  enabling would  not  any  to  p-uses  are  specify  value,  If  verifiable.  all  def  then the value  as  as  known  chosen to  be  erroneous  usage  appropriate ahead  of  the  2,  For  is  then of  if x,  this  method  time  Hence,  is  indeed if  the  them, t h e n i f  best  the  so  x<3  provided the  the  3 as  t o do when x<3  testing  that  and  x= 3  effect  of  alternative  what  of  the  of  test  is  the  type  of  y,  defs,  it  could possibly  78  test  be  y:=2 + x .  of  selecting  c o u l d be  to  erroneously def  mathematical  input  inputs  expression  y were or  involved  u s e d as t e s t  sequence  example  unnoticed.  IUT  then  statements  expressions,  well  possible  x>y  possibilities.  the  important  is  c o n d i t i o n x>y a l t o g e t h e r  w o u l d have d e t e c t e d t h e m i s s i n g p-use the  than  be  specification did specify  assumed  less  condition  s p e c i f y what t h e  missed the  testing  set  data  go w r o n g .  used. If  to  would  x 2*x,  A were the  have  gone  the  most  seems is  just  by  knowing  However,  this  Data Flow T e s t i n g is  impossible  to  be  test  taken data  where  because  into  extreme  values  implementation  select  to  those  of  are  the  apply  test  sequences  that  implementation  the  sun" would  one way  most  This,  testers  79  data  in  users.  a  can  used  however,  and t h e  method,  test  selection; likely  select  used.  approach  sequence are  as  have  are  used  This  to  value  values  select  frequently  t o be t e s t e d .  c o o p e r a t i o n between  ranged  be t o  protocol.  to  the  Instead,  and m i d d l e  that  "under  boundary-interior  approach would  values  extended  consideration.  c o u l d be w i t h t h e  more p r a c t i c a l those  everything  that  requires  all real  also  in  A  a  be is, real  close  5 THE HYBRID TECHNIQUE When hybrid  the  technique  experiment that  eUIOv-method  are  that  is is  modelled  detailing  the  is  augmented  formed which applicable  to  w i t h .EFSMs  functions  of  The h y b r i d t e c h n i q u e  the  essentially  testing  DFTP,  a  with  parameters  protocols  descriptions  and  also directly  variables.  applicable  to  t e s t i n g of p r o t o c o l s t h a t are  implemented a c c o r d i n g t o  Estelle  EFSM p o r t i o n  specifications.  modelling  its  control  method  the  hybrid  the  Estelle  aspect the  in  of  IUT  as  the  technique  is  is  input as  and  its  output  minor  believed  to  by  FSM  observing  starting  and  elements  in  In  testing, its  EFSM t e s t i n g ,  observing i t s  I/O  final an  the  states  FSM the  transition  following  and  correct. are  eUIOv-method  tests  in flow  within  whenever  The  in  the  hybrid Estelle  observations. each  transition  verifying As  exercised  i n p u t and o u t p u t p r i m i t i v e s  80  DFTP  testing  UlOv-method t e s t s  are  the  parameters  for  eUIOv-  data  variables.  adequate  operations  the  verify,  primitive  state  be  and  their  protocol,  the  guide  the  statements  describe  exercise  the  using  Pascal  p r o t o c o l c a n be u s e d t o  s p e c i f i e d p r o t o c o l s b a s e d on t h e In  The  which  to  of  checked  technique.  technique  the  well  flow,  specification  hybrid  possible,  The  a  checking  complex  augmented  their is  is  with  each  a  that  its  result,  all  and  verified.  transition  and v e r i f y i n g  by  that  The H y b r i d Technique its  starting  and  final  result,  the  element  in  Estelle  specification,  data  and  involving  the  in  as  well  parameters  an  Estelle  verified.  to  variables  are  parameters  the  hybrid  the  minor  would  but  c o n t r i b u t i n g to data is  t e s t i n g of p r o t o c o l s t h a t are  for  each  time,  transition  exercising  t r a n s i t i o n whenever This technique sequence  chapter  in and  be  tested can  be  primitive  been  where,  not  Once  all  be  elements  viewed  only  as  well  is  specification each  in  the  their  checked  one  statement  as  well.  implemented a c c o r d i n g t o IUT  an  state  applicable  the  and  as  minor  examined as  thus d i r e c t l y  all  exercised  variables  flow are  verifying  and  output  thus  Estelle  an  possible,  During t e s t i n g , the  can  also tested,  other  each  testing  variables.  have  a  whenever  can  all  verifies  transitions  and  state  are  eUIOv-method  specifications.  flow  input  As  EFSM t r a n s i t i o n s  verifying,  technique  examined,  and  comes t o  houses  data  and v a r i a b l e s  The h y b r i d t e c h n i q u e  Estelle  When i t  correct.  EFSM t r a n s i t i o n s  transition  The  extension  as  are  exercises  it  The  exercising  statements  these  its  eUIov-method.  by  parameters  also  since  transitions,  the  tested  eUIOv-method  variables  an EFSM t r a n s i t i o n .  flow  using  TSS  at  in  a the  possible. provides  can  be  used  from  an  Estelle  to  an  example  generate  of a  specification  81  how  the  hybrid  conformance to  test  an  test, IUT  The H y b r i d Technique generated Protocol  from is  the  specification.  u s e d as t h e  The  sample p r o t o c o l  Class  in  0  Transport  here.  5.1 BACKGROUND This and i t s  section  normal  provides  a  brief  introduction  to  Estelle  form.  5.1.1 E s t e l l e  ISO  Estelle  is  [IS088]  for  [Vuon88b],  is  specification  based  structure  statements  for  specifications have  the  description  communication p r o t o c o l s  Estelle control  a formal  been  on  of  an  a  and  its  to  from  but  limited  to  specifying  a  flow.  set  of  Estelle  oriented  generate  their  by  not  for  and  data  developed  services.  EFSM model  implementation  developed  implementations  of,  protocol  specifying are  technique  the  Pascal protocol  and  compilers  automatic  protocol  Estelle  specifications  [Vuong88a]. Estelle Parent  defines  modules  modules.  may  Modules  interaction communication  points  a system  using a hierarchy  dynamically contain that  channels.  create  abstract can  be  Selected  82  and  message  of  destroy  of  child  interfaces  connected sets  modules.  to  messages  or form or  The H y b r i d Technique interaction channels  primitives  to  facilitate  A protocol The of  actions the  protocol,  The c o m p l e t e is  by  are  variables  module  is  they  composed  of  enabling conditions. include  an  input  expression primitive and,  if  the  are  triggered  and  starting  transition out.  transition, involving  function  exist.  Each  set  of  well  as  other  minor  transition  the  current  minor Each  operations  of  assumed t o  variables  these  conditions  satisfied.  the  a  boolean  or  input  is  optional  The  enabling  transitions  response  and  set  state  The P a s c a l well  of  the the  a set  include  a  as  to  Once  satisfied,  state  a  and  state  be  minor  state  and  in  c i r c u m s t a n c e under which d i f f e r e n t  may  calls  as  generally  minor  parameters.  variable  machine,  not  state.  These  transitions.  variables  in  are  EFSM  behaviors  The e n a b l i n g c o n d i t i o n s may o r may  involving  indicates  of  the  of  parameters.  condition  a  event,  is  these  set  involving  absent,  across  the module, or the p r o t o c o l  STATE  if  corresponding to  d e f i n e d by a s e t of  the  exchanged  s p e c i f i e d u s i n g one o r more m o d u l e s .  module,  "state"  captured  state  each  be  c o m m u n i c a t i o n among m o d u l e s .  c a n be  of  may  an  same  pair  enabling of  of  input  conditions  o p e r a t i o n s may be  output  operations,  operation, specified  in  a  state Pascal,  or  statements  may i n c l u d e p r o c e d u r e  conditional  83  and  loop  a  carried  variables  as  interaction  in  event  primitive and  statements.  The H y b r i d Technique Conditional  statements  permit  a  choice  t o be p e r f o r m e d w i t h i n  a single  5.1.2 Normal Form E s t e l l e  Specifications  An that  Estelle  is  more  simplified  form o f  represented  n o r m a l form s p e c i f i c a t i o n  execution  to  by  are  represent  an  in  a  appropriate number  of  states  statements  are  transition  which  equals  to  This  transition  the  in  also  a  houses  number  those  of  loops  do n o t  and  function  calls  are  is  This  known as  have  sets  i n the  done of  by  the  NFS.  Estelle  states  they  replicating  times  equals  Conditional  or  a  the  variable  the  to  the  and  number  size  loop  are  appearance  of  an  NFS  Pascal  assignment  statements  times  the  loop;  is  Procedure  transition  bodies  assumed t o be n o n -  and do n o t c o n t a i n l o o p s w i t h v a r i a b l e overall  of  the  of  bounds.  within  Procedures  84  its  combined u s i n g in  statements  eliminated  using symbolic execution.  EFSM w i t h  form  graphs.  individual  set.  branches  assumes  The  a  e l i m i n a t e d i n t h e NFS by r e p l i c a t i n g  this  recursive  is  state  to  module  state  the  number  the  directed  single  expanded i n t o NFS.  simplified  s p e c i f i c a t i o n are  form  operations  [Sari86].  S t a t e s t h a t have been g r o u p e d i n t o specification  be  specification  (NFS)  Modules i n t h e E s t e l l e symbolic  may  an E s t e l l e  output  transition.  specification  easily  of  that  bounds. of  a  embodied w i t h i n  giant the  The H y b r i d Technique EFSM  transitions  interaction types  of  Control the  primitive  flows flow  input  in  is  in  interaction  parameters.  an E s t e l l e  output Data  specified  flow  Pascal,  Estelle  is on  variables displays  s p e c i f i c a t i o n more in  the  identified the  minor  and  the  two  explicitly.  STATE v a r i a b l e  involving by  and  the  interaction  the  operations,  state  variables  and  parameters.  specification  form  state An NFS  operations  primitive  original  minor  marked by changes  and  primitives.  An  involving  of  the  henceforth  refers  specification  in  to  the  subsequent  discussions.  5.1.2.1 Example of an NFS [Ural88] Transport here  provides  Protocol.  i n Appendix A.  eliminated;  an example This  All  details  that  NFS  of  is  an  NFS  of  polished  and  redundant assignment have  been  left  the  Class  reproduced  statements  out  are  0  added  are back  in. Each t r a n s i t i o n The is  current  state  i n t h e NFS  or  the  d e n o t e d w i t h FROM.  each  transition  expresses variables  the or  is  input  i d e n t i f i e d w i t h a number.  starting  The  denoted  enabling  is  final with  state state TO.  condition  primitive  85  of or  each  the  The  next  state  PROVIDED  involving  parameters.  transition  minor In  an  of  clause state Estelle  The H y b r i d Technique specification,  the  PROVIDED  clause  c o n d i t i o n s under which d i f f e r e n t the  same  combination of  input  an NFS, t h e PROVIDED c l a u s e responsible of  this  is  "cr.in.max.tpdu.size  event  and s t a r t i n g  t 3 and t 4 .  specification;  transition  t3  and t 4  conditions  in  the  transition  NFS.  interaction  transition  tl4.  This  spontaneous  transitions.  p r e c e d e d by OUT. in  END.  t h e body  Each  minor  parameters  of  Each  Each  to  state  be  An  variables  is  known  as  is  primitive  delimited  inside  by BEGIN  each  and a r e a l s o  a  ...  transition  and i n t e r a c t i o n  are expressed i n Pascal  form  example  operation resides  at  to  interaction  interaction  performed  Estelle  A t r a n s i t i o n may  transition  output  output  twice  input  primitive.  of the t r a n s i t i o n  Operations  involving  type  i n the  was r e p l i c a t e d  an  block  conditions  The b r a n c h i n g  not  is  In  An example  i s p r e c e d e d by t h e keyword WHEN. input  for  transitions.  primitive have  occur  <> n i l " and " c r . i n . m a x . t p d u . s i z e = n i l " from a s i n g l e  transitions  the  state.  a l s o houses b r a n c h i n g  have b e e n e x t r a c t e d that  only  state transitions  f o r branch paths w i t h i n transitions  denotes  primitive  enclosed  in  enclosed  in  t h e b l o c k d e l i m i t e d by BEGIN . . . END. The  interaction  parenthesis  following  parameters,  when  primitive their  referred  p r e c e d e d by t h e p r i m i t i v e  parameters  respective to  inside  primitives.  the  names and e i t h e r  86  are  These  transitions, " i n " or  are  "out" to  The H y b r i d Technique indicate  whether  they  respectively. assigned in  a  the  example  When  constant  in  tl,  output parameter is  assigned  variable,  a  the  an  the  position  where  p o s i t i o n at  example  in  name the  where  parameter  name  for  placements  eliminate  in  identical  variable  t3,  constant  When t h e  value  primitive  the  "normal"  list.  appropriate is  output  value,  appropriate is  b e l o n g t o an i n p u t o r o u t p u t  is  is  OUT  to is  directly  that  of  directly  is  placed  statement. placed  primitive a  An at  the  parameter  minor  placed  state  in  the  c o r r e s p o n d i n g OUT s t a t e m e n t . "qts.estimate"  the  parameter  directly  output  primitive  primitive  replaces  tcind.  redundant assignment  the  These  An last  direct  statements.  5.2 REFINING THE NFS An E s t e l l e  specification  graphical  description  "enriched"  EFSM.  in  this  testing  The NFS i s  section  to  bring  out  separately  of  obtain the  in  a  its  normal  protocol  further  in  terms  r e f i n e d and  canonical  underlying  form p r o v i d e s of  a an  reformatted  transitions  EFSM and. d a t a  and flow  to for  purposes.  5.2.1 C a n o n i c a l T r a n s i t i o n s In  order  expressions  to  ORed  form in  a  canonical PROVIDED  87  transitions  clause  should  in be  an  NFS,  extracted  The H y b r i d Technique and  the  because  transition OR  starting  is  merely  states  particular  replicated a  which  input  is  same t r a n s i t i o n In and The  the  same  For  of  this  that  t h e same i n p u t  is  system when kind  a of  State  sets  trigger  the  into  one s e t .  i n t h e s e t w o u l d be  extracted  for  the  done  each  member  for  all  in  the  set.  variables  f o r the TSS.  example,  PROVIDED  replicated  be  different  in Estelle.  STATE v a r i a b l e s  replicated thus  The r e a s o n  transition  An example  upon r e c e i v i n g  should  same  set feature  starting  transition  combining the  received.  f o r m i n g t h e NFS, e a c h s t a t e  responsible  its  of  trigger  combination i s the state combined d i f f e r e n t  way  accordingly.  as  if  transition  clause  instead  t3 of  i n A p p e n d i x A h a d OR i n AND,  then  follows:  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 t3: 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  t3  would  be  The H y b r i d Technique R e f o r m a t t i n g the NFS  5.2.2  Since  Estelle  structure  of  describe  its  implemented have  its  EFSM  a  uses  protocol  data  and  its  both  EFSM model  The  NFS  is  underlying generation  and  reformatted  are  flow  involve  to  are  protocol  the  against  the  Pascal  generation  should thus  data  flow and  this  that  should  specified  sequence  aid  also  a  consider  statements.  bring  out  the  test  sequence  contribute  brought  out  to  in  the  Problems two  types  problems  of  and  because  the  of  those  conditions  to  involving  that  values  permit  conditions  that  can  not.  always  89  state  an to  Conditions  belong to the  executability. minor  in  contribute  do  parameters  appropriate  testing  enabling  those  input primitive  category time  against  separate  Factors  specification:  executability  hand,  data  to  of  to  NFS.  There  that  here  its  control  specification  test  as  the  statements  testing  checked  well  problems  5.2.2.1 Executability  Estelle  as  model Pascal  specification  process.  executability  of  checked  A  an E s t e l l e  EFSM  to  Estelle  flow  reformatted  set  its  [Chan89a].  for  its  a  structure  technique  EFSM  conformance  to  data  descriptions  and  flow,  according  control  an  be  latter  input  On t h e  variables  at  other could  The H y b r i d Technique contribute are  not  the  directly  previous a  to  executability  of  sequence  of  problem  thus  these  explicit  variables  The  data  major  that  the  latter  selection  of  the  following an  by  The v a l u e s  state  constitute  the  parameters  specification  are  sequences. flow  The  are  made  executability.  new  a  reformatted EFSM and  current  variable  final  found  at  together  set  TSS  the with  90  is  specification that  the  in  TSS in  in  the  the  the  the  clauses  composed  set of  EFSM.  body o f  EFSM.  input  at  variable  indicated  PROVIDED their  appear  STATE  alterations  STATE  the  output  and  variables  d e n o t e d by WHEN c o n s t i t u t e The  The  variables  Estelle  with  the  from t h e i r  keyword  EFSM.  test  an NFS  an  together  and  primitives  these  that  do.  and b r i n g s o u t t h e  Minor  transition  primitive  they  on  specification..  constitute  obtained  TO  between  in  clause  FROM  depend  may r e q u i r e  EFSM and d a t a  features  EFSM.  PROVIDED  may  before if  separates  The  preceded  the  occur  surfaces  in  difference  from an E s t e l l e  Estelle  or they  variables  NFS  flow  constitute the  I/Os  these  values  i n t h e r e f o r m a t t e d NFS t o a i d  5.2.2.2 The Reformatted  NFS i s  Their  parameters  c o n s i d e r e d d u r i n g the  roles  p r o b l e m as  accessible.  input primitive  particular  not  executability  by  a  the Input  in  an  interaction of  inputs  the  in  output  The H y b r i d Technique primitives the  indicated  Estelle An  can  specification  or  correspond to the  clause  that  be  enable  by  statements  data  from  an  Estelle  statements  mentioned above.  In  conditions  in  flow.  either  gathering  enabling  in  an NFS, the  statements  that this  PROVIDED  corresponding  different  within  a  set  and  conditions a  of  of  in  5.2.2.4 The Def other  reformation  is  and  conditions  as w e l l as i n p u t  In  conditions  found  PROVIDED must  that  transition.  transition  types  the  transitions  contributes is  in  conditions  single  first  The  Conditions  conditions  branching  Both  NFS  features  some  those  inside  remaining  f l o w be d u p l i c a t e d .  Enabling  clause  extracted  its  5.2.2.3 The Enabling  the  The  be s e p a r a t e d and some P a s c a l  to data  that  OUT.  s p e c i f i c a t i o n belong to i t s  EFSM  requires  by  is  clause be  affect an  EFSM;  the  IF  clause to  may  minor  interaction  involve primitive  in  the  PROVIDED  second the  contributes  paths  specification,  the or  NFS from  different  expressed  the  an  separated  Estelle  to  in  the  set  CASE  flow state  of  clause  of  data.  variables  parameters.  Statements major that  change  required  statements  91  with  of  defs  the of  NFS  in  variables  its that  The H y b r i d Technique have  p-uses  specification statements future  in must  with  c-uses  t r a n s i t i o n are determines  the  brings  the  have  out  uses  the  that  be g a t h e r e d  defs or  PROVIDED  of  clause  into  variables  p-uses  one or  in block,  responsible  for  data  TSS flow  belong to  in  the  aspect.  EFSM.  Estelle  rest  parameters paths  gathered i n t o another b l o c k . next  the  of  that  have  within  The f i r s t The  the  second  For  those  variables  both b l o c k s ,  their  def  a  block block that  statements  a r e d u p l i c a t e d and p l a c e d i n b o t h 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 t h e g e n e r a l NFS  form o f t h e  reformatted  (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 . o r i . i . p . p . BEGIN {m.s.v. defs} { i . i . p . p . c-uses} { m . s . v . c-uses} { o . i . p . p . defs}  p-uses})  END; where  t*:  rNFS  i.i.p.: i.i.p.p.:  transition  label  input interaction  primitive  input interaction primitive  92  parameter  The H y b r i d Technique estate:  current  m.s.v.:  minor s t a t e  n.state:  next  o.i.p.:  and a the  rNFS  data  WHEN  original  the  of  The  OUT  the  expressed  in  The  data  the  extracted predicate  that  EFSM  transition  of  statements  from  describes  the  starting  with All  clause.  EFSM  in  replicated put  into  determines  each  EFSM  which  output  it  in  the  treated data  WHEN c l a u s e . as  flow,  TSS  variables.  then  PROVIDED c l a u s e  Variables  it  would  If be  otherwise, in the  the  reformatted  into  an rNFS  also  the data  flow  FROM put thus  affects at  the  paths.  i n Appendix A  shown i n A p p e n d i x B.  93  are  and. p l a c e d  The NFS o f t h e C l a s s 0 T r a n s p o r t P r o t o c o l is  w o u l d be  predicate  predicate  replicated  as w e l l t o i n d i c a t e  it  its these  clause  a variable;  of  and  t o use w o u l d a l s o be e x t r a c t e d and p u t i n t h e involves  the  then  primitive if  the  output  If  transition,  be  and  an  two p o s s i b l e c h o i c e s  single would  parameters  flow.  OUT  exists  a  portion  primitives  clause  the  within  EFSM  group  statements  describe  primitives  transition.  primitive  composed o f  s p e c i f i c a t i o n , there  corresponding output  to  rest  are  is  transition.  clause  primitives  output  transition  clause  PROVIDED  state  output i n t e r a c t i o n p r i m i t i v e  flow  transition;  variable  output i n t e r a c t i o n  o.i.p.p.: An  state  Note  that  The H y b r i d Technique  i when  two  transition, where its  "te"  two  transitions  their  labels  labels  data  corresponds paths  rNFS  the  flow  to  a  indicate  rNFS  Estelle that  This  Estelle  reformatted  NFS  specification  for  generating  can  by  as  and  type  "tea" "a"  rNFS  transition  with  EFSM  and  "teb"  "b"  label  and  of  variables  that  their  whenever exists  the  def  discussed  5.3 ESTELLE This  a  transition two  branch  NFS  with  statements  the the  separate.  If  are more  transition,  they  generated same  an  procedure  as  exception As w e l l ,  than  one  and  be  the state  identified duplicated  output  also  that  minor  clauses are  extracted  would  from  primitive  extracted  as  above.  EFSM TESTING section  the  shows  how  eUIOv-method.  representing extracted  easily  a p p e a r i n t h e PROVIDED  necessary. in  be  following  e n a b l i n g c o n d i t i o n s are kept  using  them  identical  within. The  and  an  transition  paths.  single  share  the  from i t s  EFSM rNFS  of  an  Estelle  Table the  5.1  Class  i n A p p e n d i x B.  94'  EFSM may is  0  an  be  EFSM  Transport  tested table  Protocol  The H y b r i d Technique "V.  C.TSS  F.TSS  IDLE  WFCC  tcreq (qr=ok) /cr  IDLE  tcreq (qrook) /tdind cr (opook) /dr  WFTR q.e.=...  cr (op=ok) /tcind  DATA i.b.=0 o.b.=0 q.e.=...  WFCC  WFTR  DATA  dr/ ndreq, tdind  teres (qr>qe) /dr, tdind tdreq/ dr  tdreq /ndreq ndind /tdind nrind /tdind  DATA o.b.oO  DATA i . b . <>0  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.00  dt/-  DATA i.b.=0  -/  tdati Table 5.1  EFSM t a b l e f o r the Class 0 Transport Protocol.  95  The H y b r i d Technique 5.3.1 Spontaneous t r a n s i t i o n s Spontaneous not  require  transitions  inputs  e n a b l e d as  l o n g as  transition  thus  another  transition starting if  a  all it  is  all  TSS  for  spontaneous  of  enabled  A  addition,  its its  a final  do  not  equal  TSS to  transition  has  the  for  output  is  absence  is  for  For  following  are  TSS  another  those  spontaneous t r a n s i t i o n .  do  spontaneous  final  and  of  that  transitions  a  part  values  the  These  part  In or  transitions  satisfied.  or  testing.  whose  TSS  TSSs a r e  when  verifying  Estelle  enabled.  verifies  during of  be  their  transition  observed capable  to  are  of  the  instance,  starting  TSS  and o u t p u t : FROM s i AND x = y OUT o l then  when  variable -/ol was  is  was not  not  In  is  at  si  to  verifies  different  and t h e  C.TSS. from i t s  verifies  either  Hence, equally  the  was  presence  absence  an  N.TSS  of  a  identical  absence  C.TSS.  96  that equal  STATE was  significant  the  Its  it  x variable  then  y.  output i s  summary,  transition  observed,  observed,  equal  transition  output  -/ol  to  not  of  verifies  the an  si  When or  x  spontaneous testing.  spontaneous to  STATE  y.  at  a  during  the  transition spontaneous  N.TSS  that  is  The H y b r i d Technique 5.3.2 T e s t i n g the EFSM i n the COTP As an e x a m p l e , table  in  Table  (COTP).  the  5.1  eUIOv-method  for  the  The EFSM had t o  Assumption  to  Completeness unspecified current  generate  state.  The  a  set  of  used  not t e s t e d of  UIOSs  the  0  in  the  and  the  Protocol  case.  example IUT  EFSM  Completeness  this  transitions  i n here,  the  Transport  UIOSs in  ignored  The a d d i t i o n a l  assumption are had been p a r t  are  Class  applied to  be c o m p l e t e d w i t h t h e  Assumption inputs  is  The  is  remains arising  that in  its  from  the  b u t t h e y w o u l d be i f  they  specification.  chosen  for  the  states  in  the  EFSM  are  as  follows:  This the  UIOS(IDLE)  = tcreq(qts.req  UIOS(WFCC)  = dr/ndreq,tdind  UIOS(WFTR)  = tdreq/dr  UIOS(DATA)  = tdreq/ndreq  is  done by  states  columns  from t h e  denote  variables;  hence,  Since  reset  the  Transport takes  selecting first  TSSs  four  each  a s t a t e back t o the  does of  are  initial  in  following  = dr/ndreq,tdind  state:  unique  table.  by  not  exist  IDLE  are  the  solely  not the  97  that  columns o f  transitions  feature  postamble(WFCC)  sequences  determined  their  Protocol,  I/O  = ok)/cr  the  to  These STATE  e.transitions. the I/O  Class  0  sequences  The H y b r i d Technique postamble(WFTR)  = tdreq/dr  postamble(DATA)  = tdreq/ndreq  The f o l l o w i n g the  EFSM  I/O  from  sequences  its  states.  No  since  UIOSs a r e  The  the  initial  special  are  c h o s e n as p r e a m b l e s  IDLE  state  requirement  themselves  exists  = tcreq(qts.req  preamble(WFTR)  = cr(option  preamble(DATA)  = tcreq(qts.req  ensure  they  test  the  initial  c a n be s h o r t e n e d by v e r i f y i n g actually  for  of  the  the  other  preambles  = ok)/cr  = ok)/tcind~  subsequences  do end a t  each  take  executable.  preamble(WFCC)  following  to  to  = ok)/cr.cc/tccon  verify  the  postambles  IDLE s t a t e .  to  The p r o c e d u r e  only those postambles t h a t  are  used.  tcreq(qts.req=ok)/cr.dr/ndreq,tdind.tcreq(qts.req=ok) /cr.dr/ndreq,tdind  (for  WFCC)  cr(option=ok)/tcind.tdreq/dr.tcreq(qts.req=ok)/cr. dr/ndreq,tdind  (for  WFTR)  tcreq(qts.req=ok)/cr.cc/tccon.tdreq/ndreq. tcreq(qts.req=ok)/cr.dr/ndreq,tdind The  following  procedures Uv:  for  test the  subsequences  constitute  EFSM.  tcreq(qts.req=ok)/cr  dr/ndreq,tdind  tcreq(qts.req=ok)/cr.dr/ndreq,tdind cr(option=ok)/tcind.tdreq/dr  98  (for the  DATA) Uv  and  ~Uv  The H y b r i d Technique tcreq(qts.req=ok)/cr.cc/tccon.tdreq/ndreq ~Uv:  dr/tdreq/tcreq(qts.req=ok)/cr.tcreq/-.dr/ndreq,tdind tcreq(qts.req=ok)/cr.tdreq/-.dr/ndreq,tdind cr(option=ok)/tcind.tcreq/-.tdreq/dr cr(option=ok)/tcind.dr/-.tdreq/dr tcreq(qts.req=ok)/cr.cc/tccon.tcreq/-.tdreq/ndreq tcreq(qts.req=ok)/cr.cc/tccon.dr/-.tdreq/ndreq  Note as  that  input,  testing WFTR  since the  for  testing  tdreq/ndreq,  WFTR and DATA b o t h have an UIOS w i t h ~Uv  procedure  tdreq/for  verifies  tdreq/dr  the  is  UIOS  shortened.  the  in  Uv  for  IDLE  absences  of  verifies  the  DATA.  DATA  tdreq  and  both  WFCC  UIOSs.  absence  of  testing  t d r e q / n d r e q i n Uv v e r i f i e s  the  f o r WFTR.  s u b s e q u e n c e s c a n be e l i m i n a t e d  Duplicated test  o p t i m i z e the The n e x t and  verifies  e. t r a n s i t i o n s entries  are  final  all  in  the  eUIOv-method  transitions.  til  and  tested  in  the  UIOS to  sequence.  procedure  subsequences are Tt:  test  absence of t d r e q / d r ,  for  tl3, this  derived  for  all  With the  Tt;  The  or  following  procedure.  tcreq(qts.req=ok)/cr.dr/ndreq,tdind tcreq(qts.reqook)/tdind.tcreq(qts.req=ok)/cr.  99  it  tests  exception  transitions  procedure. this  the  is  of  table test  The H y b r i d Technique dr/ndreq,tdind cr(option<>ok)/dr.tcreq(qts.req=ok)/cr.dr/ndreq,tdind cr(option=ok)/tcind.tdreq/dr tcreq(qts.req=ok)/cr.dr/ndreq,tdind. tcreq(qts.req=ok)/cr.dr/ndreq,tdind tcreq(qts.req=ok)/cr.cc/tccon.tdreq/ndreq cr(option=ok)/tcind.tcreq(qts.req>qts.estimate)/ dr,tdind.tcreq(qts.req=ok)/cr.dr/ndreq,tdind cr(option=ok)/tcind.tdreq/dr.tcreq(qts.req=ok)/cr. dr/ndreq,tdind cr(option=ok)/tcind.teres(qts.req<=qts.estimate)/ cc.tdreq/ndreq.dr/ndreq,tdind tcreq(qts.req=ok)/cr.cc/tccon.tdreq/ndreq.tcreq(qts.req =ok)/cr.dr/ndreq,tdind tcreq(qts.req=ok)cr.cc/tccon.ndind/tdind.tcreq(qts.req =ok)/cr.dr/ndreq,tdind tcreq(qts.req=ok)cr.cc/tccon.nrind/tdind.tcreq(qts.req =ok)/cr.dr/ndreq,tdind tcreq(qts.req=ok)/cr.cc/tccon.tdatr/-.-/dt.tdreq/ndreq tcreq(qts.req=ok)/cr.cc/tccon.dt/-.-/tdati.tdreq/ndreq Note t h a t  the  transitions their  TSSs  respectively.  last  -/dt are  two  and  subsequences  -/tdati.  enabled  Their  outputs  contain  These  are  following should thus  100  the  spontaneous  included  tdatr/-  because  and  be o b s e r v e d  dt/during  The H y b r i d Technique testing; This  hence,  implies  verify  their  type  of  inputs  dt/for  can -/dt  .-/dt  verified  entry  be  for tdatr/to  and - / t d a t i  appears  dt/-.-/tdati  dt/-.-/tdati.  the  spontaneous  their  to  its  column  out. buffer whose search  in  label  this  can  be  directly  denote  In  this  lack  example,  the  tdatr/-.-/dt; and  The row where  rows  tdatr/-  data,out.buffer=0;  transitions, would  its  Travel  denotes  their  columns  where  data,in.buffer=0.  transitions  be  example,  label,  <> 0.  would  -/tdati.  removes  all  the  the  only  However,  if  they  procedure  to  form  spontaneous t r a n s i t i o n s .  subsequences  e.transition,  and  to  as  are  -/dt  not a p p l i c a b l e here  been s p o n t a n e o u s  test  states  to  case.  The e T t p r o c e d u r e i s  had n o t  final  The  c a n be r e l a b e l l e d  in this  are  as  sequence.  UIOS(DATA)  c a n be changed t o  c a n be r e l a b e l l e d  Concatenating  e.transitions  enabled.  c a n be r e m o v e d .  appears  e.transitions  Their  transitions  are  final  require  transitions  enabling  changed  the  by t h e p r e s e n c e s o f  spontaneous  their  in  do n o t  states.  and when t h e y  EFSM t a b l e  included  and d t / -  final  of  appended t o  are  tdatr/-  automatically This  they  a  stop  t d a t r . i n . t s d u . fragment,  starting  final  follows.  take t i l  down  at  as  the  the  TSS  denoted  101  or  TSS rows  as  and DATA,  Extract  the  -/dt.  According  is  DATA  and  the  one  at  and  identical  DATA  since  find  to  that.  out.buffer o.b.oO  in  The = the  The H y b r i d Technique table. til.  Any  entry  at  this  There  is  only  row  one  t r a n s i t i o n t l O or t d a t r / - . to  enable  formed  the  which  partial  latter. begins  preamble to  to  complete  the  in  Hence,  tdatr/-  test  IDLE  -/dt,  and  example,  preamble with  DATA,  then  tdatr/-  is  preamble.  -/dt  must  be  tdatr/-.  A  takes  concatenated  The  for  namely  must p r e c e d e  a  ends  s u b s e q u e n c e s w o u l d be u s e d t o t e s t eTt:  this  tcreq(qts.req=ok)/cr.cc/tccon  EFSM f r o m i d l e form  an e n a b l i n g c o n d i t i o n  entry  To at  is  the to  following  it  test  -/dt:  (1)tcreq(qts.req=ok)/cr.cc/tccon.tdatr/-.tdreq/ndreq (2)tcreq(qts.req=ok)/cr.cc/tccon.tdatr/-.-/dt. tdreq/ndreq  where s u b s e q u e n c e it  ends  state then  at  of  the  the  tests  is  hence,  The final that  subsequence  is last  TSSs  at  involve  DATA AND  verifies  state,  to that  already  be  minor  i.b.oO.  (1)  is  preamble t o  verifying  tested.  -/dt,  Since  the  -/dt not  and is  the  ensure  starting  Subsequence  verifies really  a  possible.  its  (2) final  spontaneous Subsequence  f o r t e s t i n g the t r a n s i t i o n  tdatr/-,  included.  procedure each  thus  to  e.transition,  identical it  correct  tdreq/ndreq.  transition, (2)  first  e. t r a n s i t i o n  the  state with  (1)  is  msvv  transition. state  to  The o n l y  variables  However,  since  102  verify  are  the two  starting starting  DATA AND o . b . o O  they  enable  and TSSs and  spontaneous  The H y b r i d Technique transitions, been  verified  these be  the in  the  transitions  verified  row  effects  here  labels  of  Tt  these  predicates  procedure  when  have  the  outputs  are  observed.  The f i n a l  TSSs t h a t  are  identified  by  transitions  include  of  minor  s h o u l d be n o t e d t h a t  while  an u s e must be  of  every  def  used.  These d e f s  column l a b e l s in.buffer  are  are  occur!  This  and o . b .  are  either  select domains verified  row  there  enabled  observing  interior  the  implies  since  out.buffer  are  can e a s i l y  with  This  However,  by  not  labels.  <> 0,  that  correct.  value very when  0,  large they  include  and are  can  that  the  do  very  not  the  at  (o.b.oO)  103  be the  defs  never  used.  transitions in.buffer be  do  not i.b.  predicates  the  boundary-  can  be  to  verify  other  or  verified  using  these  require  and  and  column  predicates  =  tl2  the  transitions  The  the  the  implicitly  values  0.  qts.estimate  t d a t r . i n . t s d u . fragment  and  criterion  small  In  necessarily  are  DATA  whose  by c o m p a r i n g  t h e domains o f  but  not  at  to  preceded  instance,  defs  spontaneous  they  criterion,  will  til,  spontaneous  is  two  Since  not  two  defs  verifies  tlO,  For  two  state  those  also  0 or  these  these  t7,  = 0 do n o t a p p e a r a t  exists  when  t5,  be i d e n t i f i e d  = 0 and o u t . b u f f e r  labels.  which  variable,  t3,  from  have  variables.  tl3.  the  transitions  state  these  by a d e f  are  defs  those  example, It  already  defs  used  to the  to  be  out.buffer  =  in. buffer  =  The H y b r i d Technique dt. i n . user. data transition  is  c a n be  found  transition  t8  the  hence,  t5  again turns is  would  all  of  lead  a def  the def  exit  to  the  IDLE.  but t r a n s i t i o n s or  to  DATA  to  qts. estimate.  transition  to  the  from WFTR, <> 0 and  that  generated  qts.estimate; lead  it.  A t8.  of  hence, p-use  t7. i.b.  of  p-use  of  search  are  c a n be  from the  takes  the  and  tl  leads  which  of  does a  t8,  qts.estimate  a  to  be v e r i f i e d  104  them,  to  WFCC,  other  the  only  IDLE  def  of loop  def  of  is  no  to  any  p-use  of  could  The r e m a i n i n g d e f s of  which  not  or  contains  be  tl6  there  the  both  path  also  new  in  For  a  new  or  <> 0.  t8,  a  t3.  labels  EFSM b a c k t o  that  to  in  transitions  tl5  enables  t5  can  only  concluded that  bring  def  IDLE  also  WFTR  in  tl4,  from  it  would  exists t8  be >  f o u r t h " row,  there  introducing  which  the def  column  the  WFTR,  to  the  transition  latter path  state  qts.req  then  From t 5 ,  t3  it  if  the  qts.estimate.  for  of  qts. estimate,  DATA  Hence,  d e f i n e d i n the  Hence,  in t5.  the  Hence,  path  = ...  state  via  a  =  it.  parameter  from WFCC e i t h e r  is  enables  can be u s e d t o v e r i f y  The o t h e r  IDLE  def-free  qts.estimate  however,  input  From I D L E ,  again,  qts. estimate. back  its  up t r a n s i t i o n  free  for  example,  t8  enables  used to v e r i f y that  the  second q t s . e s t i m a t e  transition  that  in  searched  requires  qts.estimate, For  For  t3 o r c r ( o p t i o n = o k ) / t c i n d  column l a b e l s None  (i.b.oO).  never  transition are  o.b.  starting  The H y b r i d Technique TSSs  that  make  transitions. implicit  Hence,  when t h o s e  observed. test  use.  Hence,  of  them  their  belong  verifications  to are  spontaneous t r a n s i t i o n s  for  spontaneous automatic  are  t h e msvv p r o c e d u r e , t h e r e  and  enabled  and  is  one  only  subsequence.  msvv:  cr(option=ok)/tcind.teres(qts.req>qts.estimate)/ dr,tdind The  minor  predicate visible  state  (qts. req  by  its  def'd".  some  initial  in  starting  TSS  However,  n e c e s s a r y as m i n o r s t a t e to  qts.estimate  > q t s . estimate)  changing  qts.estimate  variable  at  are  can  from  this  variables  values  t8  used be  WFTR  is  the  made  more  to  "WFTR,  generally  typically  the  in  not  initialized  beginning  of  the  specification. The f i n a l Class test has  0 T r a n s p o r t P r o t o c o l has subsequences  76 t e s t  5.4 ESTELLE This IUT  unoptimized t e s t  are  sequence f o r t h e 98 t e s t  removed,  the  inputs.  EFSM o f If  optimized test  the  duplicate sequence  inputs.  DATA FLOW TESTING s e c t i o n d i s c u s s e s how t h e  generated  according to  its  tested.  105  data  Estelle  flow  portion of  an  s p e c i f i c a t i o n can  be  The H y b r i d Technique In  testing  Estelle appear the  the  data  specification, i n the data  moment t h e y  flow  the  are  defined u n t i l  the d e f s ,  the  effects  of  are  a p p l i e d whenever  of  minor  is,  variables their  state  The  whose  EFSM  enabling  aid  in  its that  tracked  from  used e i t h e r  for  Verification  for  correctness  as m e n t i o n e d i n  state  extracted  used  table  is  the  i n p u t parameters  aid  do i n t h e  verify are  in  those  different  the  that  process  eUIOv-method; minor  state  from t h o s e  of  different. in  the  for  eUIOv-method  the  executable If  then  is  augmented  data  flow  flow  paths  between  flow  portion  the  TSSs  their in  be added i n  entries.  may  transitions  data  transitions  p r e c e d e d w i t h a PROVIDED c l a u s e  form new  may t h u s  again  also  transitions.  variables,  to  spontaneous  same way t h e y  conditions  rNFS t r a n s i t i o n  new  possible  assigned values  table  rNFS  in  absences  determining  selected  rows  are  predicates.  variables  t o be i n d e e d  with  or  as  they  on  parameters  o f t h e u s e s as w e l l as t h e  i n the  their  C.TSSs  minor  or  conditions  verification  that  and  based  chapter.  Enabling involve  protocol  f l o w p o r t i o n o f t h e rNFS a r e  purposes  previous  a  variables  computational  p-uses  of  Those  p-uses  the the  PROVIDED  clauses  w o u l d be i n d i c a t e d i n t h e  106  in  would  New  augmented t a b l e  two a  involving  and d e f s  EFSM t a b l e .  to  columns  along  that  be  with  involve  appropriate  table  The H y b r i d Technique entries  to  time  input during  of  indicate  One  of  due  to  data  whereas,  if  values  advantages  from  here:  specific  the  data  of  the  redundant t e s t  r e q u i r e d at  flow  separating transitions  d u r i n g EFSM t e s t i n g ,  flow  are  the  testing.  the  transitions surfaces  that  paths NFS  are  were  the in  replicated  not  unnecessarily  used,  EFSM t e s t i n g  EFSM  an  rNFS  transitions  tested  twice;  would  contain  flow  testing  subsequences.  5.4.1 Data Flow T e s t i n g f o r the COTP This  section  provides  an  u s i n g t h e rNFS o f t h e C l a s s The  EFSM t a b l e  the  necessary  with shown  in  data  Table  flow  However,  The  since  no rows step  that  (def-itDFPs) . at  a time.  def-itDFP. there;  in  in flow  each  of  hence,  the  data  Protocol.  5.1  is  first  portions  to  form  in  the  rNFS,  transition  PROVIDED  clauses  augmented the  there  t3,  involve  t5  table  are  two  and  t6.  only  input  o r columns n e e d e d t o be added i n . is  to  identify  and  extract  inter-transitional  transition  To b e g i n w i t h , All  Table  that  span  Each  of  0 Transport  Note  their  next  transitions  data  5.2.  paths  parameters,  shown  example  in  rNFS  transition  definitions  exercising  the  the  in  tl  that  transition  107  data is  does  flow  the paths  examined  one  not  any  transition alone  all  have are  used  exercises  as  The H y b r i d Technique well  as  usages  verifies are  for  for  transitions  tlO  and t l 2 ,  all  the  defining t2,  recall  t4,  defs output tl4,  that  in  the  parameters.  tl5  and  in  w o u l d a l s o be e x e c u t e d .  tlO  and  included these  two  in  tl2 the  are Tt  procedure  transitions  tl6.  In  do  not  again.  108  have  goes  transitions tl3  execution indicate  til  and  during  same  the  and  As a r e s u l t ,  "automatic"  since  The  spontaneous t r a n s i t i o n s  may be appended t o them b e c a u s e t h e i r and t l 3  transition  the  have  til  def-itDFPs  already  EFSM t e s t i n g . to  be  been Hence,  considered  here  The H y b r i d Technique "^^C.TSS F.TSS WFCC  IDLE  WFTR  DATA  dr (dr=ui) /ndreq, tdind dr (droui) /ndreq, tdind  teres (qr>qe) /dr, tdind tdreq/ dr  tdreq /ndreq ndind /tdind nrind /tdind  DATA DATA o . b . o O i . b . <>0  tcreq (qr=ok) /cr  IDLE  tcreq (qrook) /tdind cr (opook) /dr  WFTR q.e.=...  cr (op=ok, mts<>=0) /tcind cr (op=ok, mts=0) /tcind  DATA i.b.=0 o.b.=0 q.e.=...  WFCC  DATA i.b.=0 o.b=0 DATA o.b.<>0 DATA o.b.=0 DATA i.b.oO DATA i.b.=0  cc (mtsoO) /tccon cc (mts=0) /tccon  teres (qr<=qe| /cc tdatr /-  -/dt  dt/-/  tdati Table 5.2  Augmented EFSM t a b l e f o r C l a s s 0 Transport Protocol.  109  The H y b r i d Technique Each of  the  def-itDFPs:  remaining  t3a,  that  span t h e  t3a:  remote.refer  t3b,  t5a,  :=  remote.refer  :=  tpdu.size  ...;  :=  in.buffer  tpdu.size  as  follows.  = nil)  := n i l ; :=  in.buffer  ...;  <>  (tpdu.size)} nil)  := n i l ; ,  out.buffer tpdu.size  := n i l ; :=  ...;  {out.buffer.set.max.size (cc.in.max.tpdu.size in.buffer  (tpdu.size)}  = nil)  := n i l ;  out.buffer t7, whose  transitions.  are  cr.in.source.ref  (cc.in.max.tpdu.size  parameters  transitions  statements  <> n i l )  {out.buffer.set.max.size  Transitions  The d e f  contains  := n i l ;  out.buffer  t7:  rNFS  := c r . i n . m a x . t p d u . s i z e ;  (cr.in.max.tpdu.size  t5b:  the  cr.in.source.ref  (cr.in.max.tpdu.size  t5a:  in  t 5 b and t 7 .  itDFPs i n these  tpdu.size  t3b:  transitions  := n i l ; t8  and  t9  definitions  The u s a g e s  are  contain do n o t listed  110  usages reside as  of  variables  within  follows:  the  or same  The H y b r i d Technique t7:  cc.out.dest.refer  :=  remote.refer  cc.out.calling.t.addr  :=  calling.t.addr;  cc.out.called.t.addr  :=  called.t.addr;  cc.out.max.tpdu.size  := t p d u . s i z e ;  out.buffer.set.max.size(tpdu.size) t8:  dr.out.dest.refer  :=  remote.refer;  t9:  dr.out.dest.refer  :=  remote.refer;  t6a:  {tdind.out.ts.user.reason  t6b:  =  (dr.in.disc.reason  <>  "user.init")  In  and  t6b,  transition nor  the v a r i a b l e be  equal for  the  require  by  of  output  thus  these  the  p-uses  are  not  each  used,  a  in  values the  def-free  when  above  is  specified.  these  parameter  The  verified  and  within.  correctness when  both since  Domain t e s t i n g  using  here.  variables  that  have  data  path  (def-itDFP)  111  t6a  testing  not a p p l i c a b l e  flow  is  exists  p-uses  during  of  p-uses  parameter  the  span  p-uses  transitions  list.  exercised  of  the  output  Both  neither  contain  and v e r i f y  the  are  completely  of  that  automatically  and t 6 b  boundary-interior For  are  test  both  The e f f e c t s  tdind.  to  included  t6a  they  an a d d i t i o n a l  primitive  p-uses  transitions  although  use-itDFPs,  observing  "user.init,"  are  "user.init")  dr.in.disc.reason.  verified  to  t6a  t 6 b must be e x e r c i s e d They  dr.in.add.clr.reason;}  (dr.in.disc.reason  def-itDFPs  can  :=  been  defined has  to  but be  The H y b r i d Technique generated  to  connect  extend  to  a  it  Similarly do n o t to  for  the in  if  defs  listed  defined  with  extracted uses of the  The  directly  reach is  the  follows  in  the  variable that  are  (d,u) def  no  def-free in  "u"  use.  remote.refer:  def  of  path  another in  the  - t3a,  use - t 7 , :  the  transition  first; the that  exists  - t3a,  t3b,  entire  rNFS.  in  for  transition  use  - t5a(d,u),  112  t5a,  in  t5b t7  usage the  any  indicates  t5b(d,u),  in  "def"  t9  def  contain  the  t3b t8,  is  a def  the  variable  are  follows  used without  notation  Those  rNFS t h a t  from  its  containing  that  "use"  has  (use-itDFP)  above.  same  the  path  can v e r i f y  listed  indicates  a  The  with  extracted  by  an u n o b s e r v a b l e  tpdu.size  in  definitions  transitions  list  to  correctness.  usage  which  the  "use"  listed  also  occurring  use.  the  in  transitions  notation  hence,  use  Those v a r i a b l e s  is  preceded  variable  a  first;  transition  transition; that  without  from a l l  that "d"  each  its whose  its  a transition the  possible,  A def-free  to  lists  if  verify  variables  variable  to  the v a r i a b l e .  same  list  each  of  "def"  can  and,  same t r a n s i t i o n .  of  uses  usage  those  The f o l l o w i n g  and  variables  the  its that  of  possible,  correctness. the  uses  a def  and t h e n ,  to  transition  reside  connect  it  is  same  def  of  order  to  that  it  The H y b r i d Technique in.buffer  :  def  - t5a,  t5b,  t7  use - t l 2 . t l 3 ( d ) out.buffer  :  def  - t5a,  t5b,  t7  use - t l O . t l l ( d ) remote.refer  calling.t.addr  called.t.addr  :  use - t 7 ,  :  def - t 3 a ,  :  use -  t7  def  t3a,t3b  :  tpdu.size  :  -  the  predicates,  but  they  are  compared and t h e  observing  are  the  t3b  t7  def  t3a,t3b  -  use -  they  extracted  t9  use -  def For  t8  t7  - t3a, are  t3b,  not  and t h e  transitions  differences  differences,  included in  are  verified. cr.in.max.tpdu.size tpdu.size  tpdu.size  :=  <> n i l  ->  cr.in.max.tpdu.size :  = nil  :  <> n i l  ->  : = . . . ;  cc.in.max.tpdu.size tpdu.size  :  ->  := c c . i n . m a x . t p d u . s i z e :  = nil  113  ->  that  listed  when p o s s i b l e ,  the  as  the  above they  list  enable  follows. p-uses  can  By be  The H y b r i d Technique tpdu.size  :=  ...;  dr.in.disc.reason  : = "user.init"  tdind.out.ts.user.reason :  ->  := d r . i n . a d d . c l r . r e a s o n  <> " u s e r . i n i t "  ->  ~(tdind.out.ts.user.reason) As  can  be  externally def  of  while  each  the  of  formed t o  variable  in t7,  t3a  and  reason  is  testing  the  listed  def-free for  only to  the  t7,  def  t3b and  t8  the  only  is in  :  of  used to the  based  that  listed  the  & use-itDFP)  t3a.t7  (def-  & use-itDFP)  t3b.t8  t3a.t9  (def-  & use-itDFP)  t3a.t7  (def-  & use-itDFP)  t3b.t7  has  for  the  appear  in  in  order  a def The  only  required  variable.  to The  during  following  augmented  above,  (def-  114  t9  process! on  path  that  are  verify  the  externally.  appear  paths to  if  usages  defs  and t 3 a  verified  def-free  unverified  uses  (use-itDFP) :  be  Note  unverified  to  formed,  a  a use.  its  each of the v a r i a b l e s  tpdu.size  can  verifiable  def-free  verified  are  remote.refer  are  to  since  a use t h a t  itself  paths  p-use  variables,  three  defs  because  is  two  t 8 and t 9 and i t s  connecting t3a all  last  " t p d u . s i z e " c a n be v e r i f i e d  bring its  t3b,  verify  the  first  remote.refer,  only  table,  above,  the v a r i a b l e  For t o be  seen  EFSM  The H y b r i d Technique calling.t.addr  :  called.t.addr For  the  t5b  :  cannot  reach  hence,  externally effect  the  the  of  the  externally  it  variable is  at  t7  in  these  and is  its  for  and t 3 b . result,  the  used i n can  These d e f s the  transitions  The d e f s not  used;  their  the  variables  they  assign  conditions  absences  of  transitions  the  to  for  the  outputs  necessary, the  t5a  and t 5 b  cannot  defined  also  exercised  do  by  so t h a t  115  the  during  in  not  is t3a  t7.  As  a  these  However,  are  since  satisfy  the  transitions,  the  these  spontaneous  the defs are  def-itDFPs  that  and o u t . b u f f e r  spontaneous  indicate  the  use-itDFPs  that  since  transitions  verified.  produced  cannot  The c o n v e r s e  in  in.buffer be  the  same t r a n s i t i o n be  be  parameter  Nevertheless,  transition.  values  during testing  Whenever identical  cannot  them  enabling  input  the  and  implies  cr.in.max.tpdu.size  verified.  hence,  defs  of  t5a  re-defined  c a n be d e f i n e d by t r a n s i t i o n  also  of  also  the  still  variable  p-uses  are  being  This  verified.  use  tpdu.size  transitions  transitions  of  t e s t i n g by s i m p l y e x e c u t i n g t h e true  in  without  transitions  tpdu.size, in,  defs  verified.  observed  defined  in  p-uses  cc.in.max.tpdu.size  the  and  t3a.t7  its  use  defs  observed  t3a.t7  (use-itDFP)  tpdu.size variable,  first;  be  (use-itDFP)  are final  correct.  selected test  to  be  sequence  The H y b r i d Technique may be data  reduced.  flow  t3b.t7;  The r e s u l t i n g  testing  that  procedure  itDFPs  are  to  t3a.t7,  cr(option=ok,  (def-  (def-  tdreq/dr  tdind  (use-itDFP) max.tpdu.size=nil)/tcind.  teres(qts.req<=qts.estimate)/cc the  def-itDFPs,  f o r m e d by  using  EFSM t o e a c h o f  the  bring  itDFPs  special This  their  the  preamble,  flow  previously  used  preambles  first  not  be  use.  is  For as  to ensure  correct the  follows.  to  IDLE that  before  tail  subsequences to  bring  then a postamble  are  time.  is of  e.transitions,  a  executability.  the  EFSM  verified  def-itDFP  If  the  any  ensure in  state  t h a t the  test  each  formed t o  used  s h o u l d have i t s  the  transitions,  transitions  procedure,  at  & use-itDFP)  data  need t o if  (def-  their  EFSM b a c k  includes  preamble  This  & use-itDFP)  max. t p d u . s i z e o n i l ) / t c i n d .  cr(option=ok,  to  and  & use-itDFP)  cr (option=ok,  used  t3a.t9  max.tpdu.size=nil)/tcind.  teres(qts.req>qts.estimate)/dr,  are  the  max. t p d u . s i z e o n i l ) / t c i n d .  tcres(qts.req<=qts.estimate)/cc  For  t3b.t8,  in  is,  cr (option=ok,  ,  be v e r i f i e d  prior  indeed  testing to  its  originated  transition.  use-itDFPs, For  their  test  each u s e - i t D F P ,  116  the  subsequences EFSM i s  are  brought  formed to  its  The H y b r i d Technique first  transition  again  using  whenever p o s s i b l e , t h e n t h e The  EFSM  is  postamble. itDFP,  the  The  the  The from t h e DFTP:  back  formed  the  portion  usage  verified  correct  brought  to  to  be  ensure  previously  use-itDFP  path  excluding  housing state  then  a  by  to  use  IDLE  preamble  must  preamble  concatenated to  begins  examined, the  the  the  that  is  used  at also  state and the  it.  using the  a  use-  transition  have  its  tail  examined i n d e e d r e s i d e s  at  transition.  following above  four  cr (option=ok,  data  flow  test  subsequences  itDFPs. max . t p d u . s i z e o n i l ) / t c i n d .  teres(qts.req<=qts.estimate)/cc.tdreq/ndreq cr (option=ok,  max. t p d u . s i z e o n i l ) / t c i n d .  teres(qts.req<=qts.estimate)/cc.tdreq/ndreq cr(option=ok,  max.tpdu.size=nil)/tcind.  teres(qts.req>qts.estimate)/dr, cr(option=ok,  max.tpdu.size=nil)/tcind.  teres(qts.req>qts.estimate)/dr, cr (option=ok,  tdind  tdind  max. t p d u . s i z e o n i l ) / t c i n d .  tdreq/dr cr(option=ok,  max.tpdu.size=nil)/tcind.  teres(qts.req<=qts.estimate)/cc.tdreq/ndreq cr(option=ok,  max.tpdu.size=nil)/tcind.  teres(qts.req<=qts.estimate)/cc.tdreq/ndreq  117  are  formed  The H y b r i d Technique Since  all  the  def-itDFPs  not r e q u i r e d i n t h i s each use-itDFP t o WFTR i n  n o t be v e r i f i e d because  they  All  paths  the  ones,  the  from  DATA  example.  has a l r e a d y  testing  the  transitions  at  IDLE  tdreq/ndreq  to  subsequences are  the  def-itDFP  either  postamble back  a  IDLE.  the  a  first  preamble  is  transition  at  been u s e d as a p r e a m b l e  Some o f  represent  IDLE,  Since the  EFSM p o r t i o n ,  again.  end  begin at  their  need  duplicated  as  use-itDFP.  or is  two  states  sequences are well  as  DATA. used  Added  following  tail  f r o m IDLE  For  to  to  a  the  bring the  latter  the  above  subsequences  for  EFSM test  testing  t 6 a and t 6 b .  tcreq(qts.req=ok,  disc.reason="user.init")/cr.  dr/ndreq,tdind tcreq(qts.req=ok,  disc.reasono"user.init")/cr.  dr/ndreq,tdind Length procedure  of  is  subsequences inputs.  If  of  reduced to  22. are  test  After  for  the  optimization the  length  data  in  is  flow  which  reduced  inputs  and t h e in  this  7.  118  duplicates procedure  testing  duplicate to  s u b s e q u e n c e s were compared t o t h o s e  procedure  test  sequence  removed,  these  EFSM t e s t i n g number  the  14  test  in  the  were r e m o v e d ,  the  would  be  further  The H y b r i d Technique  5.5 CHAPTER SUMMARY This  chapter  a p p l i e d to the their  Estelle In  are  is  their  testing to  starting  that  procedure,  If  can  hybrid  the  technique  transitions  that  since  their  spontaneity  still  TSSs be  satisfied,  input  which  length  83,  Class  where  transitions  can  be to  by  any  input  generate  an  test  inputs  are  for  testing  and  7  length  the  final  UIOSs c h o s e n i n t h e  test  EFSM t e s t i n g  119  them.  require are  which  transition,  that  enabled  they  are  C.TSSs  then  they  transition.  are  sequence  enable  do n o t have  example,  optimized  76  transitions  turn  to  0 Transport Protocol  structure of  in  spontaneous t r a n s i t i o n s  enabled  would  spontaneous  input  the  be  the  s h o u l d n o t be appended t o any i n p u t For  technique  those  appropriate  appended.  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  possible  the  how  specifications.  appended  This  by  the  shows  the  test  for  procedure.  of  hybrid  sequence  testing  flow  varies  the  the  data.  according  of EFSM The  to  the  6 EVALUATION AND COMPARISON OF THE HYBRID TECHNIQUE The  hybrid  generation  technique  method  that  is  implemented a c c o r d i n g t o principles  behind the  FSM t e s t i n g , according  its  those  s h o u l d be  verified  protocols This  hybrid  conformance  applicable  method a r i s e  features by  to  Estelle  that  other  from l e s s o n s  is  are  means.  technique  provides as  well  method t o o t h e r n o t a b l e  a  as  test  a  protocols  in  enough;  externally The  from  an  IUT  whenever observable  interactive method o f  general  evaluation  general  comparison  sequence g e n e r a t i o n  The  learnt  features  not  not  sequence  testing  lend themselves w e l l to t h i s  chapter  test  specifications.  e x e r c i s i n g the  specification  possible,  of  a  their  where m e r e l y  to  is  nature testing. of of  the this  techniques.  6.1 EVALUATION  6.1.1 F a u l t  Coverage  Since testing  the  methods,  coverage  is  Fault  extra  its  also  p r o d u c e d by t h e  i n terms  hybrid  STATE  fault  detection  combination  of  of  a  combination capability the  the h y b r i d technique  an e r r o n e o u s E s t e l l e and  is  or  of  two fault  fault  coverages  c a n be  expressed  two m e t h o d s .  coverage  of  a  technique  statement  exists  120  specification. in  the  Provided  erroneous  no  Estelle  E v a l u a t i o n and comparison specification, all  the  STATE e r r o r s ,  and usage  statements  technique  primitive  effects  erroneous  IUTs  that  are  errors  are  expressions.  is  capable  of  detecting  errors  in  those  errors,  whose e f f e c t s  and p o s s i b l y  whose  mathematical  Estelle  I/O  statements  and v e r i f i a b l e ,  all  hybrid  externally  in  those  not v e r i f i a b l e These  can  be  errors  are  described  observable  def  or  and  they  usage  contain  detectable  by  def  the  in  erroneous  specification.  6.1.2 E x e c u t a b i l i t y In taken  the  hybrid  into  sequences,  approach,  consideration the  resulting  Ensuring executability to  be  performed  The d i s a d v a n t a g e of  sequence  required. the  special  that  generation  test  the  sequence  and  at  of  test  most  121  all  data  that  the be  test  selection  has  procedure. the  process may  be  presentation  of  augmented  by  s e l e c t i o n can  value c r i t e r i o n used  are  executable.  computation  Test data  implementation.  generating  added t o  inputs  commonly  conditions  generation  times,  requires  of are  some t e s t  sequence  input value required.  the  process  sequences  be b a s e d on t h e b o u n d a r y - i n t e r i o r choosing  enabling  complexity i s  Executability  resulting  the  implies  during is  in  since  values  in  any  again  o r done by a  real  E v a l u a t i o n and comparison 6.1.3 A p p l i c a b i l i t y The are  test  tailored  described  for  by  sequences  sequences  an  to  erroneous  any  from w h i c h  it  IUTs  IUT is  include  transition of  Estelle  detect  is  the  test  in  well  the  as  as  of  an  sequences  IUT  branch  generated takes and  the by  applies  control  would  those  which  IUTs  but  the  type  can  The  be test  implemented  they  tree  of  that  can  of  also  be  specification  the  FSM-based  structure.  I/Os  Estelle  sequences  sequences  may  in  a protocol,  IUT. I/Os  the  control  structure  a tree,  t h e n an  erroneous  If  be  detected The  by  techniques  of to  assume  sequences  hybrid  structure  control  also  not  they  EFSM c o n t r o l  122  These  given  across  of  flow),  technique.  Checking the  capable  executed i n the  that  flow).  testing  a  be  test  Estelle  protocol.  within  (data  not  still  the  would  Recall  values  hybrid the  of  sequence of  may  are  exist  What  (control  the  advantage  to  flow  had been i m p l e m e n t e d as  of  IUT  technique  specification.  sequences  follows.  n o t o n l y assume c e r t a i n certain  hybrid  implemented a c c o r d i n g t o  data  that  an e r r o n e o u s is  an  suited  not  transitions.  The r e a s o n  in  specifications,  are  paths  as  Estelle  independent of  that  errors  flow  the  generated.  specifications, detecting  by  errors  especially  Estelle  a p p l i e d to  For  detecting  are  according  generated  technique a  protocol  check  structure  of  this such  E v a l u a t i o n and comparison an  IUT  thus  requires  knowing t h a t  the  less  structure  An a l t e r n a t i v e  unknown w o u l d be t o  the  Estelle the  FSM  of  However,  is  test  size,  m o d e l l e d by  the  coverage  6.1.4 T e s t Data The  Any  indicated  for  each  test  knowing t h a t  that  value a  required  test  During  generated  s h o u l d be for  sequence  test  be u s e d i n o r d e r t o t e s t than  could  either  chosen  set  the  sequence  the  control of  it  reducing  data  simply  the  indicate  considered during a  test  generated  selection,  a  by  is  the  test  their be of  implementation.  the  effects. based  most If  the  on  correctness The  of  boundary-interior  frequently latter  123  is  used not  also hybrid  subsequence value  of v a r i a b l e  selection  the  testing.  input  may n e e d t o be d u p l i c a t e d s i n c e more t h a n one t e s t  rather  if  advantage  sequence w i t h o u t  in  branch  encountered or  an FSM and t a k i n g  sequences  in  technique.  IUT  FSM  Selection  I/Os  special  the  the  producible.  test  sequences of  require  structures  according to  resulting  Hence,  can c o n s i d e r a b l y reduce a t e s t fault  does  IUTs whose c o n t r o l  when l o o p s a r e  considerable  it  m o d e l l e d by an EFSM.  and  c o u l d be h o r r e n d o u s l y l o n g . structure  however,  span a t r e e  specification  tree.  is  is  to t e s t i n g  are  in  work;  usages,  input  values  values  values  available,  in the  may  or a  a  real former  E v a l u a t i o n and comparison c a n be  used;  p-uses,  else,  since  it  possibilities  fussed  be  over  latter  can  are  would a l r e a d y be  the  generally  completely included  with  specified,  then,  "NOT b"  and  data  selection  alternatives  in  during data  conditions  test  should take  the  into  be  precedence.  assumed  specified, the  test  This  AND.  If  and "NOT a " does  that  and n e e d  also "a  have  AND  to  not  applies b"  w o u l d a l s o be  not  all  possibility  sequence  selection.  keyword  each  For  to  were  specified  take  these  consideration.  6.1.5 T e s t a b i l i t y A  protocol  addition state" the  of  feature length  is  that  [Sari84],  is  then  addition, these  the  lower  IUT  testers  report  an i n c o m p l e t e l y Completeness  of  requires The  The  IUT  "read  to  addition  the  report of  each of which  this is  of  problem  messages  to  o f OSI  current  can  be  state  to  testability  specification  Assumptions.  124  A  used  protocols  by  both  s y n c h r o n i z i n g the  increasing  specified  at.  the  with  s y n c h r o n i z a t i o n were a  testing  as a means o f  A n o t h e r way  the  if  testable  Sari84].  always e x i s t ,  status  its  easily  [Aho88,  currently  UIOSs w i l l  In  more  i n p u t which  s y n c h r o n i z a t i o n i n the that  made  messages  an  it  implies one.  be  "status"  message  STATE  can  is  requiring upper  and  two. by  [Sari84]  "DEFAULT"  aid  completing w i t h one  feature  can  of be  E v a l u a t i o n and comparison added t o E s t e l l e to  specify  a  "otherwise"  together,  to the  Completeness  is  primitives  similar  used  to  together,  "PROVIDED o t h e r w i s e "  Assumption.  group  and  all  For  the  "ANY_STATE"  feature  instance,  unspecified  groups  all  ,if  input  the  states  then  DEFAULT: WHEN  otherwise  FROM ANY_STATE TO SAME BEGIN END; specifies  the  state  ignored  is  assumption t h a t and  s t a t e and no o u t p u t  is  the  any  machine  generated.  input  not  remains On t h e  specified at  other  its  for  a  current  hand,  DEFAULT: WHEN  otherwise  FROM ANY_STATE TO ERROR BEGIN OUTPUT  input_error();  END; the after  above it  [Sari84]  default outputs upon  sends a  the  message  reception  of  protocol complaining an  125  to of  unspecified  the an  ERROR  state  input  error  input.  At  the  E v a l u a t i o n and comparison ERROR  state,  disconnect protocol  all  or  further  reset  will  input  return  DEFAULT t r a n s i t i o n s the  last  where  so  no  would  initial  defaults  an  is  be  received,  unspecified  time  state.  to  the  the  specified similar  as to  related  specification  becomes  required  a  These  i n a group of  input  be  until  which  specification,  situated  would  at IDLE  any m o d i f i c a t i o n  modification  ignored  and s h o u l d be  i n an E s t e l l e  If  that  is the  "PROVIDED o t h e r w i s e "  done  one,  to  are  transitions  PROVIDED c l a u s e s . is  inputs  a  specified  at  the  DEFAULT  the  FSM  testing  transitions.  6.2 COMPARISON The  hybrid  techniques  technique  in  on t h e i r  applications  to E s t e l l e  this  section. to  techniques,  the  addition,  [Ural88]  T h e s e methods a r e testing  the  the  hybrid  hybrid  c o m p r e h e n s i v e i n terms o f  while  to  IUTs  and  Sarikaya  compared b a s e d  implemented  according  specifications.  comparing  techniques  compared  and t h o s e d e v e l o p e d by U r a l  [Sari87]  In  is  examine hybrid the  only  test  technique fault  the  technique  technique  also  is  coverage  control  with  b e c a u s e FSM  its  s e q u e n c e s g e n e r a t e d by t h e  126  testing  obviously  structure  examines  FSM  of  data FSM  more testing  protocols flow.  In  techniques  E v a l u a t i o n and comparison may  not  be  technique In since  executable  while  comparing  the  the  data  the  flow  IUT,  coverage  hybrid  portion  the that  follows  using  the  control  structure  Transport STATES,  of  because  contains all  the  the data  tree  the  n o t have b e e n a b l e  spans, is not  able  paths  also  among  one o f  valid  detected,  to  in  hybrid  Ural,  also  tested  structure  achieves  better  example  is  Protocol.  only  many  WFCC  this a  correct  in  the  the  error. tree  the  of  the  EFSM.  erroneous flow error,  STATES  WFCC  and WFTR  branches  incorrect.  IUT  go  could  the  10 s e q u e n c e  obviously  127  to  its  which result, of  IUT.  paths,  state  the  reason  of  As a  the  extra  approach  implementation  data  three were  The  part  the Since  it  but the is  as  If  states  STATE; then U r a l ' s  a correct  to detect  the  the  is  of  implementation  spans  be p r e s e n t  Merging  is  that  An  and  detect  EFSM  them i m p l i e s  which  Ural.  WFTR  a single  approach examines  because,  the  control  also  Transport  spanned by t h e  flow  approach would.  with  protocol  erroneous  erroneous  p r o t o c o l would Ural's  by  were m o d e l l e d by an EFSM w i t h o n l y  been  the  by  0  an  instance,  have  the  technique  Class  e r r o n e o u s l y merged i n t o would not  of  produced  Protocol for  technique  i n a d d i t i o n t o the  hybrid  than  is  generated  are.  i n the h y b r i d technique of  those  would hybrid  an  erroneous  error EFSM  cr/tcind.cc/tccon  If data  this  error  transfer  were state  E v a l u a t i o n and comparison upon r e c e i v i n g one  after  response  a connect  another  from  its  request  from  the  user.  and a c o n n e c t  peer  confirmation  protocol  The merged STATE  without  is  thus  any  an  error  and s h o u l d be c a p t u r e d . In takes  terms  of  executability,  executability  generation  into  process,  since  the  consideration  during  sequences  generates  the  it  e x e c u t a b l e w h i l e t h o s e g e n e r a t e d by U r a l In the  comparing the  same  erroneous  Sarikaya's  method  hybrid  present  the  in  erroneous  correct  EFSM;  and  coverage  IUT. in this  In  terms  technique that of does  is  Ural  and,  Sarikaya,  of  the  detect  also  data  IUT  would  the  hybrid  test  derivation  complex  because as  example  would  of  Sarikaya,  can  be  be  be  used.  underlying  includes all  be  be.  the  flows  also  sequence  the  the  one  subtours  present  in  the  present  in  the  present  in  the  technique  provides  better  sense.  more  consideration. by  Hence,  that  As a r e s u l t ,  EFSM w o u l d  all  correct  not  to  technique  its  may n o t  spans a t r e e t h a t  EFSM.  the  corresponding erroneous  correct  Protocol  would  e r r o n e o u s EFSM b e c a u s e i t spanned by  technique  Transport again  hybrid  well,  it it  However, the  hybrid  than  has  in  those  to  has  complexity, for  testing  do more t h a n to  take  128  seems  any  one o f  approach  simpler  hybrid  FSMs  executability  comparison t o the  technique  the  and them into  taken  because  it  E v a l u a t i o n and comparison does n o t have technique,  to generate  however,  the  complex d a t a  does  require  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 t o be s e l e c t e d d u r i n g t h e addition, the may  in  effects be  the of  used  to  verify  technique  demands  semantics  of  this of  sense,  the the  that  of  values  and t e s t  into  d a t a may  p-uses,  differences  have  t o be i d e n t i f i e d  the  p-uses.  more  technique  Sarikaya.  129  Hence,  attention  specification  hybrid  taking  The  have  sequence g e n e r a t i o n p r o c e d u r e .  verification  t h e p-uses  flow graphs.  than is  be  given  Sarikaya's more  among  so t h a t the  complex  In  they  hybrid to  the  does.  In  than  that  7 CONCLUSIONS This summary future  section  of  its  brings  this  achievements  work i n t h e  area of  thesis  and  a  to  a  close  discussion  conformance  with  of  a  possible  testing.  7.1 THESIS SUMMARY Contributions the  development  of  eUIOv-method  and  formation  the  of  of  this  the  thesis  lie  in  UlOv-method, the  the  data  hybrid  flow  three  developments  testing  technique  main  and  areas: of  procedure,  its  the the  application  to  Estelle. This  thesis  techniques that protocols previous  the  claim  method achieves In  weak  faulty  (U-method)  adding so  by  that  full  a  It  that  does  of  the  not  fault  coverage tests,  provided  not exceed t h a t which  the is  it  found, most  full  U-method, in  strong  is  also  number o f i n the  130  testing  contrary  recently  procedure,  revised  FSM  conformance t e s t i n g  specified  verification the  notable  provide  completely  conformance IUTs  examining  FSMs.  [Sidh89],  testing  proposed  by  c a n be a p p l i e d t o t h e  modelled  UlO-method in  began  coverage  protocols. ~Uv,  to  in  s p e c i f i e d FSM.  It  the  U-  UlOv-method,  conformance  capable  a  developed  fault  or  states  to  of  of these The  tests.  detecting IUTs  do  D-method  Conclusions and t h e W-method were f o u n d t o be s p e c i a l  cases  of  the  UIOv-  method. This  thesis  Sequences  (UTSs)  s h o u l d have is  a  it  is  of  generated contains  does  then  not  all  UTSs.  capture  I/Os  that  so t h a t  a  s p e c i f i e d FSM. IUT  to  proposed  the  the  i n order to achieve  sequence  UTS  also  is  any  skeleton  exceed t h a t  faulty  IUTs  fault  unique  to  that  FSM if  be  is  This thesis to generate modelled  test  by  executable  since  consideration system  state  Hence,  all  verified,  The  the  total  during is  verified  elements  thesis static  in  of  flow  data  analysis  FSM t e s t i n g .  The p r o c e d u r e e x t e n d s  def-use  flow  data  by  paths  to  tests  a state  the  in  the FSM,  eUIOv-method  are  c a n be  sequences  are  taken The  is  in  into total  an  FSM.  exercised  and  testing. flow and the  verifying,  131  an  employing  system i s  an EFSM t r a n s i t i o n  possible, during  data  to  states  process.  same way  a  using  specification  test  the  generation the  which  tests.  generated  developed  a test  testing protocols that  state  the  such  An UTS  FSM f r o m  UlOv-method t o an  sequences f o r  whenever  This b a s e d on  extended the  EFSMs.  the  Test  sequence  identical  captured  The UlOv-method g e n e r a t e s  test  number o f  in  Unique  coverage. the  is  the  of a  passes  that  which  can  property  full  IUT  As a r e s u l t ,  concept  testing lessons basic  procedure  learnt  from  exercising  whenever  of  possible,  Conclusions that is  each def  within This  the  out  correct,  correct  thesis  an E s t e l l e normal  is  specification. transitions The  so t h a t  that  EFSM  appear  flow to  generating  a  resulting test  operations. technique  is  a  A  protocol  as  I/O  of  values  consider both of  the  structure  of  advantage  control  of  structure  when as  is  well  as  its  132  true  brings Estelle EFSM  combined w i t h that  or  applicable  for  protocols The  either  have  erroneous  10  by  achieved  the  is  IUTs t h a t  equally Testing  these  testing  an  of  the  by  hybrid  the  eUIOv-  procedure.  are.  well  in  redundant  achieved  those  are  specifications.  aspects.  some p r o t o c o l s  t h e s e models l e n d themselves taken  faulty  I/Os  should thus control  is  Estelle  flow t e s t i n g  sequence  its  of  from  sequences  coverage  form  eliminated.  structures  combination  correct  flow  technique  their  fault  method and t h e d a t a  data  test  control  The  p-use  separately  testing,  sequences d e t e c t  EFSM  rNFS,  procedure  conformance  normal  the  i n an NFS a r e  hybrid  the  transitions  EFSM  implemented a c c o r d i n g to  erroneous  and  testing  form  and e a c h  its  new f o r m a t ,  During  data  eUIOv-method to  and r e f o r m a t t e d  specification  underlying  correct  domain.  refined  f o r m and i t s  the  e a c h use i s  important of  FSMs  this  such p r o t o c o l s flow  so  aspect  a  protocol can model  effectively.  to t e s t i n g ,  data  a  in  Since  s h o u l d be that can  its both  Conclusions be  examined  during  testing.  d e v e l o p e d t o do j u s t The  hybrid  that  EFSM c o n t r o l  capable  detecting  would  of  otherwise  be  Ural  and S a r i k a y a .  data  flow  of  data  resulting  test  less  it  is  employs a  by  for  this  the  protocols  technique  erroneous  techniques  thus  EFSMs  that  developed  capable  certain  that  with  is  also  of  was  protocols.  the h y b r i d technique  technique  testing  sequences  data  detecting  would o t h e r w i s e  set  more complex t h a n however,  are  of  parameters  or,  values  w o u l d be c h o s e n .  it  by  includes types  be m i s s e d  for  the  and i t  hybrid  sometimes  Ural  that  is  the  generally  technique  used v a l u e s  unavailable,  To e n s u r e  of  Sarikaya.  most f r e q u e n t l y if  that  guarantees  executable  d e v e l o p e d by  selection  finite  is  is  FSMs;  input  selection  tailored  IUTs w i t h  i n an IUT  complex t h a n t h a t Test  of  technique  techniques.  The h y b r i d for  faulty  hybrid  type  structures,  missed  flow errors  and t h o s e  was  Since  testing,  by FSM t e s t i n g  for this  technique  underlying  The  for  the  boundary-interior  executability,  combined  either  with  test  test  data  sequence  selection. Test also  sequences  applicable  Estelle  to  generated IUTs  specifications.  not The  by  the  hybrid  implemented fault  133  technique  according  coverage  are  to  their  achieved  would  Conclusions be  limited  to  may n o t be  faults  in  the  I/Os;  sequencing  faults  may  or  captured.  7.2 FUTURE WORK A tool the  is  being developed i n another  hybrid technique developed i n t h i s  be  easily  applied  specifications.  to  more  Existing  study to  thesis  complex  implementation  symbolic execution to  implement the h y b r i d  a c h i e v e d by t h e optimize  the  detection  has  test  flow a n a l y s i s  emphasized  on  test  sequences  capabilities  are  maintained  can  for  the  c a n be c o u p l e d w i t h technique.  the  fault  s e q u e n c e s ; more r e s e a r c h  resulting  it  protocol  techniques  data  thesis  so t h a t  Estelle  UlO-method and s t a t i c  This  implement  is  required  such t h a t and  coverages  their  the  UTSs  to  fault remain  unique. For  test  parameter  data  values  as i n p u t s d u r i n g In layer  the  selection,  IUT  Perhaps  can the  tested  Estelle  be combined i n  commonly they  may be  p r o t o c o l s , more t h a n one  been i m p l e m e n t e d as  be  of  used used  testing.  IUT may be embedded w i t h i n an  list  s h o u l d be c o m p i l e d so t h a t  t e s t i n g o f OSI  may have  a  a large  still  similar  134  to  unit  implementation.  needs  specification  a manner  a single  to  be  f o r each of that  of  protocol  so t h a t  an  How s u c h  investigated. the  an NFS  layers  can  so t h a t  a  Conclusions single  specification  implementation. develop  test  implementation  This  exists  specification  sequences either  for  to  as a whole  135  the may  test  multi-layer  then the  o r one l a y e r  be  used  to  multi-layer at  a  time.  BIBLIOGRAPHY [Aho88]  Aho,  A.V.,  Dahbura,  "An  Optimization  Test  Generation  Chinese  on  Chan,  Tours,"  W.Y.L., for  Symposium  on  Lee,  Chan,  Improved  UIO  Sequences  City,  N.J.,  S.  Protocol  Proc.  ACM  Architectures  and  M.R.,  and  "On  Ninth  Test  International Testing  and  June 1989. and  Ito,  M.R.,  Procedure  Symposium, Austin,  Protocols,  Rural  International  Ito,  S.T.  '89  and  1988.  Generation  Sigcomm  and  Conformance  Specification,  Test  U.M.,  Testing,  Proc.  Vuong,  Uyar,  Eighth  Specification,  Protocols,"  Protocol  and  Protocol  Proc.  Vuong,  W.Y.L.,  D.  for  The N e t h e r l a n d s ,  Verification,  UIOs,"  on  Protocol  Generation  [Chan89b]  Based  Atlantic  Verification, [Chan89a]  Technique  Postman  Symposium  A.T.,  Based  "An on  Communications Texas,  September  1989 [Chan89c]  Chan,  W.Y.L.,  UIOv-Method  For  International Germany, [Chow78]  Protocol  Workshop  T. ,  State  Engineering,  S.T.  on  and  Ito,  Testing," Protocol  M.R.,  "The  Proc.  Second  Testing,  Berlin,  O c t o b e r 1989.  Chow,  Finite  Vuong,  "Testing  Machines," vol  SE-4,  Software IEEE  no.  136  3,  Design  Transactions 1978, p p .  Modelled on  178-187.  by  Software  Bibliography [Gone70]  Gonenc,  Detection vol.  G.,  "A  Experiments,"  Hecht,  New Y o r k : [IS088]  M.S.,  IEEE  the  Design  Transactions  of  Fault  on  Computers,  Flow  Analysis  o f Computer  Programs,  N o r t h - H o l l a n d , 1977.  ISO/TC97/SC21/WGl/Subgroup  Description  Technique  Transition Model,"  IS  Based  B,  "Estelle  - A  Formal  on  an  Extended  State  9074, 1988.  K o u , T . , " C o n f o r m a n c e T e s t i n g o f OSI P r o t o c o l :  Class  0  Transport Dept.  British  Columbia, August  [Nait81]  Naito,  Sequential Fault [Rapp8 5] Test  S.  Rapps, Data  OSI,"  As  Master  the U n i v e r s i t y  M. ,  "Fault  by T r a n s i t i o n T o u r s , "  of  Data  on Software  E.J., Flow  Detection  for  Proc.  IEEE  of  1981.  Conference,  and Weyuker, Using  Example,"  The  1987.  Computing  S.  An  Science,  and Tsunoyama,  Tolerant  4, A p r i l  Computer  Machines  Transactions  [Rayn86]  of  Protocol  Thesis,  V,  for  C - 1 9 , n o . 6, June 1970.  [Hech77]  [Kou87]  Method  "Selecting  Software  Information,"  Engineering,  v o l . SE-11,  IEEE no.  1985, p p . 367-375.  Rayner, Protocol M.Diaz,  D.,  "Standardizing  Specification, Ed.,  Conformance Testing  North-Holland,  N e t h e r l a n d s , 1986.  137  and  Testing for Verification,  Amsterdam,  The  Bibliography [Sabn88]  Sabnani,  Generation 4,  K . K . and D a h b u r a ,  Procedure,"  Sarikaya,  with  Test  B.  v o l . 15, no.  Networks,  Ed., [Sari84]  a n d Bochmann,  Sequence  Specification,  Generation  Testing  North-Holland, Sarikaya,  and  B.  April [Sari86]  on  Form  Experience  for Protocols,"  Protocol  C.  Verification,  Sunshine,  1982, p p . 555-567.  Issues  G.v.,  in  Protocol  Communications,  vol.  B.  a n d Bochmann,  Specifications  Usage:  Recent  Szentivanyi  (Eds.,),  Design  Transactions  for  "Synchronization Testing," COM-32,  IEEE  no.  B.,  G.v., "Obtaining  Protocols," L.  Experiences,  Sarikaya,  Test  "Some  4,  1984, p p . 389-395.  Sarikaya,  [Sari87]  and  G.v.,  and Bochmann,  Specification  Transactions  [Sidh88]  Computer  Test  1988, p p . 285-297.  [Sari82]  5,  A . T . , "A P r o t o c o l  Csaba,  North-Holland, Bochmann, for  on  Engineering,  Software  Computer K.  Tarnay  Network and T .  1986, p p . 6 0 1 - 6 1 2 .  G . v . , and C e r n y ,  Methodology  Normal  Protocol  E.,  Testing,"  "A IEEE  v o l . SE-13, n o .  May 1987, p p . 518-531. Sidhu,  Generation Symposium, Stanford,  D.  and L e u n g ,  f o r Real  T. ,  Protocols,"  Communications  "Experience Proc.  ACM Sigcomm  Architectures  C A . , A u g u s t 1988, p p . 257-261.  138  with  &  Test '88  Protocols,  Bibliography [ S i d h 8 9]  Sidhu,  Protocol on  D.P.  and L e u n g ,  Testing:  Software  T . K . , "Formal  A Detailed  Engineering  vol.  Study,"  Methods  IEEE  for  Transactions  1 5 , n o . 4, A p r i l  1989, p p .  413-426. [Ural88]  Ural,  Sequence  [Vuon88a]  Yang,  Selection  Estelle," Ottawa,  H. ,  S.T.,  Protocol  Atlantic  Vuong, Clip  Formal  Proc.  Test in  TR-88-18, The U n i v e r s i t y  of  Stirling,  Eighth  Testing,  Symposium  and  Verification,  USA, June 1988.  Local  System  Testing  September  "An  Protocol  International  W.Y.L.,  '88,  W.Y.L.,  Automatic  S . T . and Chan,  Forte  Weiser,  and C h a n ,  for  New J e r s e y ,  Description  First  "Validation Using  International the  Techniques,  An  O f The  Estelle-C  Conference  on  University  of  1988.  M . D . , Gannon,  "Comparison o f S t r u c t u r a l Software,  "A  Specified  R.I.  Specification,  City,  Compiler,"  [Weiss85]  for Protocols  Chan,  Compiler  Implementation,"  Ferry  Method  R.L.,  June 1988.  Vuong,  [Vuon88b]  and P r o b e r t ,  Technical Report,  Estelle-C  on  B.  J.D.  Test  Coverage  March 1985, p p . 8 0 - 8 5 .  139  and M c M u l l i n , Metrics,"  P.R., IEEE  Bibliography [Zimm80]  Zimmermann,  Model  of  H.,  COM-28, n o .  Reference  Architecture  Interconnection," vol.  "OSI  IEEE  for  Transactions  4, A p r i l  1980.  140  Model Open on  -  The  ISO  Systems Communication,  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 w f c c tl: BEGIN local.refer : = . . . ; 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 , called.t.addr, tpdu.size); END;  WHEN t c r e q ( t o . t . a d d r , from.t.addr, qts.req) 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 t2: 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 , ts.user.reason); 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 , max.tpdu.size) 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 t3: 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 , calling.t.addr, qts.estimate); 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.size) 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 t4: 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 ; tpdu.size : = . . . ; 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 , calling.t.addr, qts.estimate); 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 , max.tpdu.size) FROM i d l e PROVIDED c r . i n . o p t i o n <> ok TO i d l e t5: 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 , disc.reason); END;  WHEN c c ( d e s t . r e f , source.ref,calling.t.addr, called.t.addr,max.tpdu.size) FROM w f c c PROVIDED c c . i n . m a x . t p d u . s i z e <> n i l TO d a t a t6: 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 ; out.buffer.set.max.size(tpdu.size); 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 , source.ref, calling.t.addr, called.t.addr,max.tpdu.size) FROM w f c c PROVIDED c c . i n . m a x . t p d u . s i z e = n i l TO d a t a t7: 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 ; out.buffer.set.max.size(tpdu.size); 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 , add.clr.reason) FROM w f c c 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 t8: 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 , ts.disc.reason); END;  WHEN d r ( d i s c . r e a s o n , add.clr.reason) FROM w f c c 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 t9: 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 d a t a 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 ; out.buffer.set.max.size(tpdu.size); 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 , called.t.addr, tpdu.size); 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 := . . . ; dr.out.add.clr.reason : = . . . ; 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 d a t a TO d a t a t l 3 : BEGIN insert(out.buffer, tdatr.in.tsdu.fragment); END;  144  NFS OF CLASS 0 TRANSPORT PROTOCOL FROM d a t a PROVIDED o u t . b u f f e r <> n i l TO d a t a t l 4 : BEGIN remove(out.buffer, dt.out.user.data); OUT d t ( u s e r . d a t a ) ; END;  WHEN d t ( u s e r . d a t a ) FROM d a t a TO d a t a t l 5 : BEGIN insert(in.buffer, END;  dt.in.user.data)  FROM d a t a PROVIDED i n . b u f f e r <> n i l TO d a t a t l 6 : BEGIN remove(in.buffer, tdati.out.tsdu.fragment); 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 d a t a 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 n d i n d ( ) FROM d a t a 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 d a t a 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  tl:  WHEN t c r e q ( q t s . r e q = ok) FROM i d l e TO w f c c 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;  t2:  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 tdind.out.ts.disc.reason tdind.out.ts.user.reason END;  t3a:  := :=  ...; ...;  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 ; qts.estimate : = . . . ; 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 ; qts.estimate : = . . . ; 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;  t4:  WHEN c r ( o p t i o n <> ok) FROM i d l e TO i d l e OUT d r 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;  t5a:  WHEN c c FROM w f c c TO d a t a 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 c o n 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 ; out.buffer.set.max.size(tpdu.size) ; END;  148  rNFS OF CLASS 0 TRANSPORT  PROTOCOL  t5b:  WHEN C C FROM w f c c TO d a t a AND BEGIN in.buffer := 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 c o n 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 := . . . ; out.buffer.set.max.size (tpdu.size); END;  t6a:  WHEN d r FROM w f c c TO i d l e OUT n d r e q , 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 ; tdind.out.ts.user.reason : = dr.in.add.clr.reason; END;  t6b:  WHEN d r FROM w f c c TO i d l e OUT n d r e q , 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 := dr.in.disc.reason; END;  149  rNFS OF CLASS 0 TRANSPORT PROTOCOL  t7:  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 d a t a 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 C C 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 ; out.buffer.set.max.size (tpdu.size); END;  t8:  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;  t9:  WHEN t d r e q FROM w f t r TO i d l e OUT d r 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 tlO:  WHEN t d a t r ( t s d u . f r a g m e n t ) FROM d a t a TO d a t a AND insert(out.buffer,tdatr.in.tsdu.fragment) BEGIN insert(out.buffer,tdatr.in.tsdu.fragment); END;  til:  FROM d a t a AND o u t . b u f f e r <> n i l TO d a t a 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 remove(out.buffer, dt.out.user.data); END;  tl2:  WHEN d t FROM d a t a TO d a t a AND i n s e r t ( i n . b u f f e r , dt.in.user.data) BEGIN insert(in.buffer, dt.in.user.data); END;  tl3:  FROM d a t a AND i n . b u f f e r <> n i l TO d a t a AND remove(in.buffer,tdati.out.tsdu.fragment) OUT t d a t i BEGIN remove(in.buffer, tdati.out.tsdu.fragment); END;  tl4:  WHEN t d r e q FROM d a t a TO i d l e OUT n d r e q BEGIN ndreq.out.disc.reason:= tdreq.in.ts.user.reason; END;  151  rNFS OF CLASS 0 TRANSPORT PROTOCOL tl5:  tl6:  WHEN n d i n d FROM d a t a TO i d l e OUT t d i n d BEGIN tdind.out.ts.disc.reason END;  WHEN n r i n d FROM d a t a TO i d l e OUT t d i n d BEGIN tdind.out.ts.disc.reason 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:
http://iiif.library.ubc.ca/presentation/dsp.831.1-0064927/manifest

Comment

Related Items