Research

Research Interests

  • Cyber-physical systems: real-time, networked embedded control systems and software
  • Hybrid systems and distributed systems
  • Software engineering, formal methods, and formal verification
  • Reliability and fault-tolerance
  • Application areas including transportation systems (aerospace and automotive), robotics, power and energy

Research Support

We gratefully acknowledge the support of our research by AFOSR, AFRL, NSF (CISE CCF/SHF, CNS/CPS; ENG ECCS/EPCN), NVIDIA, and USDOT. More details on the projects are available in my CV.

Active Research Projects

  • "Reusable Formal Verification for Cyber-Physical Systems," Air Force Office of Scientific Research (AFOSR), Young Investigator Program (YIP), 2016-2019, Award Number: FA9550-16-1-0246, Role: Sole PI.
  • "Cyber-Physical Systems Specification Mismatch and Safe Upgrades," Air Force Office of Scientific Research (AFOSR), 2015-2018, Award Number: FA9550-15-1-0258, Role: Sole PI.
  • "SHF: Small: Automating Improvement of Development Environments for Cyber-Physical Systems (AIDE-CPS)," NSF CISE CCF/SHF, 2015-2018, Award Number: 1527398, Role: PI, with Co-PI Christoph Csallner
  • "App-Based Crowd Sourcing of Bicycle and Pedestrian Conflict Data," University Transportation Center for Livable Communities (TRCLC), US Department of Transportation (USDOT), 2015-2016, Role: Co-PI, with PI Stephen Mattingly and Co-PI Colleen Casey.
  • "Real-time Ab Initio Modeling of Electric Machines," NSF ENG ECCS/EPCN, 2015-2018, Award Number: 1509804, Role: Co-PI, with PI Ali Davoudi and Co-PI David Levine
  • "Formal Modeling of Emergence in Distributed Cyber-Physical Systems," Air Force Research Laboratory (AFRL), Trusted Autonomy and Verification and Validation (V&V), Integrated Command and Control, BAA-10-01-RIKA, 2015-2017, Award Number: FA8750-15-1-0105, Role: Sole PI
  • "CRII: CPS: Safe Cyber-Physical Systems Upgrades," NSF CISE CNS/CPS, 2015-2017, Award Number: 1464311, Role: Sole PI

Program Committees and Conference Organization

  • International Conference on Parallel Processing (ICPP), Cyber-Physical Systems Track: 2016
  • ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS), Work-in-Progress/Demo Co-Chair at CPS Week 2016: 2016
  • Applied Verification for Continuous and Hybrid Systems (ARCH), Evalation Chair, at CPS Week 2016: 2016
  • ACM International Conference on Hybrid Systems: Computation and Control (HSCC) at CPS Week 2016: 2016
  • IEEE Real-Time Systems Symposium (RTSS): 2015
  • IEEE Control and Modeling for Power Electronics (COMPEL): 2015
  • Applied Verification for Continuous and Hybrid Systems (ARCH), CPS Week 2015: 2015
  • Runtime Verification (RV): 2014
  • Coordinated Science Lab Symposium on Emerging Topics in Control and Modelling: 2012

Research Links

Software and Tools

We develop a large amount of research software, particularly verification tool prototypes. Some code is available on my Bitbucket account and the Verivital Bitbucket account, with limited developed on the Verivital GitHub account. Particular tools are:

Publications

Journal Articles (5)

2016
[J5], , , , "Real-Time Reachability for Verified Simplex Design", In ACM Transactions on Embedded Computing Systems (TECS), ACM, vol. 15, no. 2, New York, NY, USA, pp. 26:1–26:27, 2016, February. [bibtex] [pdf] [doi]
2015
[J4], , , , , , , , "Guided Search for Hybrid Systems Based on Coarse-Grained Space Abstractions", In Software Tools for Technology Transfer (STTT), Springer, , pp. , 2015, August. [abstract] [software / source code] [bibtex] [pdf] [doi] [cites]
[J3], , "Safe and Stabilizing Distributed Multi-Path Cellular Flows", In Theoretical Computer Science, Elsevier, vol. , no. , , pp. 1–46, 2015, February. [abstract] [software / source code] [bibtex] [pdf] [doi]
2014
[J2], , , "Virtual Prototyping for Distributed Control of a Fault-Tolerant Modular Multilevel Inverter for Photovoltaics", In IEEE Transactions on Energy Conversion, vol. 29, , pp. 841–850, 2014, December. (arxiv preprint) [abstract] [bibtex] [pdf] [doi] [cites]
2011
[J1], , "Safe Flocking in Spite of Actuator Faults using Directional Failure Detectors", In Journal of Nonlinear Systems and Applications, Watam Press Inc., vol. 2, no. 1-2, Waterloo, Ontario, Canada, pp. 73–95, 2011, April. (pdf (publisher), doi) [abstract] [bibtex] [pdf] [cites]

Conference Papers (21)

