@STRING{hp_TaylorT.Johnson="http://www.taylortjohnson.com/"}
@STRING{hp_SayanMitra="http://users.crhc.illinois.edu/mitras/"}
@STRING{hp_ParasaraSridharDuggirala="http://www.cs.illinois.edu\~duggira3/"}
@STRING{hp_SairajDhople="http://www.ece.umn.edu\~sdhople/"}
@STRING{hp_SergiyBogomolov="http://www.sergiybogomolov.com/"}
@STRING{hp_AlexandreDonze="http://www.eecs.berkeley.edu\~donze/"}
@STRING{hp_GoranFrehse="https://sites.google.com/site/frehseg/"}
@STRING{hp_RaduGrosu="http://ti.tuwien.ac.at/cps/people/grosu"}
@STRING{hp_AndreasPodelski="http://www.informatik.uni-freiburg.de\~podelski/"}
@STRING{hp_MartinWehrle="http://ai.cs.unibas.ch/people/mwehrle/"}
@STRING{hp_CedricLangbort="http://aerospace.illinois.edu/directory/profile/langbort"}
@STRING{hp_MarcoCaccamo="http://pertsserver.cs.uiuc.edu\~mcaccamo/"}
@STRING{hp_LuiSha="http://publish.illinois.edu/cpsintegrationlab/people/lui-sha/"}
@STRING{hp_StanleyBak="http://stanleybak.com/"}
@STRING{hp_LeonardoBobadilla="http://users.cis.fiu.edu\~jabobadi/"}
@STRING{hp_AmyLaViers="http://www.amylaviers.com"}
@STRING{hp_SebastianFischmeister="https://uwaterloo.ca/embedded-software-group/people-profiles/sebastian-fischmeister"}
@STRING{hp_ChristianSchilling="http://swt.informatik.uni-freiburg.de/staff/christian_schilling"}
@article{johnson2016tecs,
Title = {Real-Time Reachability for Verified Simplex Design},
Author = {Taylor T. Johnson and Stanley Bak and Marco Caccamo and Lui Sha},
journal = {ACM Transactions on Embedded Computing Systems (TECS)},
pdf = {http://www.taylortjohnson.com/research/johnson2015tecs.pdf},
Owner = {tjohnson},
Timestamp = {2014.07.21},
volume = {15},
number = {2},
month = feb,
year = {2016},
issn = {1539-9087},
pages = {26:1--26:27},
articleno = {26},
numpages = {27},
doi = {10.1145/2723871},
acmid = {2723871},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Formal verification, cyber-physical systems, hybrid systems},
}
@InProceedings{bak2016hscc,
author = {Stanley Bak and Sergiy Bogomolov and Thomas A. Henzinger and Taylor T. Johnson and Pradyot Prakash},
title = {Scalable Static Hybridization Methods for Analysis of Nonlinear Systems},
booktitle = {19th Intl. Conf. on Hybrid Systems: Computation and Control (HSCC 2016)},
year = {2016},
month = apr,
publisher = {ACM},
owner = {tjohnson}
}
@patent{hoefel2015patent,
author = {Albert Hoefel and Bernard, Francois and Harms, Kent David and Ramshaw, Sylvain and Darayan, Shayan and Taylor T. Johnson},
title = {Control of a component of a downhole tool},
year = {2015},
month = dec,
day = {29},
number = {US 9222352},
type = {Patent},
version = {},
location = {US},
comment = {DOI},
pdf = {http://www.taylortjohnson.com/research/hoefel2015patent.pdf},
filing_num = {61415006},
yearfiled = {2010},
monthfiled = nov,
dayfiled = {18},
abstract = {}
}
@inproceedings{nguyen2015cfv,
author = {Luan Viet Nguyen and Djordje Maksimovic and Taylor T. Johnson and Andreas Veneris},
title = {Quantified Bounded Model Checking for Rectangular Hybrid Automata},
year = {2015},
month = nov,
Booktitle = {9th International Workshop on Constraints in Formal Verification (CFV 2015)},
address = {Austin, Texas},
pdf = {http://www.taylortjohnson.com/research/nguyen2015cfv.pdf},
}
@InProceedings{bak2015rtss,
Title = {Periodically-Scheduled Controller Analysis using Hybrid Systems Reachability and Continuization},
Author = {Stanley Bak and Taylor T. Johnson},
Booktitle = {36th IEEE Real-Time Systems Symposium (RTSS 2015)},
Year = {2015},
Address = {San Antonio, Texas},
Month = dec,
Publisher = {IEEE Computer Society},
pdf = {http://www.taylortjohnson.com/research/bak2015rtss.pdf},
}
@inproceedings{nguyen2015rv,
author = {Luan Viet Nguyen and Christian Schilling and Sergiy Bogomolov and Taylor T. Johnson},
title = {Runtime Verification of Model-based Development Environments},
year = {2015},
month = sep,
Booktitle = {15th International Conference on Runtime Verification (RV 2015)},
address = {Vienna, Austria},
pdf = {http://www.taylortjohnson.com/research/nguyen2015rv.pdf},
}
@article{bogomolov2015sttt,
author = {Sergiy Bogomolov and Alexandre Donze and Goran Frehse and Radu Grosu and Taylor T. Johnson and Hamed Ladan and Andreas Podelski and Martin Wehrle},
title = {Guided Search for Hybrid Systems Based on Coarse-Grained Space Abstractions},
year = {2015},
journal = {Software Tools for Technology Transfer (STTT)},
publisher = {Springer},
address = {},
month = aug,
pages = {},
doi = {10.1007/s10009-015-0393-y},
gsid = {4980588848043524788},
abstract = {},
software = {http://www2.informatik.uni-freiburg.de{\~}bogom/sttt2015/},
pdf = {http://www.taylortjohnson.com/research/bogomolov2015sttt.pdf}
}
@inproceedings{bak2015snr,
author = {Stanley Bak and Sergiy Bogomolov and Taylor T. Johnson},
title = {HyST: A Source Transformation and Translation Tool for Hybrid Automaton Models},
year = {2015},
month = jul,
Booktitle = {1st International Workshop on Symbolic and Numerical Methods for Reachability Analysis
(SNR 2015), Co-Located with the 27th International Conference on Computer Aided Verification (CAV 2015)},
address = {San Francisco, California},
pdf = {http://www.taylortjohnson.com/research/bak2015snr.pdf},
}
@inproceedings{johnson2015esv,
Author = {Taylor T. Johnson and Raghunath Gannamaraju and Sebastian Fischmeister},
Title = {A Survey of Electrical and Electronic (E/E) Notifications for Motor Vehicles},
Year = {2015},
Booktitle = {24th NHTSA International Technical Conference on the Enhanced Safety of Vehicles (ESV)},
address = {Gothenburg, Sweden},
month = jun,
Pages = {1--15},
doi = {},
gsid = {},
abstract = {},
comment = {publisher PDF},
pdf = {http://www.taylortjohnson.com/research/johnson2015esv.pdf},
}
@InProceedings{johnson2015iccps,
Title = {Cyber-Physical Specification Mismatch Identification with Dynamic Analysis},
Author = {Taylor T. Johnson and Stanley Bak and Steven Drager},
Booktitle = {6th International Conference on Cyber-Physical Systems (ICCPS 2015)},
Year = {2015},
Address = {Seattle, Washington},
Month = apr,
Publisher = {ACM/IEEE},
comment = {Hynger software tool},
software = {http://verivital.com/hynger/},
pdf = {http://www.taylortjohnson.com/research/johnson2015iccps.pdf},
Owner = {tjohnson},
Timestamp = {2014.12.23}
}
@InProceedings{bak2015hscc,
Title = {{HyST}: A Source Transformation and Translation Tool for Hybrid Automaton Models},
Author = {Stanley Bak and Sergiy Bogomolov and Taylor T. Johnson},
Booktitle = {18th International Conference on Hybrid Systems: Computation and Control (HSCC 2015)},
Year = {2015},
Address = {Seattle, Washington},
Month = apr,
Publisher = {ACM},
comment = {Hyst software tool},
pdf = {http://www.taylortjohnson.com/research/bak2015hscc.pdf},
software = {http://verivital.com/hyst/},
Owner = {tjohnson},
Timestamp = {2014.12.20}
}
@misc{nguyen2015hscc,
author = {Luan Viet Nguyen and Christian Schilling and Sergiy Bogomolov and Taylor T. Johnson},
title = {HyRG: a random generation tool for affine hybrid automata},
note = {Presented at 18th International Conference on Hybrid Systems: Computation and Control (HSCC 2015) Poster/Demo Session},
year = {2015},
gsid = {15770939070662677354},
month = apr,
doi = {10.1145/2728606.2728650},
pdf = {http://www.taylortjohnson.com/research/nguyen2015hscc.pdf},
software = {http://www.verivital.com/hyrg/},
comment = {HyRG Software Tool},
}
@inproceedings{tran2015arch,
author = {Hoang-Dung Tran and Luan Viet Nguyen and Taylor T. Johnson},
title = {Benchmark: A Nonlinear Reachability Analysis Test Set from Numerical Analysis},
year = {2015},
booktitle = {Applied Verification for Continuous and Hybrid Systems Workshop (ARCH 2015)},
address = {Seattle, Washington},
month = apr,
pages = {},
doi = {},
gsid = {},
abstract = {},
comment = {model source code},
pdf = {http://www.taylortjohnson.com/research/tran2015arch.pdf},
}
@inproceedings{bak2015arch,
author = {Stanley Bak and Sergiy Bogomolov and Marius Greitschus and Taylor T. Johnson},
title = {Benchmark Generator for Stratified Controllers of Tank Networks},
year = {2015},
booktitle = {Applied Verification for Continuous and Hybrid Systems Workshop (ARCH 2015)},
address = {Seattle, Washington},
month = apr,
pages = {},
doi = {},
gsid = {},
abstract = {},
comment = {model source code},
pdf = {http://www.taylortjohnson.com/research/bak2015arch.pdf},
}
@InProceedings{bobadilla2015scitech,
Title = {Verified Planar Formation Control Algorithms by Composition of Primitives},
Author = {Leonardo Bobadilla and Taylor T. Johnson and Amy LaViers and Umer Huzaifa},
Booktitle = {AIAA SciTech},
Year = {2015},
Address = {Kissimmee, Florida},
Month = jan,
Publisher = {AIAA},
Owner = {tjohnson},
Timestamp = {2014.08.22},
pdf = {http://www.taylortjohnson.com/research/bobadilla2015scitech.pdf},
}
@article{nguyen2014tec,
author = {Luan Viet Nguyen and Hoang-Dung Tran and Taylor T. Johnson},
title = {Virtual Prototyping for Distributed Control of a Fault-Tolerant Modular Multilevel Inverter for Photovoltaics},
year = {2014},
journal = {IEEE Transactions on Energy Conversion},
address = {},
month = dec,
volume = {29},
issue = {4},
pages = {841--850},
doi = {10.1109/TEC.2014.2362716},
gsid = {},
abstract = {In this paper, we present virtual prototyping of the distributed control for a modular multilevel inverter used as a grid-tie interface for photovoltaics. Due to the distributed control and inherent redundancy in the system composed of many panels and inverter modules, the system topology exhibits fault-tolerance capabilities that we study through virtual prototyping. The fault-tolerance is enabled by several distributed algorithms, such as services to identify which, if any, agents controlling inverter modules have failed. A distributed identifier algorithm allows the system to keep track of the number of operating panels to appropriately regulate the dc voltage output of the panels using buck–boost converters and determine appropriate switching times for H-bridges in the grid-tie. We evaluate the distributed inverter, its control strategy, and fault-tolerance through thousands of simulation scenarios in Mathworks Simulink/Stateflow. Our virtual prototyping framework allows for generating multilevel inverters composed of many inverter modules, and we evaluate inverters composed of five to dozens of inverter modules. Our analysis suggests the achievable total harmonic distortion of the modular multilevel inverter may allow for operating solar arrays in spite of failures of the power electronics, control software, and other subcomponents.},
comment = {arxiv preprint},
pdf = {http://www.taylortjohnson.com/research/nguyen2014tec.pdf},
}
@InProceedings{bak2014rtss,
Title = {Real-Time Reachability for Verified Simplex Design},
Author = {Stanley Bak and Taylor T. Johnson and Marco Caccamo and Lui Sha},
Booktitle = {35th IEEE Real-Time Systems Symposium (RTSS 2014)},
Year = {2014},
Address = {Rome, Italy},
Month = dec,
Publisher = {IEEE Computer Society},
pdf = {http://www.taylortjohnson.com/research/bak2014rtss.pdf},
slides = {http://www.taylortjohnson.com/research/slides/bak2014rtss_slides.pdf},
Owner = {tjohnson},
Timestamp = {2014.07.21}
}
@inproceedings{johnson2014formats,
author = {Taylor T. Johnson and Sayan Mitra},
title = {Anonymized Reachability of Hybrid Automata Networks},
year = {2014},
booktitle = {Proceedings of the 12th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2014)},
address = {Florence, Italy},
month = sep,
pages = {},
doi = {10.1007/978-3-319-10512-3_10},
gsid = {},
abstract = {In this paper, we present a method for computing the set of reachable states for networks consisting of the parallel composition of a finite number of the same hybrid automaton template with rectangular dynamics. The method utilizes a symmetric representation of the set of reachable states (modulo the automata indices) that we call anonymized states, which makes it scalable. Rather than explicitly enumerating each automaton index in formulas representing sets of states, the anonymized representation encodes only: (a) the classes of automata, which are the states of automata represented with formulas over symbolic indices, and (b) the number of automata in each of the classes. We present an algorithm for overapproximating the reachable states by computing state transitions in this anonymized representation. Unlike symmetry reduction techniques used in finite state models, the timed transition of a network composed of hybrid automata causes the continuous variables of all the automata to evolve simultaneously. The anonymized representation is amenable to both reducing the discrete and continuous complexity. We evaluate a prototype implementation of the representation and reachability algorithm in our satisfiability modulo theories (SMT)-based tool, Passel. Our experimental results are promising, and generally allow for scaling to networks composed of tens of automata, and in some instances, hundreds (or more) of automata.},
pdf = {http://www.taylortjohnson.com/research/johnson2014formats.pdf},
}
@inproceedings{nguyen2014arch,
author = {Luan Viet Nguyen and Taylor T. Johnson},
title = {Benchmark: DC-to-DC Switched-Mode Power Converters (Buck Converters, Boost Converters, and Buck-Boost Converters)},
year = {2014},
booktitle = {Applied Verification for Continuous and Hybrid Systems Workshop (ARCH 2014)},
address = {Berlin, Germany},
month = apr,
pages = {},
doi = {},
gsid = {},
abstract = {Power electronics represent a large and important class of hybrid systems, as modern digital computers and many other systems rely on their correct operation. In this benchmark description, we model three DC-to-DC switched-mode power converters as hybrid automata with continuous dynamics specified by linear ordinary differential equations. A DC-to-DC converter transforms a DC source voltage from one voltage level to another utilizing switches toggled at some (typically kilohertz) frequency with some duty cycle. The state of this switch gives rise to the locations of the hybrid automaton, and the continuous variables are currents and voltages. The main contributions of this benchmark description are (a) unified modeling these three types of converters as a single hybrid automaton with two locations where the different converters are realized simply by using an appropriate system matrix and input vector, and (b) a basic benchmark generator that allows for simulation of these converters in Simulink/Stateflow and reachability analysis in SpaceEx.},
pdf = {http://www.taylortjohnson.com/research/nguyen2014arch.pdf},
software = {http://www.taylortjohnson.com/research/nguyen2014arch.zip},
}
@inproceedings{nguyen2014cyphy,
author = {Luan Viet Nguyen and Eric Nelson and Amol Vengurlekar and Ruoshi Zhang and Kristopher I White and Victor Salinas and Taylor T. Johnson},
title = {Model-Based Design and Analysis of a Reconfigurable Continuous-Culture Bioreactor (Work-in-Progress)},
year = {2014},
booktitle = {Fourth ACM Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems (CyPhy 2014)},
address = {Berlin, Germany},
month = apr,
pages = {},
doi = {10.1145/2593458.2593469},
gsid = {},
abstract = {In this paper, we present the model-based design and analysis of prototype laboratory equipment used for growing bacteria under precisely controlled conditions for systems biology experiments. Continuous-culture bioreactors grow microorganisms continuously over periods as long as several months. Depending on the particular experiment, the reconfigurable continuous-culture bioreactor we model and analyze may operate as: (a) a chemostat with constant volume, (b) a turbidostat with constant bacterial concentration as observed through turbidity (optical density), or (c) a morbidostat with constant death-rate of bacteria. Such systems have interesting safety specifications such as not overflowing beakers, maintaining constant bacterial concentrations, etc., that must be maintained over long experimental periods. We develop preliminary controller and plant models and analyze them through simulation in Simulink/Stateflow (SLSF), and using reachability analysis in SpaceEx by translating the SLSF models to hybrid automata. The analysis indicates that the proposed controller and model satisfies its regulation specifications and avoids an error scenario encountered in experiments with a prior design (overflowing of beakers).},
comment = {ACM Authorizer},
pdf = {http://www.taylortjohnson.com/research/nguyen2014cyphy.pdf},
}
@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 = {doi},
pdf = {http://www.taylortjohnson.com/research/johnson2013phdthesis.pdf},
software = {https://publish.illinois.edu/passel-tool/},
}
@inproceedings{johnson2013infotech,
author = {Taylor T. Johnson and Sayan Mitra},
title = {Invariant Synthesis for Verification of Parameterized Cyber-Physical Systems with Applications to Aerospace Systems},
year = {2013},
booktitle = {Proceedings of the AIAA Infotech at Aerospace Conference (AIAA Infotech 2013)},
address = {Boston, MA},
month = aug,
isbn = {},
volume = {},
gsid = {},
editor = {},
doi = {10.2514/6.2013-4811},
publisher = {AIAA},
pages = {},
abstract = {In this paper, we describe a method for synthesizing inductive invariants for cyber-physical aerospace systems that are parameterized on the number of participants, such as the number of aircraft involved in a coordinated maneuver. The methodology is useful for automating the traditionally manual process of deductive verification of safety properties, such as collision avoidance, and establishes such properties regardless of the number of participants involved in a protocol. We illustrate the methodology using a simplified model of the landing protocol of the Small Aircraft Transportation System (SATS) as a case study. Each participant (aircraft) in the protocol is modeled as a hybrid automaton with both discrete and continuous states and potentially nondeterministic evolution thereof. Discrete states change instantaneously according to transitions and continuous states evolve according to rectangular differential inclusions. The invariant synthesis method enables a fully automatic verification of the main safety property of SATS, namely, safe separation of aircraft on approach to the runway. The method is implemented in a prototype verification tool called Passel. We present promising experimental results using the methodology, which has enabled a fully automatic proof of safe separation for the model of SATS.},
pdf = {http://www.taylortjohnson.com/research/johnson2013infotech.pdf},
}
@inproceedings{bogomolov2013spin,
author = {Sergiy Bogomolov and Alexandre Donze and Goran Frehse and Radu Grosu and Taylor T. Johnson and Hamed Ladan and Andreas Podelski and Martin Wehrle},
title = {Abstraction-Based Guided Search for Hybrid Systems},
year = {2013},
booktitle = {Proceedings of the 20th International SPIN Symposium on Model Checking of Software (SPIN 2013)},
address = {Stony Brook, New York, USA},
month = jul,
pages = {},
doi = {10.1007/978-3-642-39176-7_8},
gsid = {9142077756418010202},
abstract = {Hybrid systems represent an important and powerful formalism for modeling real-world applications that require both discrete and continuous behavior. A verification tool such as SpaceEx is based on the exploration of a symbolic search space (the region space). As a verification tool, it is typically optimized towards proving the absence of errors. In some settings, e.g., when the verification tool is employed in a feedback-directed design cycle, one would like to have the option to call a version that is optimized towards finding an error path in the region space. A recent approach in this direction is based on guided search. Guided search relies on a cost function that indicates which states are promising to be explored, and preferably explores more promising states first. In this paper, we introduce an abstraction-based cost function based on pattern databases for guiding the reachability analysis. For this purpose, we introduce a suitable abstraction technique that exploits the flexible granularity of modern reachability analysis algorithms. Our cost function is an effective extension of pattern database approaches that have been successfully applied in other areas. We have implemented our approach in the SpaceEx model checker. Our evaluation shows its practical potential.},
pdf = {http://www.taylortjohnson.com/research/bogomolov2013spin.pdf},
}
@inproceedings{hossain2013peci,
author = {Shamina Hossain and Sairaj Dhople and Taylor T. Johnson},
title = {Reachability Analysis of Closed-Loop Switching Power Converters},
year = {2013},
booktitle = {Proceedings of the 4th IEEE Power and Energy Conference at Illinois (PECI 2013)},
address = {Urbana, Illinois, USA},
month = feb,
pages = {},
doi = {10.1109/PECI.2013.6506047},
gsid = {8886180814224184900},
abstract = {A design verification method for closed-loop switching power converters is presented in this paper. The method computes the set of reachable states from an initial set of states. Case studies are presented for closed-loop buck converters using this approach. The buck converter is first modeled as a switched linear system. Two controllers are studied, first a simple hysteresis controller, and then a linear controller. The analysis method is automated and uses the hybrid systems reachability analysis tool SpaceEx. The applications and limitations of the analysis method are explored in this study.},
pdf = {http://www.taylortjohnson.com/research/hossain2013peci.pdf},
}
@inproceedings{duggirala2012rtss,
author = {Parasara Sridhar Duggirala and Taylor T. Johnson and Adam Zimmerman and Sayan Mitra},
title = {Static and Dynamic Analysis of Timed Distributed Traces},
year = {2012},
booktitle = {Proceedings of the 33rd IEEE Real-Time Systems Symposium (RTSS 2012)},
address = {San Juan, Puerto Rico},
month = dec,
pages = {173--182},
doi = {10.1109/RTSS.2012.69},
gsid = {7478096960006514961},
abstract = {This paper presents an algorithm for checking global predicates from traces of distributed embedded systems. For an individual agent, such as a mobile phone, tablet, or robot, a trace is a finite sequence of state observations and message histories. Each recording has a possibly inaccurate timestamp from the agent's local clock. The challenge is to symbolically overapproximate the reachable states of the entire system from the unsynchronized traces of the individual devices. The presented algorithm first approximates the time of occurrence of each event, based on the synchronization errors of the local clocks, and then overapproximates the reach sets of the continuous variables between consecutive observations. The algorithm is shown to be sound; it is also complete for a class of agents with restricted continuous dynamics and when the traces have precise information about timing synchronization inaccuracies. The algorithm is implemented in an SMT solver-based tool for analyzing traces of distributed Android Apps. Experimental results using the tool illustrate that interesting properties like safe separation, correct geocast delivery, and distributed deadlocks can be automatically checked and potential counterexamples can be found. Analyzing these properties on a 10 second long distributed trace for 20 agents completes within a minute and often in seconds, suggesting that the approach can scale.},
pdf = {http://www.taylortjohnson.com/research/duggirala2012rtss.pdf},
}
@article{johnson2015tcs,
author = {Taylor T. Johnson and Sayan Mitra},
title = {Safe and Stabilizing Distributed Multi-Path Cellular Flows},
year = {2015},
journal = {Theoretical Computer Science},
publisher = {Elsevier},
address = {},
volume = {},
number = {},
issn = {},
doi = {10.1016/j.tcs.2015.01.023},
pages = {1--46},
month = feb,
pdf = {http://www.taylortjohnson.com/research/johnson2015tcs.pdf},
software = {https://bitbucket.org/verivital/cell_flows},
abstract = {We study the problem of distributed traffic control in the partitioned plane, where the movement of all entities (vehicles) within each partition (cell) is coupled. Establishing liveness in such systems is challenging, but such analysis will be necessary to apply such distributed traffic control algorithms in applications like the intelligent highway system and for coordinating robot swarms. We present a distributed traffic control protocol that guarantees minimum separation between vehicles, even as some cells fail. Once new failures cease occurring, in the case of a single target, the protocol is guaranteed to self-stabilize and the vehicles with feasible paths to the target cell make progress towards it. For multiple targets, failures may cause deadlocks in the system, so we identify a class of non-deadlocking failures where all vehicles are able to make progress to their respective targets. The algorithm relies on two general principles: temporary blocking for maintenance of safety and local geographical routing for guaranteeing progress. Our assertional proofs may serve as a template for the analysis of other distributed traffic control protocols. We present simulation results that provide estimates of throughput as a function of vehicle velocity, safety separation, single-target path complexity, failure-recovery rates, and multi-target path complexity.},
}
@incollection{johnson2012fm,
author = {Taylor T. Johnson and Jeremy Green and Sayan Mitra and Rachel Dudley and Richard Scott Erwin},
title = {Satellite Rendezvous and Conjunction Avoidance: Case Studies in Verification of Nonlinear Hybrid Systems},
year = {2012},
booktitle = {Proceedings of the 18th International Conference on Formal Methods (FM 2012)},
address = {Paris, France},
month = aug,
isbn = {978-3-642-32758-2},
volume = {7436},
gsid = {6661230319939383532},
editor = {Giannakopoulou, Dimitra and M\'{e}ry, Dominique},
doi = {10.1007/978-3-642-32759-9_22},
publisher = {Springer Berlin Heidelberg},
pages = {252--266},
abstract = {Satellite systems are beginning to incorporate complex autonomous operations, which calls for rigorous reliability assurances. Human operators usually plan satellite maneuvers in detail, but autonomous operation will require software to make decisions using noisy sensor data and problem solutions with numerical inaccuracies. For such systems, formal verification guarantees are particularly attractive. This paper presents automatic verification techniques for providing assurances in satellite maneuvers. The specific reliability criteria studied are rendezvous and conjunction avoidance for two satellites performing orbital transfers. Three factors pose challenges for verifying satellite systems: (a) incommensurate orbits, (b) uncertainty of orbital parameters after thrusting, and (c) nonlinear dynamics. Three abstractions are proposed for contending with these challenges: (a) quotienting of the state-space based on periodicity of the orbital dynamics, (b) aggregation of similar transfer orbits, and (c) overapproximation of nonlinear dynamics using hybridization. The method's feasibility is established via experiments with a prototype tool that computes the abstractions and uses existing hybrid systems model checkers.},
pdf = {http://www.taylortjohnson.com/research/johnson2012fm.pdf},
}
@inproceedings{johnson2012forte,
author = {Taylor T. Johnson and Sayan Mitra},
title = {A Small Model Theorem for Rectangular Hybrid Automata Networks},
year = {2012},
booktitle = {Proceedings of the IFIP International Conference on Formal Techniques for Distributed Systems, Joint 14th Formal Methods for Open Object-Based Distributed Systems and 32nd Formal Techniques for Networked and Distributed Systems (FORTE/FMOODS 2012)},
address = {Stockholm, Sweden},
month = jun,
pages = {},
gsid = {4606381030313410526},
abstract = {Rectangular hybrid automata (RHA) are finite state machines with additional skewed clocks that are useful for modeling real-time systems. This paper is concerned with the uniform verification of safety properties of networks with arbitrarily many interacting RHAs. Each automaton is equipped with a finite collection of pointers to other automata that enables it to read their state. This paper presents a small model result for such networks that reduces the verification problem for a system with arbitrarily many processes to a system with finitely many processes. The result is applied to verify and discover counterexamples of inductive invariant properties for distributed protocols like Fischer's mutual exclusion algorithm and the Small Aircraft Transportation System (SATS). We have implemented a prototype tool called Passel relying on the satisfiability modulo theories (SMT) solver Z3 to check inductive invariants automatically.},
doi = {10.1007/978-3-642-30793-5_2},
comment = {**Best Paper Award for DisCoTec**, Passel tool and specification source, Passel tool overview},
pdf = {http://www.taylortjohnson.com/research/johnson2012forte.pdf},
software = {http://publish.illinois.edu/passel-tool/},
}
@inproceedings{johnson2012iccps,
author = {Taylor T. Johnson and Sayan Mitra},
title = {Parameterized Verification of Distributed Cyber-Physical Systems: An Aircraft Landing Protocol Case Study},
year = {2012},
booktitle = {Proceedings of the 3rd ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS 2012)},
address = {Beijing, China},
month = apr,
pages = {161--170},
gsid = {11740586308134469378},
doi = {10.1109/ICCPS.2012.24},
abstract = {In this paper, we present the formal modeling and automatic parameterized verification of a distributed air traffic control protocol called the Small Aircraft Transportation System (SATS). Each aircraft is modeled as a timed automaton with (possibly unbounded) counters. SATS is then described as the composition of $N$ such aircraft, where $N$ is a parameter from the natural numbers. We verify several safety properties for arbitrary $N$, the most important of which is separation assurance, which ensures that no two aircraft may ever collide. The verification methodology relies on computing the set of backward reachable states from the set of unsafe states to a fixed point, and checking emptiness of the intersection of these reachable states and the initial set of states. We used the Model Checker Modulo Theories (MCMT) tool, which implements this technique.},
comment = {source code},
pdf = {http://www.taylortjohnson.com/research/johnson2012iccps.pdf},
}
@inproceedings{johnson2012peci,
author = {Taylor T. Johnson and Zhihao Hong and Akash Kapoor},
title = {Design Verification Methods for Switching Power Converters},
year = {2012},
booktitle = {Proceedings of the 3rd IEEE Power and Energy Conference at Illinois (PECI 2012)},
address = {Urbana, Illinois, USA},
month = feb,
pages = {1--6},
gsid = {17399493867618088222},
doi = {10.1109/PECI.2012.6184587},
abstract = {In this paper, we present two methods for performing design verification of switching power converters. The first method can be used to compute the set of reachable states from an initial set of states with non-deterministic parameters. We demonstrate the method on a buck converter in an open-loop configuration. The method is automatic and uses the hybrid systems reachability analysis tool SpaceEx. The second method uses model checking to verify circuits that can naturally be modeled as timed automata. We demonstrate the method on an open-loop multilevel converter used to convert several DC inputs to one AC output. The method is also automatic and uses the timed automata model checker Uppaal. Finally, we mention that in contrast to simulation or testing based approaches---for instance, the standard Monte Carlo analysis used when analyzing component variation in circuit designs---the methods presented in this paper perform the verification for all runs of the circuits and all possible component parameter variations.},
pdf = {http://www.taylortjohnson.com/research/johnson2012peci.pdf},
}
@inproceedings{johnson2011cdc,
author = {Taylor T. Johnson and Sayan Mitra and Cedric Langbort},
title = {Stability of Digitally Interconnected Linear Systems},
year = {2011},
booktitle = {Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference (CDC ECC 2011)},
address = {Orlando, Florida, USA},
month = dec,
pages = {2687--2692},
gsid = {14666544104064248628},
doi = {10.1109/CDC.2011.6161264},
abstract = {A sufficient condition for stability of linear subsystems interconnected by digitized signals is presented. There is a digitizer for each linear subsystem that periodically samples an input signal and produces an output that is quantized and saturated. The output of the digitizer is then fed as an input (in the usual sense) to the linear subsystem. Due to digitization, each subsystem behaves as a switched affine system, where state-dependent switches are induced by the digitizer. For each quantization region, a storage function is computed for each subsystem by solving appropriate linear matrix inequalities (LMIs), and the sum of these storage functions is a Lyapunov function for the interconnected system. Finally, using a condition on the sampling period, we specify a subset of the unsaturated state space from which all executions of the interconnected system reach a neighborhood of the quantization region containing the origin. The sampling period proves to be pivotal---if it is too small, then a dwell-time argument cannot be used to establish convergence, while if it is too large, an unstable subsystem may not receive timely-enough inputs to avoid diverging.},
issn = {0743-1546},
pdf = {http://www.taylortjohnson.com/research/johnson2011cdc.pdf},
}
@article{johnson2011jnsa,
author = {Taylor T. Johnson and Sayan Mitra},
title = {Safe Flocking in Spite of Actuator Faults using Directional Failure Detectors},
year = {2011},
journal = {Journal of Nonlinear Systems and Applications},
publisher = {Watam Press Inc.},
address = {Waterloo, Ontario, Canada},
volume = {2},
number = {1-2},
issn = {1918-3704},
pages = {73--95},
month = apr,
gsid = {17168942288498640040},
abstract = {The safe flocking problem requires a collection of mobile agents to (a) converge to and maintain an equi-spaced lattice formation, (b) arrive at a destination, and (c) always maintain a minimum safe separation. Safe flocking in Euclidean spaces is a well-studied and difficult coordination problem. In this paper, we study one-dimensional safe flocking in the presence of actuator faults and directional failure detectors (DFDs). Actuator faults cause affected agents to move permanently with arbitrary velocities, and DFDs detect failures only when actuation and required motion are in opposing directions. First, assuming existence of a DFD for actuator faults, we present an algorithm for safe flocking. Next, we show that certain actuator faults cannot be detected with DFDs, while detecting others requires time that grows linearly with the number of participating agents. Finally, we show that our DFD algorithm achieves the latter bound.},
comment = {pdf (publisher), doi},
pdf = {http://www.taylortjohnson.com/research/johnson2011jnsa.pdf},
}
@inproceedings{johnson2011peci,
author = {Taylor T. Johnson and Albert Hoefel},
title = {Turbo-Alternator Stalling Protection using Available Power Estimate},
booktitle = {Proceedings of the 2nd Annual IEEE Power and Energy Conference at Illinois (PECI 2011)},
year = {2011},
address = {Urbana, Illinois, USA},
month = feb,
doi = {10.1109/PECI.2011.5740501},
gsid = {14808654063079790680},
comment = {**Best Paper Award**},
pdf = {http://www.taylortjohnson.com/research/johnson2011peci.pdf},
abstract = {In environments where electromechanical loads may suffer from disturbances with large magnitude---such as in sampling downhole reservoirs---stalling protection for the power source of the alternator may be critical to prevent potentially catastrophic system failure. First, a real-time estimation method is described to determine the maximum available electrical power produced by a turbo-alternator for a given volumetric flow rate acting on the turbine. Next, the available-power estimate and used electrical power measurement are used to prevent turbine stalling by regulating an electromechanical load---in this case a permanent magnet synchronous motor (PMSM)---to draw less power. The stalling protection is implemented through an additional proportional-integral-derivative (PID) controller for load power, which is cascaded outside already cascaded velocity and torque PID controllers used for control of the PMSM. To ensure fast tracking, the power PID controller implements integral anti-windup. An experimental evaluation of the methodology is presented.},
}
@incollection{johnson2010sss,
author = {Taylor T. Johnson and Sayan Mitra},
affiliation = {University of Illinois at Urbana-Champaign, Urbana, IL 61801, USA},
title = {Safe Flocking in Spite of Actuator Faults},
booktitle = {12th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2010)},
series = {Lecture Notes in Computer Science},
editor = {Dolev, Shlomi and Cobb, Jorge and Fischer, Michael and Yung, Moti},
publisher = {Springer Berlin / Heidelberg},
isbn = {},
pages = {588--602},
volume = {6366},
doi = {10.1007/978-3-642-16023-3_45},
gsid = {14477781552252082549},
abstract = {The safe flocking problem requires a collection of N mobile agents to (a) converge to and maintain an equi-spaced lattice formation, (b) arrive at a destination, and (c) always maintain a minimum safe separation. Safe flocking in Euclidean spaces is a well-studied and difficult coordination problem. Motivated by real-world deployment of multi-agent systems, this paper studies one-dimensional safe flocking, where agents are afflicted by actuator faults. An actuator fault is a new type of failure that causes an affected agent to be stuck moving with an arbitrary velocity. In this setting, first, a self-stabilizing solution for the problem is presented. This relies on a failure detector for actuator faults. Next, it is shown that certain actuator faults cannot be detected, while others may require $O(N)$ time for detection. Finally, a simple failure detector that achieves the latter bound is presented. Several simulation results are presented for illustrating the effects of failures on the progress towards flocking.},
year = {2010},
month = sep,
pdf = {http://www.taylortjohnson.com/research/johnson2010sss.pdf},
}
@inproceedings{johnson2010icdcs,
author = {Taylor T. Johnson and Sayan Mitra and Karthik Manamcheri},
booktitle = {30th IEEE International Conference on Distributed Computing Systems (ICDCS 2010)},
title = {Safe and Stabilizing Distributed Cellular Flows},
year = {2010},
month = jun,
pages = {577--578},
keywords = {},
ISSN = {1063-6927 },
isbn = {978-1-4244-7261-1},
address = {Genoa, Italy},
gsid = {12377696546842138389},
abstract = {Advances in wireless vehicular networks present us with opportunities for developing new distributed traffic control algorithms that avoid phenomena such as abrupt phase-transitions. Towards this end, we study the problem of distributed traffic control in a partitioned plane where the movement of all entities (vehicles) within each partition (or cell) is controlled by a single process. We present a distributed traffic control protocol that guarantees minimum separation between vehicles at all times, even when some cell-processes fail by crashing. Once failures cease, the protocol is guaranteed to stabilize and the packets with feasible paths to the target cell make progress towards it. The algorithm relies on two general principles: local geographical routing, and temporary blocking for maintenance of safety. Our proofs use mostly assertional reasoning and may serve as a template for analyzing other distributed traffic control protocols. We also present simulation results which provide estimates of throughput as a function of velocity, safety separation, and path complexity. Further, we present simulation results to estimate throughput as a function of failure and recovery rates.},
doi = {10.1109/ICDCS.2010.49},
pdf = {http://www.taylortjohnson.com/research/johnson2010icdcs.pdf},
}
@techreport{johnson2010tr,
author = {Taylor T. Johnson and Sayan Mitra},
title = {Safe and Stabilizing Distributed Flocking In Spite of Actuator Faults},
institution = {University of Illinois at Urbana-Champaign},
address = {Urbana, IL 61801, USA},
month = may,
year = {2010},
number = {UILU-ENG-10-2204 (CRHC-10-02)},
note = {Extended version of~\cite{johnson2010sss}},
pdf = {http://www.taylortjohnson.com/research/johnson2010tr.pdf},
}
@mastersthesis{johnson2010msthesis,
author = {Taylor T. Johnson},
title = {Fault-Tolerant Distributed Cyber-Physical Systems: Two Case Studies},
school = {Department of Electrical and Computer Engineering, University of Illinois at Urbana-Champaign},
address = {Urbana, IL 61801, USA},
month = may,
year = 2010,
gsid = {9683503763763426403},
abstract = {Fault-tolerance in distributed computing systems has been investigated extensively in the literature and has a rich history and detailed theory. This thesis studies fault-tolerance for distributed cyber-physical systems (DCPS), where distributed computation is combined with dynamics of physical processes. Due to their interaction with the physical world, DCPS may suffer from failures that are qualitatively different from the types of failures studied in distributed computing. Failures of the components of DCPS which interact with the physical processes---such as actuators and sensors---must be considered. Failures in the cyber domain may interact with failures of sensors and actuators in adverse ways.
This thesis takes a first step in analyzing fault-tolerance in DCPS through the presentation of two case studies. In each case study, the DCPS are modeled as distributed algorithms executed by a set of agents, where each agent acts independently based on information obtained from its communication neighbors and agents may suffer from various failures. The first case study is a distributed traffic control problem, where agents control regions of roadway to move vehicles toward a destination, in spite of some agents' computers crashing permanently. The second case study is a distributed flocking problem, where agents form a flock, or a roughly equally spaced distribution in one dimension, and move towards a destination, in spite of some agents' actuators becoming stuck at some value.
Each algorithm incorporates self-stabilization in order to solve the problem in spite of failures. The traffic algorithm uses a local signaling mechanism to guarantee safety and a self-stabilizing routing protocol to guarantee progress. The flocking algorithm uses a failure detector combined with an additional control strategy to ensure safety and progress.},
comment = {doi},
pdf = {http://www.taylortjohnson.com/research/johnson2010msthesis.pdf},
}
@misc{johnson2009rtss,
author = {Taylor T. Johnson and Sayan Mitra},
title = {Handling Failures in Cyber-Physical Systems: Potential Directions},
note = {Presented at RTSS 2009 PhD Student Forum},
year = {2009},
month = dec,
gsid = {18127665186175310638},
abstract = {The strong coupling of software and physical processes in the emerging field of cyber-physical systems (CPS) motivates the development of new methods to respond to failures in both the cyber and physical domains. To this end, we propose a study of existing work on handling failures from various disciplines. If these models and methods are applicable to CPS, appropriate extensions should be made to apply them. However, if they are not, then we should head off into uncharted territory, developing new methods, which we suggest to be drawn from fields such as formal methods and verification.},
comment = {**Award for Most Interesting Cyber-Physical Systems Research Problem**},
pdf = {http://www.taylortjohnson.com/research/johnson2009rtss.pdf},
slides = {http://www.taylortjohnson.com/research/slides/johnson2009rtss_slides.pdf},
}
@misc{johnson2009rtas,
author = {Taylor T. Johnson and Sayan Mitra},
title = {Power Usage of Time and Event-Triggered Paradigms: A Case Study},
note = {Presented at RTAS 2009 Poster Session},
abstract = {We evaluate the time-triggered and event-triggered programming paradigms in the context of developing large-scale distributed real-time systems with fault-tolerance. To this end, we present a simple case study using the Lego Mindstorms NXT platform in an intrusion detection problem, and compare the power consumption and accuracy of event detection in time-triggered and event-triggered systems. We use this case study comparison as part of the motivation for the development of a new mixed event-triggered and time-triggered language.},
year = {2009},
gsid = {1931943751823825557},
month = apr,
pdf = {http://www.taylortjohnson.com/research/johnson2009rtas.pdf},
slides = {http://www.taylortjohnson.com/research/johnson2009rtas_poster.pdf},
software = {http://code.google.com/p/nxtosek-giotto/},
}