View in EDS HTML Full Text PDF Full Text

Sound and mechanised compositional verification of input-output conformance.

Saved in:
Bibliographic Details
Title: Sound and mechanised compositional verification of input-output conformance.
Authors: Sampaio, Augusto1, Nogueira, Sidney1,2, Mota, Alexandre1, Isobe, Yoshinao3
Source: Software Testing: Verification & Reliability. Jun2014, Vol. 24 Issue 4, p289-319. 31p.
Subjects: CSP (Computer program language), Computer software testing, Motorola Inc., Mobile apps, Conformance testing, Algebra
Abstract: SUMMARY This paper mechanises conformance verification in the setting of the CSP process algebra. The verification strategy is captured by a theorem stated as a process refinement expression, which can be verified by a model checker such as FDR. The conformance relation, cspio, distinguishes input and output events. The process algebraic framework of CSP is used to address compositional conformance verification by establishing compositionality properties for cspio with respect to the CSP operators. Although cspio has been defined in the standard CSP traces model, one can address quiescence situations using a special output event, in which case it is formally established that cspio is equivalent to Tretmans ioco. All the results have been mechanically proved using the CSP-Prover. The proposed testing theory has been adopted in an industrial context involving collaboration with Motorola, on testing mobile applications. Several examples and a case study are presented to illustrate the overall approach. Copyright © 2013 John Wiley & Sons, Ltd. [ABSTRACT FROM AUTHOR]
Copyright of Software Testing: Verification & Reliability is the property of Wiley-Blackwell and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
Full text is not displayed to guests.
FullText Links:
  – Type: pdflink
Text:
  Availability: 1
Header DbId: egs
DbLabel: Engineering Source
An: 95876786
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Sound and mechanised compositional verification of input-output conformance.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Sampaio%2C+Augusto%22">Sampaio, Augusto</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22Nogueira%2C+Sidney%22">Nogueira, Sidney</searchLink><relatesTo>1,2</relatesTo><br /><searchLink fieldCode="AR" term="%22Mota%2C+Alexandre%22">Mota, Alexandre</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22Isobe%2C+Yoshinao%22">Isobe, Yoshinao</searchLink><relatesTo>3</relatesTo>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Software+Testing%3A+Verification+%26+Reliability%22">Software Testing: Verification & Reliability</searchLink>. Jun2014, Vol. 24 Issue 4, p289-319. 31p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22CSP+%28Computer+program+language%29%22">CSP (Computer program language)</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+software+testing%22">Computer software testing</searchLink><br /><searchLink fieldCode="DE" term="%22Motorola+Inc%2E%22">Motorola Inc.</searchLink><br /><searchLink fieldCode="DE" term="%22Mobile+apps%22">Mobile apps</searchLink><br /><searchLink fieldCode="DE" term="%22Conformance+testing%22">Conformance testing</searchLink><br /><searchLink fieldCode="DE" term="%22Algebra%22">Algebra</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: SUMMARY This paper mechanises conformance verification in the setting of the CSP process algebra. The verification strategy is captured by a theorem stated as a process refinement expression, which can be verified by a model checker such as FDR. The conformance relation, cspio, distinguishes input and output events. The process algebraic framework of CSP is used to address compositional conformance verification by establishing compositionality properties for cspio with respect to the CSP operators. Although cspio has been defined in the standard CSP traces model, one can address quiescence situations using a special output event, in which case it is formally established that cspio is equivalent to Tretmans ioco. All the results have been mechanically proved using the CSP-Prover. The proposed testing theory has been adopted in an industrial context involving collaboration with Motorola, on testing mobile applications. Several examples and a case study are presented to illustrate the overall approach. Copyright © 2013 John Wiley & Sons, Ltd. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Software Testing: Verification & Reliability is the property of Wiley-Blackwell and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=95876786
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1002/stvr.1498
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 31
        StartPage: 289
    Subjects:
      – SubjectFull: CSP (Computer program language)
        Type: general
      – SubjectFull: Computer software testing
        Type: general
      – SubjectFull: Motorola Inc.
        Type: general
      – SubjectFull: Mobile apps
        Type: general
      – SubjectFull: Conformance testing
        Type: general
      – SubjectFull: Algebra
        Type: general
    Titles:
      – TitleFull: Sound and mechanised compositional verification of input-output conformance.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Sampaio, Augusto
      – PersonEntity:
          Name:
            NameFull: Nogueira, Sidney
      – PersonEntity:
          Name:
            NameFull: Mota, Alexandre
      – PersonEntity:
          Name:
            NameFull: Isobe, Yoshinao
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 06
              Text: Jun2014
              Type: published
              Y: 2014
          Identifiers:
            – Type: issn-print
              Value: 09600833
          Numbering:
            – Type: volume
              Value: 24
            – Type: issue
              Value: 4
          Titles:
            – TitleFull: Software Testing: Verification & Reliability
              Type: main
ResultId 1