TY - GEN
T1 - Augmenting sequence constraints in Z and its application to testing
AU - Tsai, W. T.
AU - Agarwal, V.
AU - Huang, B.
AU - Paul, R.
N1 - Publisher Copyright:
© 2000 IEEE.
PY - 2000
Y1 - 2000
N2 - The paper introduces sequence constraints into a formal specification language Z. Formal specification languages have been used to specify safety-critical applications, and many static and dynamic aspects of the system can be specified. However, the method calling constraints, a runtime behavior, are often missed. The paper introduces two kinds of sequence constraints: those constraints with respect to a schema and those with respect to multiple schemas. Once sequence constraints are specified, together with parameter specifications already in Z, one can generate test cases including test inputs and their expected outputs using various testing strategies such as partition testing, boundary testing, random testing, stress testing, and negative testing. An application has been specified in Z using sequence constraints, and test cases generated have been used to test the software. The results show that the test cases generated successfully detected all the faults seeded.
AB - The paper introduces sequence constraints into a formal specification language Z. Formal specification languages have been used to specify safety-critical applications, and many static and dynamic aspects of the system can be specified. However, the method calling constraints, a runtime behavior, are often missed. The paper introduces two kinds of sequence constraints: those constraints with respect to a schema and those with respect to multiple schemas. Once sequence constraints are specified, together with parameter specifications already in Z, one can generate test cases including test inputs and their expected outputs using various testing strategies such as partition testing, boundary testing, random testing, stress testing, and negative testing. An application has been specified in Z using sequence constraints, and test cases generated have been used to test the software. The results show that the test cases generated successfully detected all the faults seeded.
KW - Application software
KW - Computer science
KW - Electrical capacitance tomography
KW - Formal specifications
KW - Mission critical systems
KW - Runtime
KW - Safety
KW - Specification languages
KW - Stress
KW - Testing
UR - https://www.scopus.com/pages/publications/0006697799
U2 - 10.1109/ASSET.2000.888030
DO - 10.1109/ASSET.2000.888030
M3 - 会议稿件
AN - SCOPUS:0006697799
T3 - Proceedings - 3rd IEEE Symposium on Application-Specific Systems and Software Engineering Technology
SP - 41
EP - 48
BT - Proceedings - 3rd IEEE Symposium on Application-Specific Systems and Software Engineering Technology
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 3rd IEEE Symposium on Application-Specific Systems and Software Engineering Technology, ASSET 2000
Y2 - 24 March 2000 through 25 March 2000
ER -