In this paper, we apply formal verification and falsification of temporal logic specifications to analyze chemical plant automation systems. We present new results, obtained by applying a recently-developed approach to handle combined invariance and reachability requirements. In addition, we develop a set of tests that can be generated automatically for a given control system, some of which have the same form as those in the existing literature, and some of which combine invariance and reachability, to which we apply the new approach mentioned previously. In both cases, we work with abstractions of the automation systems in order to apply symbolic model checking to industrial-scale problems. We demonstrate the results using a series of small illustrative examples, and also report results from an industrial case study. The methods that we apply are implemented in a pair of open-source software tools, which we describe briefly. (C) 2017 Elsevier Ltd. All rights reserved.