We modeled and tested an embedded controller that will be incorporated into a medical process control application. The controller (including customized software) was developed by others, and its original documentation does not include a functional speci cation that is su ciently complete and accurate for our needs. We proposed a functional speci cation of certain important controller behaviors, based on the available documentation and behavior that we had observed. We used Petri nets for our speci cation notation. From the Petri net, we derived a series of tests intended to reveal whether our provisional speci cation accurately characterized controller behavior. The method for deriving the tests from the Petri net is described. The tests systematically traverse the Petri net and also present faults that should be handled in a reasonable way. Performing the tests revealed several errors in our initial speci cation. We modi ed our speci cation until it was consistent with all observed behaviors, covering a wide range of situations. Department of Computer Science and Engineering, FR-35, University of Washington, Seattle WA 98195. Supported in part by National Institutes of Health grant number LM04174 from the National Library of Medicine
分享
引用
