loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Eighth Asian Test Symposium (ATS'99)
An Approach to Testing the Nonexistence of Initial State in Z Specifications
Shanghai, China
November 16-November 18
ISBN: 0-7695-0315-2
Huaikou Miao, Shanghai University
Xiaolei Gao, Shanghai University
Ling Liu, Shanghai University
Formal methods use a mathematically based notation to describe the specification of software system and, based on these they have a notation of an implementation satisfying a specification. Z notation has been widely used in academia and industry. One of the things that we have either to prove formally or to convince ourselves of in some other way, about every specification written in Z is that the initial state exists. This paper explores theoretically the test of initial states in Z specifications. The new concepts, constructed function and constrained states space are introduced. The testing approach proposed in this paper can be used to detect the erroneous initial state in Z specifications. By way of examples, the application of testing approach is given. Keywords: Z specifications, states space, constructed function, constrained states space.
Citation:
Huaikou Miao, Xiaolei Gao, Ling Liu, "An Approach to Testing the Nonexistence of Initial State in Z Specifications," ats, pp.289, Eighth Asian Test Symposium (ATS'99), 1999
Usage of this product signifies your acceptance of the Terms of Use.