@phdthesis{johnson2013phdthesis,
    author      =   {Taylor T. Johnson},
    title       =   {Uniform Verification of Safety for Parameterized Networks of Hybrid Automata},
    school      =   {Department of Electrical and Computer Engineering, University of Illinois at Urbana-Champaign},
    address     =   {Urbana, IL 61801, USA},
    month       =   aug,
    year        =   2013,
    gsid        =   {},
    abstract    =   {Distributed cyber-physical systems (CPS) incorporate communicating agents with their own cyber and physical states and transitions. Such systems are typically designed to accomplish tasks in the physical world. For example, the objective of a robotic swarm may be to cover an area while avoiding collisions. The combination of physical dynamics, software dynamics, and communications leads these systems naturally to be modeled as networks of hybrid automata. Hybrid automata are finite-state machines with additional real-valued continuous variables whose dynamics may vary in different states. These networks are naturally parameterized on the number of participants---processes, robots, vehicles, etc. The uniform verification problem is to verify (prove) some property regardless of the number of participants. In this dissertation, we develop a framework for formally modeling and automatically verifying networks composed of arbitrarily many participants. Three methods are presented and evaluated for proving safety properties---those that always hold throughout the evolutions of the system.
                The first method is a backward search from the set of unsafe states, which are those that violate a desired safety property. The method computes the set of reachable states for a parameterized network, and checks that the intersection of the reachable states and unsafe states is empty. We apply this technique using the Model Checker Modulo Theories (MCMT) verification tool to automatically verify safe separation of aircraft in a conceptual air traffic landing protocol of the Small Aircraft Transportation System (SATS), regardless of the number of aircraft involved in the protocol.
                The Passel verification tool we develop as a part of this dissertation implements the next two methods and can verify safety properties of parameterized networks of hybrid automata with dynamics specified as rectangular differential inclusions. The second method computes the set of reachable states for networks composed of a finite number of participants. While this method cannot in general prove safety regardless of the number of participants, it can be used as a subroutine for other methods, such as synthesizing candidate inductive invariants to perform uniform verification. It is also useful on its own as an initial sanity check prior to attempting to prove properties regardless of the number of participants, which is harder in general---in terms of decidability and complexity.
                The third method---when it is successful---automates the traditionally deductive verification approach of proving inductive invariants. This is accomplished by combining model checking with theorem proving. An algorithm synthesizes candidate inductive invariants by computing the reachable states of finite instantiations. The conditions for inductive invariance are then checked for these candidates. If a small model theorem applies, finite instantiations of the parameterized network can be checked, but in general, a theorem prover is queried.  In this case, the inductive invariance conditions are encoded as satisfiability checks, for which it may be possible to discharge automatically.  When these steps are successful, a fully automatic verification of safety is achieved.
                The main contributions of this thesis include (a) the modeling framework for parameterized networks of hybrid automata, (b) the first fully automatic uniform verification of parameterized networks composed of hybrid automata with rectangular dynamics, such as Fischer's mutual exclusion protocol and SATS, (c) formalization of the SATS case study as a uniform verification problem, (d) the Passel verification tool, (e) an extension of the invisible invariants and split invariants approaches for invariant synthesis to networks of hybrid automata, and (f) a small model theorem for checking inductive invariance conditions of networks of rectangular hybrid automata.},
    comment     =   {<a href="https://www.ideals.illinois.edu/handle/2142/46679">doi</a>},
    pdf = {http://www.taylortjohnson.com/research/johnson2013phdthesis.pdf},
    software = {https://publish.illinois.edu/passel-tool/},
}