Research Commons
      • Browse 
        • Communities & Collections
        • Titles
        • Authors
        • By Issue Date
        • Subjects
        • Types
        • Series
      • Help 
        • About
        • Collection Policy
        • OA Mandate Guidelines
        • Guidelines FAQ
        • Contact Us
      • My Account 
        • Sign In
        • Register
      View Item 
      •   Research Commons
      • University of Waikato Research
      • Computing and Mathematical Sciences
      • Computing and Mathematical Sciences Papers
      • View Item
      •   Research Commons
      • University of Waikato Research
      • Computing and Mathematical Sciences
      • Computing and Mathematical Sciences Papers
      • View Item
      JavaScript is disabled for your browser. Some features of this site may not work without it.

      Controlling test case explosion in test generation for B formal models: Research Articles

      Legeard, Bruno; Peureux, Fabien; Utting, Mark
      DOI
       10.1002/stvr.v14:2
      Link
       www3.interscience.wiley.com
      Find in your library  
      Citation
      Export citation
      Legeard, B., Peureux, F. & Utting, M.(2004). Controlling test case explosion in test generation for B formal models: Research Articles. Software Testing, Verification & Reliability, 14(2), 81-103.
      Permanent Research Commons link: https://hdl.handle.net/10289/1521
      Abstract
      BZ-TESTING-TOOLS (BZ-TT) is a tool set for automated test case generation from B and Z specifications. BZ-TT uses boundary and cause–effect testing on the basis of the formal model. It has been used and validated on several industrial applications in the domain of critical software, particularly smart card and transport systems. This paper presents the test coverage criteria supported by BZ-TT. On the one hand, these correspond to various classical structural coverage criteria, but specialized to the case of B abstract machines. The paper gives algorithms for these in Prolog. On the other hand, BZ-TT introduces new coverage criteria for complex data structures, based on boundary analysis: this paper defines weak and strong state-boundary coverage, input-boundary coverage and output-boundary coverage. Finally, the paper describes how BZ-TT presents a unified view of these criteria to the validation engineer, and allows him or her to control the test case explosion on a coarse basis (choosing from a range of coverage criteria) as well as a fine basis (selecting options for each state or input variable).
      Date
      2004
      Type
      Journal Article
      Publisher
      John Wiley & Sons, Ltd.
      Collections
      • Computing and Mathematical Sciences Papers [1454]
      Show full item record  

      Usage

       
       
       

      Usage Statistics

      For this itemFor all of Research Commons

      The University of Waikato - Te Whare Wānanga o WaikatoFeedback and RequestsCopyright and Legal Statement