@STRING{hp_Hoang-DungTran="https://sites.google.com/site/trhoangdung/"}
@STRING{hp_TaylorT.Johnson="http://www.taylortjohnson.com/"}
@STRING{hp_JohnsonTaylorT="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"}
@STRING{hp_KhalilGhorbal="http://www.lix.polytechnique.fr\~ghorbal/"}
@STRING{hp_KhazaAnuarulHoque="http://www.uta.edu/faculty/hoqueka/"}
@STRING{hp_OsmanHasan="http://ohasan.seecs.nust.edu.pk/"}
@STRING{hp_WeimingXiang="https://scholar.google.com/citations?user=Vm_7JP8AAAAJ&hl=en"}
@STRING{hp_XiangWeiming="https://scholar.google.com/citations?user=Vm_7JP8AAAAJ&hl=en"}
% NOTE: remember to include . in Taylor's name, otherwise there's a weird parsing bug
@INPROCEEDINGS{an2024aaai,
author={Ziyan An and Taylor T. Johnson and Meiyi Ma},
title={Formal Logic Enabled Personalized Federated Learning through Property Inference},
booktitle={Proceedings of the 38th AAAI Conference on Artificial Intelligence (AAAI'24)},
year={2024},
month=feb,
volume={},
number={},
pages={},
doi={10.1609/aaai.v38i10.28962},
pdf="research/an2024.pdf"
}
@INPROCEEDINGS{robinette2023ecai,
author={Preston Robinette and Taylor T. Johnson and David Wang and Nishan Shehadeh and Daniel Moyer},
booktitle={26th European Conference on Artificial Intelligence (ECAI)},
title={{SUDS}: Sanitizing Universal and Dependent Steganography},
year={2023},
month=sept,
volume={},
number={},
pages={},
doi={},
pdf="research/robinette2023ecai.pdf"
}
@INPROCEEDINGS{lopez2023cav,
author={Diego Manzanas Lopez and Sung Woo Choi and Hoang-Dung Tran and Taylor T. Johnson},
booktitle={International Conference on Computer Aided Verification (CAV)},
title={{NNV} 2.0: the neural network verification tool},
year={2023},
month=july,
volume={},
number={},
pages={},
doi={},
pdf="research/lopez2023cav.pdf"
}
@ARTICLE{lopez2022jat,
author={Diego Manzanas Lopez and Taylor T. Johnson and Stanley Bak and Hoang-Dung Tran and Kerianne Hobbs},
journal={AIAA Journal of Air Transportation (JAT)},
title={Evaluation of Neural Network Verification Methods for Air to Air Collision Avoidance},
year={2022},
month=oct,
volume={},
number={},
pages={},
pdf = "research/lopez2022jat.pdf",
doi = {},
}
@INPROCEEDINGS{serbinowski2022sefm,
author={Bernard Serbinowski and Taylor T. Johnson},
booktitle={20th International Conference on Software Engineering and Formal Methods (SEFM)},
title={BehaVerify: Verifying Temporal Logic Specifications for Behavior Trees},
year={2022},
month=sep,
volume={},
number={},
pages={},
doi={},
pdf="research/serbinowski2022sefm.pdf"
}
@INPROCEEDINGS{hamilton2022sefm,
author={Hamilton, Nathaniel and Preston K. Robinette and Taylor T. Johnson},
booktitle={20th International Conference on Software Engineering and Formal Methods (SEFM)},
title={Training Agents to Satisfy Timed and Untimed Signal Temporal Logic Specifications with Reinforcement Learning},
year={2022},
month=sep,
volume={},
number={},
pages={},
doi={},
pdf="research/hamilton2022sefm.pdf"
}
@INPROCEEDINGS{yang2022formats,
author={Xiaodong Yang and Tom Yamaguchi and Hoang-Dung Tran and Taylor T. Johnson and Danil Prokhorov},
booktitle={20th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS)},
title={Neural Network Repair with Reachability Analysis},
year={2022},
month=sep,
volume={},
number={},
pages={},
doi={},
pdf="research/yang2022formats.pdf"
}
@INPROCEEDINGS{lopez2022formats,
author={Diego Manzanas Lopez and Patrick Musau and Nathaniel Hamilton and Taylor T. Johnson},
booktitle={20th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS)},
title={Reachability Analysis of a General Class of Neural Ordinary Differential Equations},
year={2022},
month=sep,
volume={},
number={},
pages={},
doi={},
pdf="research/lopez2022formats.pdf"
}
@INPROCEEDINGS{bao2022uai,
author={Tianshu Bao and Shengyu Chen and Taylor T. Johnson and Peyman Givi and Shervin Sammak and Xiaowei Jia},
booktitle={38th Conference on Uncertainty in Artificial Intelligence (UAI)},
title={Physics Guided Neural Networks for Spatio-temporal Super-resolution of Turbulent Flows},
year={2022},
month=aug,
volume={},
number={},
pages={},
pdf="research/bao2022uai.pdf",
}
@INPROCEEDINGS{hamilton2022icaa,
author={Hamilton, Nathaniel and Musau, Patrick and Lopez, Diego Manzanas and Taylor T. Johnson},
booktitle={2022 IEEE International Conference on Assured Autonomy (ICAA)},
title={Zero-Shot Policy Transfer in Autonomous Racing: Reinforcement Learning vs Imitation Learning},
year={2022},
volume={},
number={},
pages={11-20},
doi={10.1109/ICAA52185.2022.00011},
pdf="research/hamilton2022icaa.pdf"
}
@INPROCEEDINGS{musau2022icaa,
author={Musau, Patrick and Hamilton, Nathaniel and Lopez, Diego Manzanas and Robinette, Preston and Taylor T. Johnson},
booktitle={2022 IEEE International Conference on Assured Autonomy (ICAA)},
title={On Using Real-Time Reachability for the Safety Assurance of Machine Learning Controllers},
year={2022},
volume={},
number={},
pages={1-10},
doi={10.1109/ICAA52185.2022.00010},
pdf="research/musau2022icaa.pdf"
}
@INPROCEEDINGS{bao2021icdm,
author={Bao, Tianshu and Jia, Xiaowei and Zwart, Jacob and Sadler, Jeffrey and Appling, Alison and Oliver, Samantha and Taylor T. Johnson},
booktitle={2021 IEEE International Conference on Data Mining (ICDM)},
title={Partial Differential Equation Driven Dynamic Graph Networks for Predicting Stream Water Temperature},
year={2021},
month = "December",
volume={},
number={},
pages={11-20},
doi={10.1109/ICDM51629.2021.00011},
pdf="research/bao2021icdm.pdf"
}
@inproceedings{johnson2021archcomp,
author = {Taylor T. Johnson},
title = {ARCH-COMP21 Repeatability Evaluation Report},
booktitle = {8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21)},
editor = {Goran Frehse and Matthias Althoff},
series = {EPiC Series in Computing},
volume = {80},
pages = {153--160},
year = {2021},
publisher = {EasyChair},
issn = {2398-7340},
url = {https://easychair.org/publications/paper/cfpN},
doi = {10.29007/zqdx}
}
@inproceedings{johnson2021archcomp_ainncs,
author = {Taylor T. Johnson and Diego Manzanas Lopez and Luis Benet and Marcelo Forets and Sebastian Guadalupe and Christian Schilling and Radoslav Ivanov and Taylor J. Carpenter and James Weimer and Insup Lee},
title = {ARCH-COMP21 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants},
booktitle = {8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21)},
editor = {Goran Frehse and Matthias Althoff},
series = {EPiC Series in Computing},
volume = {80},
pages = {90--119},
year = {2021},
publisher = {EasyChair},
issn = {2398-7340},
url = {https://easychair.org/publications/paper/Jq4h},
doi = {10.29007/kfk9}
}
@InProceedings{tran2021cav,
author = "Hoang-Dung Tran and Neelanjana Pal and Patrick Musau and Xiaodong Yang and Nathaniel P. Hamilton and Diego Manzanas Lopez and Stanley Bak and Taylor T. Johnson",
title = "Robustness Verification of Semantic Segmentation Neural Networks using Relaxed Reachability",
booktitle = "33rd International Conference on Computer-Aided Verification (CAV)",
year = "2021",
month = "July",
publisher = "Springer",
pdf = "research/tran2021cav.pdf",
}
@InProceedings{muvva2021scitech,
author = "Krishna Muvva and Justin M. Bradley and Marilyn Wolf and Taylor T. Johnson",
title = "Assuring Learning-Enabled Components in Small Unmanned Aircraft Systems",
booktitle = "AIAA Scitech 2021 Forum",
year = "2021",
month = "January",
publisher = "AIAA",
pdf = "research/muvva2021scitech.pdf",
doi = "10.2514/6.2021-0994",
}
@InProceedings{lopez2021scitech,
author = "Diego Manzanas Lopez and Taylor T. Johnson and Hoang-Dung Tran and Stanley Bak and Xin Chen and Kerianne Hobbs",
title = "Verification of Neural Network Compression of ACAS Xu Lookup Tables with Star Set Reachability",
booktitle = "AIAA Scitech 2021 Forum",
year = "2021",
month = "January",
publisher = "AIAA",
pdf = "research/lopez2021scitech.pdf",
}
@ARTICLE{xiang2021tnnls,
author={Weiming Xiang and Hoang-Dung Tran and Xiaodong Yang and Taylor T. Johnson},
journal={IEEE Transactions on Neural Networks and Learning Systems},
title={Reachable Set Estimation for Neural Network Control Systems: A Simulation-Guided Approach},
year={2021},
month=may,
volume={32},
number={5},
pages={1821-1830},
pdf = "research/xiang2021tnnls.pdf",
doi = {10.1109/TNNLS.2020.2991090},
}
@inproceedings{yang2021hscc,
author = {Yang, Xiaodong and Taylor T. Johnson and Tran, Hoang-Dung and Yamaguchi, Tomoya and Hoxha, Bardh and Prokhorov, Danil},
title = {Reachability Analysis of Deep ReLU Neural Networks Using Facet-Vertex Incidence},
year = {2021},
isbn = {9781450383394},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
doi = {10.1145/3447928.3456650},
booktitle = {Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control (HSCC)},
articleno = {18},
numpages = {7},
location = {Nashville, Tennessee},
series = {HSCC '21},
pdf = "research/yang2021hscc.pdf",
}
@ARTICLE{beg2021access,
author={Beg, Omar Ali and Nguyen, Luan Viet and Johnson, Taylor T. and Davoudi, Ali},
journal={IEEE Access},
title={Cyber-Physical Anomaly Detection in Microgrids Using Time-Frequency Logic Formalism},
year={2021},
volume={9},
number={},
pages={20012-20021},
doi={10.1109/ACCESS.2021.3055229}
}
@ARTICLE{tran2020mdat,
author={Tran, Hoang-Dung and Xiang, Weiming and Johnson, Taylor T.},
journal={IEEE Design and Test},
title={Verification Approaches for Learning-Enabled Autonomous Cyber-Physical Systems},
year={2020},
volume={},
number={},
pages={1-1},
doi={10.1109/MDAT.2020.3015712},
pdf="research/tran2020dandt.pdf",
}
@InProceedings{tran2020cav,
author = "Hoang-Dung Tran and Stanley Bak and Weiming Xiang and Taylor T. Johnson",
title = "Verification of Deep Convolutional Neural Networks Using ImageStars",
booktitle = "32nd International Conference on Computer-Aided Verification (CAV)",
year = "2020",
month = "July",
publisher = "Springer",
pdf = "research/tran2020cav.pdf",
doi = "10.1007/978-3-030-53288-8_2"
}
@inproceedings{tran2020cav_tool,
author = "Hoang-Dung Tran and Xiaodong Yang and Diego Manzanas Lopez and Patrick Musau and Luan Viet Nguyen and Weiming Xiang and Stanley Bak and Taylor T. Johnson",
title = "{NNV}: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems",
booktitle = "32nd International Conference on Computer-Aided Verification (CAV)",
year = "2020",
month = "July",
pdf = "research/tran2020cav_tool.pdf",
doi = "10.1007/978-3-030-53288-8_1",
}
@inproceedings{bak2020cav,
author = "Stanley Bak and Hoang-Dung Tran and Kerianne Hobbs and Taylor T. Johnson",
title = "Improved Geometric Path Enumeration for Verifying {ReLU} Neural Networks",
booktitle = "32nd International Conference on Computer-Aided Verification (CAV)",
year = "2020",
month = "July",
pdf = "research/bak2020cav.pdf",
doi = "10.1007/978-3-030-53288-8_4",
}
@inproceedings{chowdhury2020icse,
author="Shafiul Azam Chowdhury and Sohil Lal Shrestha and Taylor T. Johnson and Christoph Csallner",
title="{SLEMI}: Equivalence Modulo Input (EMI) Based Mutation of CPS Models for Finding Compiler Bugs in Simulink",
year="2020",
booktitle="42nd ACM/IEEE International Conference on Software Engineering (ICSE)",
month="May",
pdf="research/chowdhury2020icse.pdf",
}
@misc{chowdhury2020icse_demo,
author="Shafiul Azam Chowdhury and Sohil Lal Shrestha and Taylor T. Johnson and Christoph Csallner",
title="Demo: {SLEMI}: Finding Simulink Compiler Bugs through Equivalence Modulo Input (EMI)",
year="2020",
booktitle="42nd ACM/IEEE International Conference on Software Engineering (ICSE)",
month="May",
pdf="research/chowdhury2020icse_demo.pdf",
}
@InProceedings{tran2019emsoft,
author="Tran, Hoang-Dung
and Feiyang Cei
and Diego Manzanas Lopez
and Taylor T. Johnson
and Xenofon Koutsoukos",
title="Safety Verification of Cyber-Physical Systems with Reinforcement Learning Control",
booktitle="ACM SIGBED International Conference on Embedded Software (EMSOFT'19)",
year="2019",
month="October",
publisher="ACM",
pdf="research/tran2019emsoft.pdf",
}
@InProceedings{tran2019fm,
author="Tran, Hoang-Dung
and Musau, Patrick
and Diego Manzanas Lopez
and Xiaodong Yang
and Nguyen, Luan Viet
and Xiang, Weiming
and Taylor T. Johnson",
editor="",
title="Star-Based Reachability Analysis for Deep Neural Networks",
booktitle="23rd International Symposium on Formal Methods (FM'19)",
year="2019",
month="October",
publisher="Springer International Publishing",
pdf="research/tran2019fm.pdf",
}
@InProceedings{tran2019formats,
author="Tran, Hoang-Dung
and Nguyen, Luan Viet
and Nathaniel Hamilton
and Xiang, Weiming
and Taylor T. Johnson",
editor="",
title="Reachability Analysis for High-Index Linear Differential Algebraic Equations (DAEs)",
booktitle="17th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'19)",
year="2019",
month="August",
publisher="Springer International Publishing",
pdf="research/tran2019formats.pdf",
}
@InProceedings{tran2019forte,
author="Tran, Hoang-Dung
and Nguyen, Luan Viet
and Musau, Patrick
and Xiang, Weiming
and Taylor T. Johnson",
editor="P{\'e}rez, Jorge A.
and Yoshida, Nobuko",
title="Decentralized Real-Time Safety Verification for Distributed Cyber-Physical Systems",
booktitle="Formal Techniques for Distributed Objects, Components, and Systems (FORTE'19)",
year="2019",
publisher="Springer International Publishing",
address="Cham",
month="June",
pages="261--277",
abstract="Safety-critical distributed cyber-physical systems (CPSs) have been found in a wide range of applications. Notably, they have displayed a great deal of utility in intelligent transportation, where autonomous vehicles communicate and cooperate with each other via a high-speed communication network. Such systems require an ability to identify maneuvers in real-time that cause dangerous circumstances and ensure the implementation always meets safety-critical requirements. In this paper, we propose a real-time decentralized safety verification approach for a distributed multi-agent CPS with the underlying assumption that all agents are time-synchronized with a low degree of error. In the proposed approach, each agent periodically computes its local reachable set and exchanges this reachable set with the other agents with the goal of verifying the system safety. Our method, implemented in Java, takes advantages of the timing information and the reachable set information that are available in the exchanged messages to reason about the safety of the whole system in a decentralized manner. Any particular agent can also perform local safety verification tasks based on their local clocks by analyzing the messages it receives. We applied the proposed method to verify, in real-time, the safety properties of a group of quadcopters performing a distributed search mission.",
isbn="978-3-030-21759-4",
pdf="research/tran2019forte.pdf",
}
@article{rahman2019aap,
title = "Using crowd sourcing to locate and characterize conflicts for vulnerable modes",
journal = "Accident Analysis and Prevention",
volume = "128",
pages = "32--39",
year = "2019",
issn = "0001-4575",
doi = "10.1016/j.aap.2019.03.014",
author = "Ziaur Rahman and Stephen P. Mattingly and Rahul Kawadgave and Dian Nostikasari and Nicole Roeglin and Colleen Casey and Taylor T. Johnson",
keywords = "Bicyclist, Pedestrian, Surrogate safety measure, App development, Crowd sourcing, Hot spot analysis",
abstract = "Most agencies and decision-makers rely on crash and crash severity (property damage only, injury or fatality) data to assess transportation safety; however, in the context of public health where perceptions of safety may influence the willingness to adopt active transportation modes (e.g. bicycling and walking), pedestrian-motor vehicle and other similar conflicts types may define a better performance measure for safety assessment. In the field of transportation safety, an absolute conflict occurs when two parties’ paths cross and one of the parties must undertake an evasive maneuver (e.g. change direction or stop) to avoid a crash. Other less severe conflicts where paths cross but no evasive maneuver is required may also impact public perceptions of safety especially for vulnerable modes. Most of the existing literature focuses on vehicle conflicts. While in the past several years, more research has investigated bicycle and pedestrian conflicts, most of this has focused on the intersection environment. A comprehensive analysis of conflicts appears critical. The major objective of this study is two fold: 1) Development of an innovative and cost effective conflict data collection technique to better understand the conflicts (and their severity) involving vulnerable road users (e.g. bicycle/pedestrian, bicycle/motor vehicle, and pedestrian/motor vehicle) and their severity. 2) Test the effectiveness and practicality of the approach taken and its associated crowd sourced data collection. In an endeavor to undertake these objectives, the researchers developed an android-based crowd-sourced data collection app. The crowd-source data collected using the app is compared with traditional fatality data for hot spot analysis. At the end, the app users provide feedback about the overall competency of the app interface and the performance of its features to the app developers. If widely adopted, the app will enable communities to create their own data collection efforts to identify dangerous sites within their neighborhoods. Agencies will have a valuable data source at low-cost to help inform their decision making related to bicycle and pedestrian education, encouragement, enforcement, programs, policies, and infrastructure design and planning."
}
@inproceedings{tran2019formalise,
author = {Tran, Hoang-Dung and Musau, Patrick and Lopez, Diego Manzanas and Yang, Xiaodong and Nguyen, Luan Viet and Xiang, Weiming and Taylor T. Johnson},
title = {Parallelizable Reachability Analysis Algorithms for Feed-forward Neural Networks},
booktitle = {Proceedings of the 7th International Workshop on Formal Methods in Software Engineering (FormaliSE'19)},
series = {FormaliSE '19},
year = {2019},
location = {Montreal, Quebec, Canada},
pages = {31--40},
numpages = {10},
doi = {10.1109/FormaliSE.2019.00012},
acmid = {3338820},
publisher = {IEEE Press},
address = {Piscataway, NJ, USA},
month="May",
pdf = {research/tran2019formalise.pdf},
}
@inproceedings{manzanas2019arch_ainncs,
author = {Diego Manzanas Lopez and Patrick Musau and Hoang-Dung Tran and Souradeep Dutta and Taylor J. Carpenter and Radoslav Ivanov and Taylor T. Johnson},
title = {ARCH-COMP19 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants},
booktitle = {ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems},
editor = {Goran Frehse and Matthias Althoff},
series = {EPiC Series in Computing},
volume = {61},
pages = {103--119},
year = {2019},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {https://easychair.org/publications/paper/BFKs},
doi = {10.29007/rgv8},
month="April",
}
@inproceedings{manzanas2019arch,
author = {Diego Manzanas Lopez and Patrick Musau and Hoang-Dung Tran and Taylor T. Johnson},
title = {Verification of Closed-loop Systems with Neural Network Controllers},
booktitle = {ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems},
editor = {Goran Frehse and Matthias Althoff},
series = {EPiC Series in Computing},
volume = {61},
pages = {201--210},
year = {2019},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {https://easychair.org/publications/paper/ZmnC},
doi = {10.29007/btv1},
month = "April",
}
@inproceedings{johnson2019arch,
author = {Taylor T. Johnson},
title = {ARCH-COMP19 Repeatability Evaluation Report},
booktitle = {ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems},
editor = {Goran Frehse and Matthias Althoff},
series = {EPiC Series in Computing},
volume = {61},
pages = {162--169},
year = {2019},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {https://easychair.org/publications/paper/xvBM},
doi = {10.29007/wbl3},
month = "April",
}
@inproceedings{rees2019iccps_demo,
author = {Rees, Stephen A. and Kecskes, Tamas and Meijer, Patrik and Taylor T. Johnson and Dey, Katie and Tabuada, Paulo and Lucas, Marcus},
title = {Cyber-physical Systems Virtual Organization: Active Resources: Enabling Reproducibility, Improving Accessibility, and Lowering the Barrier to Entry},
booktitle = {Proceedings of the 10th ACM/IEEE International Conference on Cyber-Physical Systems},
series = {ICCPS '19},
year = {2019},
isbn = {978-1-4503-6285-6},
location = {Montreal, Quebec, Canada},
pages = {340--341},
numpages = {2},
url = {http://doi.acm.org/10.1145/3302509.3313331},
doi = {10.1145/3302509.3313331},
acmid = {3313331},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {analysis, cloud services, collaborative design, educational tools, modeling, reproducibility, verification, simulation, web-based tools},
month="April",
}
@inproceedings{bak2019hscc,
author = {Bak, Stanley and Tran, Hoang-Dung and Taylor T. Johnson},
title = {Numerical Verification of Affine Systems with Up to a Billion Dimensions},
booktitle = {Proceedings of the 22Nd ACM International Conference on Hybrid Systems: Computation and Control},
series = {HSCC '19},
year = {2019},
isbn = {978-1-4503-6282-5},
location = {Montreal, Quebec, Canada},
pages = {23--32},
numpages = {10},
doi = {10.1145/3302504.3311792},
acmid = {3311792},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {formal verification, hybrid systems, reachability},
pdf = {http://taylortjohnson.com/research/bak2019hscc.pdf},
month="April",
}
@inproceedings{kecskes2019destion,
author = {Kecskes, Tamas and Meijer, Patrik and Taylor T. Johnson and Lucas, Marcus},
title = {Demo: A Design Studio for Verification Tools},
booktitle = {Proceedings of the Workshop on Design Automation for CPS and IoT},
series = {DESTION '19},
year = {2019},
isbn = {978-1-4503-6699-1},
location = {Montreal, Quebec, Canada},
pages = {60--61},
numpages = {2},
doi = {10.1145/3313151.3314057},
acmid = {3314057},
publisher = {ACM},
address = {New York, NY, USA},
month="April",
}
@inproceedings{hartsell2019destion,
author = {Hartsell, Charles and Mahadevan, Nagabhushan and Ramakrishna, Shreyas and Dubey, Abhishek and Bapty, Theodore and Taylor T. Johnson and Koutsoukos, Xenofon and Sztipanovits, Janos and Karsai, Gabor},
title = {Model-based Design for CPS with Learning-enabled Components},
booktitle = {Proceedings of the Workshop on Design Automation for CPS and IoT},
series = {DESTION '19},
year = {2019},
isbn = {978-1-4503-6699-1},
location = {Montreal, Quebec, Canada},
pages = {1--9},
numpages = {9},
doi = {10.1145/3313151.3313166},
acmid = {3313166},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {cyber physical systems, machine learning, model based design},
month="April",
}
@Article{sogokon2018jar,
author="Sogokon, Andrew
and Jackson, Paul B.
and Taylor T. Johnson",
title="Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants",
journal="Journal of Automated Reasoning",
year="2018",
month="Nov",
day="24",
abstract="We describe a method for verifying the temporal property of persistence in non-linear hybrid systems. Given some system and an initial set of states, the method establishes that system trajectories always eventually evolve into some specified target subset of the states of one of the discrete modes of the system, and always remain within this target region. The method also computes a time-bound within which the target region is always reached. The approach combines flowpipe computation with deductive reasoning about invariants and is more general than each technique alone. We illustrate the method with a case study showing that potentially destructive stick-slip oscillations of an oil-well drill eventually die away for a certain choice of drill control parameters. The case study demonstrates how just using flowpipes or just reasoning about invariants alone can be insufficient and shows the richness of systems that one can handle with the proposed method, since the systems features modes with non-polynomial ODEs. We also propose an alternative method for proving persistence that relies solely on flowpipe computation.",
issn="1573-0670",
doi="10.1007/s10817-018-9497-x",
pdf = {http://www.taylortjohnson.com/research/sogokon2018jar.pdf},
}
@inproceedings{chowdhury2018sescps,
author = {Shafiul Azam Chowdhury and Lina Sera Varghese and Soumik Mohian and Taylor T. Johnson and Christoph Csallner},
title = {A curated corpus of {Simulink} models for model-based empirical studies},
booktitle = {Proc. 4th International Workshop on Software Engineering for
Smart Cyber-Physical Systems (SEsCPS)},
year = {2018},
month = may,
publisher = {ACM},
pages = {45--48},
pdf= {http://ranger.uta.edu/~csallner/papers/Chowdhury18Curated.pdf},
doi = {10.1145/3196478.3196484},
}
@inproceedings{johnson2018arch,
author = {Taylor T. Johnson},
title = {ARCH-COMP18 Repeatability Evaluation Report},
booktitle = {ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems},
editor = {Goran Frehse},
series = {EPiC Series in Computing},
volume = {54},
pages = {128--134},
year = {2018},
publisher = {EasyChair},
issn = {2398-7340},
url = {https://easychair.org/publications/paper/9J6v},
doi = {10.29007/n9t3},
}
@InProceedings{tran2018arch,
author = {Hoang-Dung Tran and Tianshu Bao and Taylor T. Johnson},
title = {Discrete-Space Analysis of Partial Differential Equations (PDEs) (Benchmark Proposal)},
booktitle = {5th Applied Verification for Continuous and Hybrid Systems Workshop (ARCH)},
year = {2018},
address = {Oxford, UK},
month = july,
pdf = {http://www.taylortjohnson.com/research/tran2018arch.pdf},
doi = {https://doi.org/10.29007/fvpp},
}
@InProceedings{musau2018arch_dae,
author = {Patrick Musau and Diego Manzanas Lopez and Hoang-Dung Tran and Taylor T. Johnson},
title = {Differential Algebraic Equations (DAEs) with Varying Index (Benchmark Proposal)},
booktitle = {5th Applied Verification for Continuous and Hybrid Systems Workshop (ARCH)},
year = {2018},
address = {Oxford, UK},
month = july,
pdf = {http://www.taylortjohnson.com/research/musau2018arch_dae.pdf},
doi = {https://doi.org/10.29007/4gj7},
}
@InProceedings{musau2018arch,
author = {Patrick Musau and Taylor T. Johnson},
title = {Continuous-Time Recurrent Neural Networks (CTRNNs) (Benchmark Proposal)},
booktitle = {5th Applied Verification for Continuous and Hybrid Systems Workshop (ARCH)},
year = {2018},
address = {Oxford, UK},
month = july,
pdf = {http://www.taylortjohnson.com/research/musau2018arch.pdf},
doi = {https://doi.org/10.29007/6czp},
}
@article{xiang2018tcyb,
author = {Weiming Xiang and Hoang-Dung Tran and Taylor T. Johnson},
title = {Reachable Set Computation and Safety Verification for Neural Networks with ReLU Activations},
journal = {In Submission},
year = {2018},
month = sept,
publisher = {IEEE},
file = {http://www.taylortjohnson.com/research/xiang2018tcyb.pdf},
owner = {tjohnson},
}
@article{xiang2019ust,
author="Xiang, Weiming
and Lopez, Diego Manzanas
and Musau, Patrick
and Taylor T. Johnson",
editor="Yu, Huafeng
and Li, Xin
and Murray, Richard M.
and Ramesh, S.
and Tomlin, Claire J.",
title="Reachable Set Estimation and Verification for Neural Network Models of Nonlinear Dynamic Systems",
bookTitle="Safe, Autonomous and Intelligent Vehicles",
year="2019",
publisher="Springer International Publishing",
pages="123--144",
abstract="Neural networks have been widely used to solve complex real-world problems. Due to the complex, nonlinear, non-convex nature of neural networks, formal safety and robustness guarantees for the behaviors of neural network systems are crucial for their applications in safety-critical systems. In this paper, the reachable set estimation and safety verification problems for Nonlinear Autoregressive-Moving Average (NARMA) models in the forms of neural networks are addressed. The neural networks involved in the model are a class of feed-forward neural networks called Multi-Layer Perceptrons (MLPs). By partitioning the input set of an MLP into a finite number of cells, a layer-by-layer computation algorithm is developed for reachable set estimation of each individual cell. The union of estimated reachable sets of all cells forms an over-approximation of the reachable set of the MLP. Furthermore, an iterative reachable set estimation algorithm based on reachable set estimation for MLPs is developed for NARMA models. The safety verification can be performed by checking the existence of non-empty intersections between unsafe regions and the estimated reachable set. Several numerical examples are provided to illustrate the approach.",
isbn="978-3-319-97301-2",
doi="10.1007/978-3-319-97301-2_7",
pdf = {http://www.taylortjohnson.com/research/xiang2018ust.pdf},
}
@InProceedings{xiang2018acc,
author = {Weiming Xiang and Hoang-Dung Tran and Joel Rosenfeld and Taylor T. Johnson},
title = {Reachable Set Estimation and Verification for a Class of Piecewise Linear Systems with Neural Network Controllers},
booktitle = {American Control Conference (ACC 2018), Special Session on Formal Methods in Controller Synthesis I},
year = {2018},
month = jun,
publisher = {IEEE},
pdf = {http://www.taylortjohnson.com/research/xiang2018acc.pdf},
owner = {tjohnson},
}
@ARTICLE{beg2018tsg,
author = {Omar Ali Beg and Luan Viet Nguyen and Taylor T. Johnson and Ali Davoudi},
ISSN = {},
language = {English},
title = {Signal Temporal Logic-based Attack Detection in DC Microgrids},
journal = {IEEE Transactions on Smart Grids (TSG)},
year = {2018},
month = apr,
publisher ={Institute of Electrical and Electronics Engineers (IEEE)},
doi={10.1109/TSG.2018.2832544},
pdf = {http://www.taylortjohnson.com/research/beg2018tsg.pdf},
}
@article{xiang2018tac_b,
author = {Weiming Xiang and Hoang-Dung Tran and Taylor T. Johnson},
title = {Nonconservative Lifted Convex Conditions for Stability of Discrete-Time Switched Systems under Minimum Dwell-Time Constraint},
journal = {IEEE Transactions on Automatic Control (TAC)},
year = {2018},
month = sept,
pdf = {http://www.taylortjohnson.com/research/xiang2018tac_b.pdf},
doi = {},
}
@article{xiang2018tnnls,
author = {Weiming Xiang and Hoang-Dung Tran and Taylor T. Johnson},
title = {Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks},
journal = {IEEE Transactions on Neural Networks and Learning Systems (TNNLS)},
year = {2018},
month = mar,
pdf = {http://taylortjohnson.com/research/xiang2018tnnls.pdf},
doi = {10.1109/TNNLS.2018.2808470},
}
@InProceedings{nguyen2018adhs,
author = {Luan-Viet Nguyen and Bardh Hoxha and Georgios Fainekos and Taylor T. Johnson},
title = {Mission Planning for Multiple Vehicles with Temporal Specifications using {UxAS}},
booktitle = {IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2018)},
year = {2018},
month = jul,
publisher = {IFAC},
file = {http://www.taylortjohnson.com/research/nguyen2018adhs.pdf},
owner = {tjohnson},
doi = {j.ifacol.2018.08.012},
}
@InProceedings{tran2018adhs,
author = {Hoang-Dung Tran and Weiming Xiang and Stanley Bak and Taylor T. Johnson},
title = {Reachability Analysis for One Dimensional Linear Parabolic Equation},
booktitle = {IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2018)},
year = {2018},
month = jul,
publisher = {IFAC},
file = {http://www.taylortjohnson.com/research/tran2018adhs.pdf},
owner = {tjohnson},
doi = {j.ifacol.2018.08.023},
}
@InProceedings{chowdhury2018icse,
author = {Shafiul Azam Chowdhury and Soumik Mohian and Sidharth Mehra and Siddhant Gawsane and Taylor T. Johnson and Christoph Csallner },
title = {Automatically Finding Bugs in a Commercial Cyber-Physical System Development Tool Chain With SLforge},
booktitle = {40th International Conference on Software Engineering (ICSE 2018)},
year = {2018},
month = may,
publisher = {ACM},
file = {http://www.taylortjohnson.com/research/chowdhury2018icse.pdf},
owner = {tjohnson},
doi = {10.1145/3183440.3183455},
}
@article{nguyen2018tcps,
Title = {Cyber-Physical Specification Mismatches},
Author = {Luan Viet Nguyen and Khaza Hoque and Stanley Bak and Steven Drager and Taylor T. Johnson},
journal = {ACM Transactions on Cyber-Physical Systems (TCPS)},
pdf = {http://www.taylortjohnson.com/research/nguyen2018tcps.pdf},
Owner = {tjohnson},
year = {2018},
doi = {10.1145/3170500},
}
@article{xiang2018tac_a,
author = {Weiming Xiang and Hoang-Dung Tran and Taylor T. Johnson},
title = {Robust Exponential Stability and Disturbance Attenuation for Discrete-Time Switched Systems under Arbitrary Switching},
journal = {IEEE Transactions on Automatic Control (TAC)},
year = {2018},
month = may,
pdf = {http://www.taylortjohnson.com/research/xiang2018tac_a.pdf},
doi = {10.1109/TAC.2017.2748918},
}
@InProceedings{beg2017fac,
author = {Omar Ali Beg and Luan Viet Nguyen and Ali Davoudi and Taylor T. Johnson},
title = {Computer-Aided Formal Verification of Power Electronics Circuits},
booktitle = {8th International Workshop on Frontiers in Analog CAD (FAC)},
year = {2017},
address = {Frankfurt, Germany},
month = july,
pdf = {http://www.taylortjohnson.com/research/beg2017fac.pdf},
}
@InProceedings{sogokon2017emsoft,
author = {Andrew Sogokon and Khalil Ghorbhal and Taylor T. Johnson},
title = {Operational models of piecewise-smooth systems},
booktitle = {17th ACM SIGBED International Conference on Embedded Software (EMSOFT 2017)},
year = {2017},
month = oct,
owner = {tjohnson},
doi = {},
acmid = {},
pdf = {http://www.taylortjohnson.com/research/sogokon2017emsoft.pdf},
}
@InProceedings{nguyen2017memocode,
author = {Luan Viet Nguyen and James Kapinski and Xiaoqing Jin and Jyotirmoy Deshmukh and Taylor T. Johnson},
title = {Hyperproperties of real-valued signals},
booktitle = {15th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2017)},
year = {2017},
month = oct,
publisher = {IEEE},
file = {http://www.taylortjohnson.com/research/nguyen2017memocode.pdf},
owner = {tjohnson},
}
@InProceedings{johnson2017arch,
author = {Taylor T. Johnson},
title = {ARCH-COMP17 Repeatability Evaluation Report},
booktitle = {4th Applied Verification for Continuous and Hybrid Systems Workshop (ARCH)},
year = {2017},
address = {Pittsburgh, PA},
month = apr,
pdf = {http://www.taylortjohnson.com/research/johnson2017arch.pdf},
}
@InProceedings{beg2017arch,
author = {Omar Ali Beg and Ali Davoudi and Taylor T. Johnson},
title = {Reachability Analysis of Transformer-Isolated DC-DC Converters (Benchmark Proposal)},
booktitle = {4th Applied Verification for Continuous and Hybrid Systems Workshop (ARCH)},
year = {2017},
address = {Pittsburgh, PA},
month = apr,
pdf = {http://www.taylortjohnson.com/research/beg2017arch.pdf},
}
@InProceedings{tran2017arch,
author = {Hoang-Dung Tran and Luan Viet Nguyen and Weiming Xiang and Taylor T. Johnson},
title = {Distributed Autonomous Systems (Benchmark Proposal)},
booktitle = {4th Applied Verification for Continuous and Hybrid Systems Workshop (ARCH)},
year = {2017},
address = {Pittsburgh, PA},
month = apr,
pdf = {http://www.taylortjohnson.com/research/tran2017arch.pdf},
}
@article{bak2019sttt,
author = {Bak, Stanley and Beg, Omar Ali and Bogomolov, Sergiy and Taylor T. Johnson and Nguyen, Luan Viet and Schilling, Christian},
title = {Hybrid Automata: From Verification to Implementation},
journal = {Int. Journal on Software Tools for Technology Transfer (STTT)},
issue_date = {February 2019},
volume = {21},
number = {1},
month = feb,
year = {2019},
issn = {1433-2779},
pages = {87--104},
numpages = {18},
doi = {10.1007/s10009-017-0458-1},
acmid = {3316202},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
keywords = {Hybrid automata, Model-based design, Simulink/Stateflow},
software = {http://github.com/verivital/hyst},
pdf = {http://www.taylortjohnson.com/research/bak2017sttt.pdf}
}
@article{xiang2017tac,
author = {Weiming Xiang and Hoang-Dung Tran and Taylor T. Johnson},
title = {Output Reachable Set Estimation for Switched Linear Systems and Its Application in Safety Verification},
journal = {IEEE Transactions on Automatic Control (TAC)},
year = {2017},
pdf = {http://www.taylortjohnson.com/research/xiang2017tac.pdf},
doi = {10.1109/TAC.2017.2692100},
}
@article{tran2017deds,
author = {Hoang-Dung Tran and Luan Viet Nguyen and Weiming Xiang and Taylor T. Johnson},
title = {Order-reduction abstractions for safety verification of high-dimensional linear systems},
journal = {Discrete Event Dynamic Systems (DEDS)},
year = {2017},
pdf = {http://www.taylortjohnson.com/research/tran2017deds.pdf},
doi = {10.1007/s10626-017-0244-y},
url = {http://rdcu.be/q8Xd},
}
@ARTICLE{xiang2017iet,
author = {Weiming Xiang and Taylor T. Johnson},
keywords = {robust sampling;event-triggering condition;continuous-time switched linear system;feedback control;periodical sampling scheme;asymptotic stability;event-triggered control;},
ISSN = {1751-8644},
language = {English},
abstract = {The event-triggered control problem for switched linear system is addressed in this study. The periodical sampling scheme and event-triggering condition are incorporated in the closed-loop. The feedback control updates its value only at sampling instants as long as event-triggering condition is satisfied as well. In addition, the switchings are only allowed to occur at sampling instants and meanwhile the switching condition is satisfied. Three equivalent sufficient conditions are proposed to ensure the asymptotic stability of switched systems. In particular, one condition has a promising feature of affineness in system matrices, and as a consequence, it is extended to robust sampling case and L 2 -gain analysis. Several examples are provided to illustrate the authors results.},
title = {Event-triggered control for continuous-time switched linear systems},
journal = {IET Control Theory and Applications},
pdf = {http://www.taylortjohnson.com/research/xiang2017iet.pdf},
year = {2017},
month = {February},
publisher ={Institution of Engineering and Technology},
copyright = {The Institution of Engineering and Technology},
# url = {http://digital-library.theiet.org/content/journals/10.1049/iet-cta.2016.0672},
doi = {10.1049/iet-cta.2016.0672},
}
%@InProceedings{xiang2017cdc,
% author = {Weiming Xiang and Taylor T. Johnson},
% title = {},
% booktitle = {Proceedings of the 56th IEEE Conference on Decision and Control (CDC 2017)},
% year = {2017},
% month = dec,
% owner = {tjohnson},
% doi = {},
%}
@ARTICLE{beg2017tie,
author = {Omar Ali Beg and Houssam Abbas and Taylor T. Johnson and Ali Davoudi},
ISSN = {},
language = {English},
title = {Model Validation of PWM DC-DC Converters },
journal = {IEEE Transactions on Industrial Electronics. (TIE)},
year = {2017},
month = jun,
publisher ={Institute of Electrical and Electronics Engineers (IEEE)},
doi = {10.1109/TIE.2017.2688961},
pdf = {http://www.taylortjohnson.com/research/beg2017tie.pdf},
}
@InProceedings{xiang2017acc,
author = {Weiming Xiang and Taylor T. Johnson},
title = {On Reachable Set Estimation for Discrete-Time Switched Linear Systems under Arbitrary Switching},
booktitle = {30th IEEE American Control Conference (ACC 2017)},
year = {2017},
month = july,
owner = {tjohnson},
doi = {10.23919/ACC.2017.7963654},
acmid = {},
pdf = {http://www.taylortjohnson.com/research/xiang2017acc.pdf},
}
@InProceedings{sogokon2017nfm,
author = {Andrew Sogokon and Paul Jackson and Taylor T. Johnson},
title = {Verifying safety and persistence properties of hybrid systems using flowpipes and continuous invariants},
booktitle = {9th NASA Formal Methods Symposium (NFM 2017)},
year = {2017},
month = may,
owner = {tjohnson},
doi = {10.1007/978-3-319-57288-8_14},
acmid = {},
pdf = {http://www.taylortjohnson.com/research/sogokon2017nfm.pdf},
}
@InProceedings{nguyen2017hscc,
author = {Luan Viet Nguyen and James Kapinski and Xiaoqing Jin and Jyotirmoy Deshmukh and Ken Butts and Taylor T. Johnson},
title = {Abnormal Data Classification Using Time-Frequency Temporal Logic},
booktitle = {20th Intl. Conf. on Hybrid Systems: Computation and Control (HSCC 2017)},
year = {2017},
month = apr,
publisher = {ACM},
owner = {tjohnson},
doi = {10.1145/3049797.3049809},
acmid = {3049809},
pdf = {http://www.taylortjohnson.com/research/nguyen2017hscc.pdf},
}
@ARTICLE{beg2017tii,
author={Omar Ali Beg and Taylor T. Johnson and Ali Davoudi},
journal={IEEE Transactions on Industrial Informatics},
title={Detection of False-data Injection Attacks in Cyber-Physical DC Microgrids},
year={2017},
volume={},
number={},
pages={},
abstract={Power electronics-intensive DC microgrids use increasingly complex software-based controllers and communication networks. They are evolving into cyber-physical systems (CPS) with sophisticated interactions between physical and computational processes, making them vulnerable to cyber attacks. This work presents a framework to detect possible false-data injection attacks (FDIA) in cyber-physical DC microgrids. The detection problem is formalized as identifying a change in sets of inferred candidate invariants. Invariants are microgrids properties that do not change over time. Both the physical plant and the software controller of CPS can be described as Simulink/Stateflow (SLSF) diagrams. The dynamic analysis infers the candidate invariants over the input/output variables of SLSF components. The reachability analysis generates the sets of reachable states (reach sets) for the CPS modeled as hybrid automata. The candidate invariants that contain the reach sets are called the actual invariants. The candidate invariants are then compared with the actual invariants, and any mismatch indicates the presence of FDIA. To evaluate the proposed methodology, the hybrid automaton of a DC microgrid, with a distributed cooperative control scheme, is presented. The reachability analysis is performed to obtain the reach sets and, hence, the actual invariants. Moreover, a prototype tool, HYbrid iNvariant GEneratoR (Hynger), is extended to instrument SLSF models, obtain candidate invariants, and identify FDIA.},
keywords={Automata;Communication networks;Hybrid power systems;Microgrids;Phasor measurement units;Security;Topology;Cyber-physical systems;dc microgrid;distributed control;false-data injection attack;hybrid automaton},
doi={10.1109/TII.2017.2656905},
ISSN={1551-3203},
month={},
pdf={http://www.taylortjohnson.com/research/beg2017tii.pdf},
}
@InProceedings{chowdhury2016cyphy,
author = {Shafiul Azam Chowdhury and Taylor T. Johnson and Christoph Csallner},
title = {CyFuzz: : A Differential Testing Framework for Cyber-Physical Systems Development Environments},
booktitle = {6th International Workshop Workshop on Design, Modeling and Evaluation of Cyber Physical Systems (CyPhy 2016)},
year = {2016},
address = {Pittsburgh, PA},
month = aug,
doi = {10.1007/978-3-319-51738-4_4},
pdf = {http://www.taylortjohnson.com/research/chowdhury2016cyphy.pdf},
}
@inproceedings{xiang2016cdc,
author = {Weiming Xiang and Hoang-Dung Tran and Taylor T. Johnson},
title = {Reachable Set Estimation and Control for Switched Linear Systems with Dwell-Time Restriction},
year = {2016},
booktitle = {Proceedings of the 55th IEEE Conference on Decision and Control (CDC 2016)},
address = {Las Vegas, NV, USA},
month = dec,
# pages = {2687--2692},
# gsid = {14666544104064248628},
doi = {10.1109/CDC.2016.7799387},
# 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/xiang2016cdc.pdf},
}
@incollection{sogokon2016fm,
author = {Andrew Sogokon and Khalil Ghorbal and Taylor T. Johnson},
title = {Decoupled simulating abstractions of non-linear ordinary differential equations},
year = {2016},
booktitle = {Proceedings of the 21st International Symposium on Formal Methods (FM 2016)},
address = {Limassol, Cyprus},
month = dec,
# isbn = {978-3-642-32758-2},
# volume = {7436},
# gsid = {6661230319939383532},
# editor = {Giannakopoulou, Dimitra and M\'{e}ry, Dominique},
doi = {10.1007/978-3-319-48989-6_38},
# publisher = {Springer Berlin Heidelberg},
# pages = {252--266},
abstract = {},
pdf = {http://www.taylortjohnson.com/research/sogokon2016fm.pdf},
}
@inproceedings{duggirala2016msc,
author = {Parasara Sridhar Duggirala and Chuchu Fan and Matthew Potok and Bolun Qi and Sayan Mitra and Mahesh Viswanathan and Stanley Bak and Sergiy Bogomolov and Taylor T. Johnson and Luan Viet Nguyen and Christian Schilling and Andrew Sogokon and Hoang-Dung Tran and Weiming Xiang},
title = {Tutorial: Software Tools for Hybrid Systems Verification, Transformation, and Synthesis: C2E2, HyST, and TuLiP},
year = {2016},
booktitle = {Proceedings of the IEEE Multi-Conference on Systems and Control (MSC 2016)},
address = {Las Vegas, NV, USA},
month = sep,
# pages = {2687--2692},
# gsid = {14666544104064248628},
doi = {10.1109/CCA.2016.7587948},
# 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/duggirala2016msc.pdf},
}
@inproceedings{sardar2016nfm,
author="Sardar, Muhammad Usama
and Afaq, Nida
and Khaza Anuarul Hoque
and Taylor T. Johnson
and Osman Hasan",
editor="Rayadurgam, Sanjai
and Tkachuk, Oksana",
title="Probabilistic Formal Verification of the SATS Concept of Operation",
booktitle="Proceedings of the 8th NASA Formal Methods (NFM 2016) International Symposium",
year="2016",
month = june,
publisher="Springer International Publishing",
pages="191--205",
isbn="978-3-319-40648-0",
doi="10.1007/978-3-319-40648-0_15",
pdf = {http://www.taylortjohnson.com/research/sardar2016nfm.pdf},
}
# , NFM 2016, Minneapolis, MN, USA, June 7-9, 2016,
@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},
doi = {10.1145/2883817.2883837},
acmid = {2883837},
pdf = {http://www.taylortjohnson.com/research/bak2016hscc.pdf},
}
@InProceedings{beg2016arch,
author = {Omar Ali Beg and Ali Davoudi and Taylor T. Johnson},
title = {Charge Pump Phase-Locked Loops and Full Wave Rectifiers for Reachability Analysis (Benchmark Proposal)},
booktitle = {3rd Applied Verification for Continuous and Hybrid Systems Workshop (ARCH)},
year = {2016},
address = {Vienna, Austria},
month = apr,
pdf = {http://www.taylortjohnson.com/research/beg2016arch.pdf},
}
@InProceedings{sogokon2016arch,
author = {Andrew Sogokon and Khalil Ghorbal and Taylor T. Johnson},
title = {Non-linear Continuous Systems for Safety Verification (Benchmark Proposal)},
booktitle = {3rd Applied Verification for Continuous and Hybrid Systems Workshop (ARCH)},
year = {2016},
address = {Vienna, Austria},
month = apr,
pdf = {http://www.taylortjohnson.com/research/sogokon2016arch.pdf},
}
@InProceedings{tran2016arch,
author = {Hoang-Dung Tran and Luan Viet Nguyen and Taylor T. Johnson},
title = {Large-Scale Linear Systems from Order-Reduction (Benchmark Proposal)},
booktitle = {3rd Applied Verification for Continuous and Hybrid Systems Workshop (ARCH)},
year = {2016},
address = {Vienna, Austria},
month = apr,
pdf = {http://www.taylortjohnson.com/research/tran2016arch.pdf},
}
@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/johnson2016tecs.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},
}
@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{bogomolov2016sttt,
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 = {2016},
journal = {Software Tools for Technology Transfer (STTT)},
publisher = {Springer},
address = {},
month = aug,
pages = {},
doi = {10.1007/s10009-015-0393-y},
gsid = {4980588848043524788},
abstract = {},
volume = {18},
issue = {4},
software = {http://www2.informatik.uni-freiburg.de{\~}bogom/sttt2015/},
pdf = {http://www.taylortjohnson.com/research/bogomolov2016sttt.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 = {2nd 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 = {2nd 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/},
}