Using Formal Models to Plan Control System Testing

Jonathan Jacky, Alexandra Barke and Ruedi Risler

February, 1991


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 specification that is sufficiently complete and accurate for our needs. We proposed a functional specification of certain important controller behaviors, based on the available documentation and behavior that we had observed. We used Petri nets for our specification notation. From the Petri net, we derived a series of tests intended to reveal whether our provisional specification 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 specification. We modified our specification until it was consistent with all observed behaviors, covering a wide range of situations.

Download (19 pages): PDF (200 kb)