2016
[C21], , , , , "Scalable Static Hybridization Methods for Analysis of Nonlinear Systems", In 19th Intl. Conf. on Hybrid Systems: Computation and Control (HSCC 2016), ACM, 2016, April. [bibtex]
2015
[C20], , "Periodically-Scheduled Controller Analysis using Hybrid Systems Reachability and Continuization", In 36th IEEE Real-Time Systems Symposium (RTSS 2015), IEEE Computer Society, San Antonio, Texas, 2015, December. [bibtex] [pdf]
[C19], , , , "Runtime Verification of Model-based Development Environments", In 15th International Conference on Runtime Verification (RV 2015), Vienna, Austria, 2015, September. [bibtex] [pdf]
[C18], , , "A Survey of Electrical and Electronic (E/E) Notifications for Motor Vehicles", In 24th NHTSA International Technical Conference on the Enhanced Safety of Vehicles (ESV), Gothenburg, Sweden, pp. 1–15, 2015, June. (publisher PDF) [abstract] [bibtex] [pdf] [doi] [cites]
[C17], , , "HyST: A Source Transformation and Translation Tool for Hybrid Automaton Models", In 18th International Conference on Hybrid Systems: Computation and Control (HSCC 2015), ACM, Seattle, Washington, 2015, April. (Hyst software tool) [software / source code] [bibtex] [pdf]
[C16], , , "Cyber-Physical Specification Mismatch Identification with Dynamic Analysis", In 6th International Conference on Cyber-Physical Systems (ICCPS 2015), ACM/IEEE, Seattle, Washington, 2015, April. (Hynger software tool) [software / source code] [bibtex] [pdf]
[C15], , , , "Verified Planar Formation Control Algorithms by Composition of Primitives", In AIAA SciTech, AIAA, Kissimmee, Florida, 2015, January. [bibtex] [pdf]
2014
[C14], , , , "Real-Time Reachability for Verified Simplex Design", In 35th IEEE Real-Time Systems Symposium (RTSS 2014), IEEE Computer Society, Rome, Italy, 2014, December. [slides] [bibtex] [pdf]
[C13], , "Anonymized Reachability of Hybrid Automata Networks", In Proceedings of the 12th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2014), Florence, Italy, pp. , 2014, September. [abstract] [bibtex] [pdf] [doi] [cites]
2013
[C12], , "Invariant Synthesis for Verification of Parameterized Cyber-Physical Systems with Applications to Aerospace Systems", In Proceedings of the AIAA Infotech at Aerospace Conference (AIAA Infotech 2013) (, ed.), AIAA, vol. , Boston, MA, pp. , 2013, August. [abstract] [bibtex] [pdf] [doi] [cites]
[C11], , , , , , , , "Abstraction-Based Guided Search for Hybrid Systems", In Proceedings of the 20th International SPIN Symposium on Model Checking of Software (SPIN 2013), Stony Brook, New York, USA, pp. , 2013, July. [abstract] [bibtex] [pdf] [doi] [cites]
[C10], , , "Reachability Analysis of Closed-Loop Switching Power Converters", In Proceedings of the 4th IEEE Power and Energy Conference at Illinois (PECI 2013), Urbana, Illinois, USA, pp. , 2013, February. [abstract] [bibtex] [pdf] [doi] [cites]
2012
[C9], , , , "Static and Dynamic Analysis of Timed Distributed Traces", In Proceedings of the 33rd IEEE Real-Time Systems Symposium (RTSS 2012), San Juan, Puerto Rico, pp. 173–182, 2012, December. [abstract] [bibtex] [pdf] [doi] [cites]
[C8], , , , , "Satellite Rendezvous and Conjunction Avoidance: Case Studies in Verification of Nonlinear Hybrid Systems", Chapter in Proceedings of the 18th International Conference on Formal Methods (FM 2012) (Dimitra Giannakopoulou, Dominique Méry, eds.), Springer Berlin Heidelberg, vol. 7436, Paris, France, pp. 252–266, 2012, August. [abstract] [bibtex] [pdf] [doi] [cites]
[C7], , "A Small Model Theorem for Rectangular Hybrid Automata Networks", In 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), Stockholm, Sweden, pp. , 2012, June. (Best Paper Award for DisCoTec, Passel tool and specification source, Passel tool overview) [abstract] [software / source code] [bibtex] [pdf] [doi] [cites]
[C6], , "Parameterized Verification of Distributed Cyber-Physical Systems: An Aircraft Landing Protocol Case Study", In Proceedings of the 3rd ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS 2012), Beijing, China, pp. 161–170, 2012, April. (source code) [abstract] [bibtex] [pdf] [doi] [cites]
[C5], , , "Design Verification Methods for Switching Power Converters", In Proceedings of the 3rd IEEE Power and Energy Conference at Illinois (PECI 2012), Urbana, Illinois, USA, pp. 1–6, 2012, February. [abstract] [bibtex] [pdf] [doi] [cites]
2011
[C4], , , "Stability of Digitally Interconnected Linear Systems", In Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference (CDC ECC 2011), Orlando, Florida, USA, pp. 2687–2692, 2011, December. [abstract] [bibtex] [pdf] [doi] [cites]
[C3], , "Turbo-Alternator Stalling Protection using Available Power Estimate", In Proceedings of the 2nd Annual IEEE Power and Energy Conference at Illinois (PECI 2011), Urbana, Illinois, USA, 2011, February. (Best Paper Award) [abstract] [bibtex] [pdf] [doi] [cites]
2010
[C2], , "Safe Flocking in Spite of Actuator Faults", Chapter in 12th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2010) (Shlomi Dolev, Jorge Cobb, Michael Fischer, Moti Yung, eds.), Springer Berlin / Heidelberg, vol. 6366, pp. 588–602, 2010, September. [abstract] [bibtex] [pdf] [doi] [cites]
[C1], , , "Safe and Stabilizing Distributed Cellular Flows", In 30th IEEE International Conference on Distributed Computing Systems (ICDCS 2010), Genoa, Italy, pp. 577–578, 2010, June. [abstract] [bibtex] [pdf] [doi] [cites]

