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.

      Automated Boundary Testing from Z and B

      Legeard, Bruno; Peureux, Fabien; Utting, Mark
      DOI
       10.1007/3-540-45614-7_2
      Link
       www.springerlink.com
      Find in your library  
      Citation
      Export citation
      Legeard, B., Peureux, F. & Utting, M.(2002). Automated boundary testing from Z and B. In Proceeding of International Symposium of Formal Methods Europe Copenhagen, Denmark, July 22-24, 2002(pp. 221-236). Berlin: Springer.
      Permanent Research Commons link: https://hdl.handle.net/10289/1523
      Abstract
      We present a method for black-box boundary testing from B and Z formal specifications. The basis of the method is to test every operation of the system at every boundary state using all input boundary values of that operation. The test generation process is highly automated. It starts by calculating boundary goals from Pre/Post predicates derived from the formal model. Then each boundary goal is instantiated to a reachable boundary state, by searching for a sequence of operations that reaches the boundary goal from the initial state. This process makes intensive use of a set-oriented constraint technology, both for boundary computation and to traverse the state space. The method was designed on the basis of industrial applications in the domain of critical software (Smart card and transportation). Application results show the effectiveness and the scalability of the method. In this paper, we give an overview of the method and focus on the calculation of the boundary goals and states.
      Date
      2002
      Type
      Conference Contribution
      Publisher
      Springer
      Collections
      • Computing and Mathematical Sciences Papers [1455]
      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