This paper describes a methodology for verifying the stability and performance of closed-loop nonlinear systems, as arise in chemical plants with process controllers, when the process model is incompletely known, with uncertainty both in the parameter values and in the form of the equations. A systematic way of generating and summarizing all possible behavior patterns of the system is described. Temporal logic is used to formalize the posing of and automatic answering of qualitative questions about the response of the system. The methodology is demonstrated for controller verification in the design of a CSTR for styrene polymerization.