Workshop Papers (6)

2015
[W6], , , , "Quantified Bounded Model Checking for Rectangular Hybrid Automata", In 9th International Workshop on Constraints in Formal Verification (CFV 2015), Austin, Texas, 2015, November. [bibtex] [pdf]
[W5], , , "HyST: A Source Transformation and Translation Tool for Hybrid Automaton Models", In 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), San Francisco, California, 2015, July. [bibtex] [pdf]
[W4], , , "Benchmark: A Nonlinear Reachability Analysis Test Set from Numerical Analysis", In Applied Verification for Continuous and Hybrid Systems Workshop (ARCH 2015), Seattle, Washington, pp. , 2015, April. (model source code) [abstract] [bibtex] [pdf] [doi] [cites]
[W3], , , , "Benchmark Generator for Stratified Controllers of Tank Networks", In Applied Verification for Continuous and Hybrid Systems Workshop (ARCH 2015), Seattle, Washington, pp. , 2015, April. (model source code) [abstract] [bibtex] [pdf] [doi] [cites]
2014
[W2], , "Benchmark: DC-to-DC Switched-Mode Power Converters (Buck Converters, Boost Converters, and Buck-Boost Converters)", In Applied Verification for Continuous and Hybrid Systems Workshop (ARCH 2014), Berlin, Germany, pp. , 2014, April. [abstract] [software / source code] [bibtex] [pdf] [doi] [cites]
[W1], , , , , , , "Model-Based Design and Analysis of a Reconfigurable Continuous-Culture Bioreactor (Work-in-Progress)", In Fourth ACM Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems (CyPhy 2014), Berlin, Germany, pp. , 2014, April. (ACM Authorizer) [abstract] [bibtex] [pdf] [doi] [cites]

Theses (2)

2013
[TH2], "Uniform Verification of Safety for Parameterized Networks of Hybrid Automata", PhD thesis, Department of Electrical and Computer Engineering, University of Illinois at Urbana-Champaign, Urbana, IL 61801, USA, 2013, August. (doi) [abstract] [software / source code] [bibtex] [pdf] [cites]
2010
[TH1], "Fault-Tolerant Distributed Cyber-Physical Systems: Two Case Studies", Master's thesis, Department of Electrical and Computer Engineering, University of Illinois at Urbana-Champaign, Urbana, IL 61801, USA, 2010, May. (doi) [abstract] [bibtex] [pdf] [cites]

Technical Reports (1)

2010
[R1], , "Safe and Stabilizing Distributed Flocking In Spite of Actuator Faults", UILU-ENG-10-2204 (CRHC-10-02), University of Illinois at Urbana-Champaign, no. UILU-ENG-10-2204 (CRHC-10-02), Urbana, IL 61801, USA, 2010, May. [bibtex] [pdf]

Demos/Posters/Abstracts (3)

2015
[D3], , , , "HyRG: a random generation tool for affine hybrid automata", Presented at 18th International Conference on Hybrid Systems: Computation and Control (HSCC 2015) Poster/Demo Session, 2015, April. (HyRG Software Tool) [software / source code] [bibtex] [pdf] [doi] [cites]
2009
[D2], , "Handling Failures in Cyber-Physical Systems: Potential Directions", Presented at RTSS 2009 PhD Student Forum, 2009, December. (Award for Most Interesting Cyber-Physical Systems Research Problem) [abstract] [slides] [bibtex] [pdf] [cites]
[D1], , "Power Usage of Time and Event-Triggered Paradigms: A Case Study", Presented at RTAS 2009 Poster Session, 2009, April. [abstract] [slides] [software / source code] [bibtex] [pdf] [cites]

The entire BiBteX file is available here.

Copyright Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.