@techreport{TR-IC-09-10,
  number = {IC-09-10},
  author = {Patrick H. S. Brito and Rogério de Lemos and Cecília
                  M. F. Rubira}, 
  title = {Verifying Architectural Variabilities in Software Fault
                  Tolerance Techniques}, 
  month = {March},
  year = {2009}, 
  institution = {Institute of Computing, University of Campinas},
  note = {In English, 15 pages.
    \par\selectlanguage{english}\textbf{Abstract}
      This technical report  considers the representation of different
      software   fault  tolerance   techniques  as   a   product  line
      architecture   (PLA)  for  promoting   the  reuse   of  software
      artefacts, such  as formal specifications  and verification. The
      proposed  PLA enables  to specify  a series  of  closely related
      applications  in  terms  of  a  single  architecture,  which  is
      obtained by identifying  variation points associated with design
      decisions  regarding software  fault tolerance.  These decisions
      are used  to choose the  appropriate technique depending  on the
      features selected for the instance, e.g, the number of redundant
      resources,  or the  type of  adjudicator. The  proposed approach
      also comprises the formalisation  of the PLA, using B-Method and
      CSP,  for  systematising   the  verification  of  fault-tolerant
      software  systems  at the  architectural  level. The  properties
      verified cover two complementary  contexts: the selection of the
      correct architectural  variabilities for instantiating  the PLA,
      and  also   the  properties   of  the  chosen   fault  tolerance
      techniques.
  }
}