Announcements
Center for Information Protection
UC Davis is planning to join the NSF I/UCRC
Center for Information Protection. We are looking
for companies to join our Industrial Advisory
Board.
Find out more here!
Conferences and Workshops
- ISGIG 2009
- ACSAC 25
- PETRA 2010 (due 11/15)
- Oakland 2010 (due 11/18)
My Links
- My Home Page
- Books
- Classes
- Papers
- Reports and Notes
- Research
- Security in Programming
- Service
- Students
- Talks
- Miscellaneous
- My Family
- About Me (CV and such)
Other Links
- MyUCDavis
- Computer Security Lab
- Dept. of Computer Science
- College of Engineering
- University of California, Davis
- City of Davis
- County of Yolo
- State of California
- United States of America
An Interface Language Between Specification and Testing
Citation
- G. Fink, M. Helmke, M. Bishop, and K. Levitt, “An Interface Language Between Specification and Testing”, Technical Report CSE-95-15, Dept. of Computer Science, University of California at Davis, Davis, CA 95616-8562 (Aug. 1995).
Paper
About This Report
From the introduction:Specifications describe models that programs are supposed to implement. Testing is used to verify if a program’s implementation is correct. Specification languages such as Z don’t provide ways to relate this model to a program state. Alternatively, the program couuld be developed independent of the specification, so there is no natural correspondence between specification and code.
In this paper, we present a new specification language TASPEC which can serve as an intermediary between a Z specification and the testing process. TASPEC can express close correspondences between code and abstract semantics. Large portions of Z are shown to be semi-automatically translatable into TASPEC. Test oracles and other testing artifacts can be derived from TASPEC specifications. As an example, a recently discovered flaw in an implementation of the TCP protocol is uncovered using this technique.
