We present Q Framework: a verification framework used at Sandia National Laboratories. Q is a collection of tools used to verify safety and correctness properties of high-consequence embedded systems and captures the structure and compositionality of system specifications written with state machines in order to prove system-level properties about their implementations. Q consists of two main workflows: 1) compilation of temporal properties and state machine models (such as those made with Stateflow) into SMV models and 2) generation of ACSL specifications for the C code implementation of the state machine models. These together prove a refinement relation between the state machine model and its C code implementation, with proofs of properties checked by NuSMV (for SMV models) and Frama-C (for ACSL specifications).

We present an algorithm to compute the unique maximally permissive state-based supervisor for any deterministic finite labeled transition system subject to a specification with combined invariance and reachability requirements. The specifications that we consider are expressed in computation tree logic and include specifications with multiple reachability requirements, each of which should always be satisfied. The form of the controller (a state-based supervisor) is purely memoryless, so the control decisions can be made by directly sampling the state of the system that is being controlled, without recording any past event or transition history. The algorithm has been implemented in SynthSMV, an extension of the well-known model-checking solver NuSMV, which uses NuSMV's efficient implementation of symbolic model checking (based on binary decision diagrams). A case study that involves coordinating the operation of a set of reactors in a chemical plant shows how the methods that we develop apply in practice.

In this paper, we address the problem of incorporating knowledge of the automation system in a chemical plant into the online scheduling problem. Optimization models for online scheduling necessarily omit some of the plant dynamics to ensure sufficiently fast solution times for use in online rescheduling. This can result in the computed schedules not being feasible when executed in the plant. To overcome this difficulty, we propose to use online analysis of a formal model of the automation logic to detect these infeasible schedules and avoid them when rescheduling. Model checking is applied to an abstraction of the automation system's dynamics to detect infeasible schedules, and a state-space resource task network scheduling model is used to account for the associated delay information. We demonstrate the techniques using an illustrative running example, and show the utility of the integrated approach using a case study involving multiple batch reactions.

We apply discrete-event-control-theoretic techniques for opacity enforcement by insertion or deletion of output events to the problem of location privacy enforcement in an indoor environment where users are continuously monitored by IoT devices. We design an obfuscator of user trajectories in a grid model with obstacles. The obfuscator must preserve a secret (e.g., visits to secret cells of the grid), while at the same time enforce feasibility and utility constraints for obfuscated trajectories. We implement the obfuscator to map the true location of the user to an obfuscated location, in real time, using services provided by a data server called the Global Data Plane which records sensor readings from IoT devices and publishes them to subscribers. We explain how scalability of obfuscator synthesis (off-line) and instantiation (online) is achieved. We demonstrate the approach on a grid with over 1,500 cells modeling the first floor of a university building, where location estimation is achieved using the ALPS Acoustic Location Processing System.

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.

We present an approach to online scheduling of chemical plant operations that incorporates precise knowledge of the dynamics enforced by the automation system. The scheduling problem is solved using a discrete-time state-space resource task network formulation. Rescheduling is triggered when the schedule currently being executed conflicts with the dynamical behavior allowed by the automation system. We present a case study to show that better operation is achieved using our approach compared to iterative rescheduling alone.

We propose an abstraction-based method that can be applied to falsify a class of computation tree logic (CTL) specifications that combine invariance and reachability requirements in terms of the discrete state of a hybrid control system. The fragment of CTL that we address is not expressible in ACTL∗ (which includes LTL). The method involves applying supervisory control to a finite abstraction of the hybrid system to falsify the specification. For the class of systems that we consider, falsification of the specification implies a flaw in the design of the control and automation logic.

In this paper a method for detecting errors in the discrete logic of hybrid systems is applied to chemical plant automation systems. The method relies on the application of supervisory control theory to a discrete abstraction of the hybrid system that models the plant and controller. A set of general operability requirements are also presented that can be applied to any automation system to detect common operability problems. A small example is included to demonstrate the method and its application.

In this paper, we provide a review of Professor Powers's and his students' work on connecting fault analysis, discrete process control, human operating procedures, and symbolic model checking. In recent years, this type of research is placed under the banner of "cyber-physical systems research". Some of the techniques and procedures Powers and his students developed can be found in the open literature and conference proceedings. However, they have not been published broadly due to the untimely passing of Professor Powers. A complete overview of the methods are not available, and the cap-stone results obtained in the two last Ph.D. theses have not been published.

A specification expressed in computation tree logic (CTL) that enforces safety and reachability requirements in discrete event systems is proposed. It is shown that the specification has a unique minimal control strategy that maximizes the set of states that satisfy the specification, and an algorithm is provided to calculate the control strategy. The specification captures the idea that the chemical process should always be able to shut down in a safe manner. The algorithm uses established CTL model checking procedures to perform the intermediate calculations, and can incorporate symbolic model checking. The maximum problem size for which a control strategy can be calculated is similar to that of the corresponding verification problem. A small example demonstrates the application of the algorithm to a problem that includes safety and reachability constraints. Current work aims to use the techniques to solve a real process control problem supplied by industry.

A new approach for flare monitoring is proposed so that flare combustion efficiency can be predicted online in industrial plants. Multivariate image analysis (MIA), which is based on principal component analysis (PCA) and projection to latent structures (PLS), has been applied to flare combustion systems in order to predict their resulting combustion efficiencies, as a function of the crosswind velocity, using simulated results, and as a function of steam or air flow rates, using experimental tests of a full-size flare. The results show that a multivariate regression model based on flare color images can be used to predict the flare performance over a range of operating conditions for steam-assisted flares. Therefore, simple two-dimensional color images of industrial flares may be a fast, accurate, and inexpensive approach for online monitoring of these industrial combustion systems. This would allow for developing effective flare control and mitigation strategies.