News and About



Brief Bio: Taylor T. Johnson is an Assistant Professor of Computer Science and Engineering at the University of Texas at Arlington (since September 2013), where he directs the Verification and Validation for Intelligent and Trustworthy Autonomy Laboratory (VeriVITAL). Taylor completed an PhD in Electrical and Computer Engineering (ECE) at the University of Illinois at Urbana-Champaign in 2013, where he worked in the Coordinated Science Laboratory with Prof. Sayan Mitra. Taylor completed an MSc in ECE at Illinois in 2010, earned a BSEE from Rice University in 2008, received the AFOSR Summer Faculty Fellowship Program (SFFP) award to visit the Air Force Research Laboratory (AFRL)'s Information Directorate in 2015, was a Visiting Faculty Research Program (VFRP) participant at AFRL's Information Directorate in 2014, and was a visiting graduate research assistant through the SFFP at AFRL's Space Vehicles Directorate at Kirtland Air Force Base in 2011. Taylor worked in industry for Schlumberger at various times between 2005 and 2010 helping develop new downhole embedded control systems. Taylor's research focus is developing formal verification techniques and software tools for cyber-physical systems (CPS). Taylor has published over two-dozen papers on these methods and their applications across domain areas like power and energy systems, aerospace, transportation systems, and robotics, two of which were recognized with best paper awards, from the IEEE and IFIP, respectively. Taylor's research aims to develop reliable embedded and cyber-physical systems by advancing and applying techniques and tools from formal methods, control theory, embedded systems, and software engineering. Taylor's research is supported by AFRL, AFOSR, NSF (CISE CCF/SHF, CNS/CPS; ENG ECCS/EPCN), NVIDIA, and USDOT.

Physical Location:
Taylor Johnson
Department of Computer Science and Engineering
Engineering Research Building, Room 559
University of Texas at Arlington
500 UTA Blvd.
Arlington, Texas 76010

Email: taylor.johnson AT nospam DOT gmail DOT com
Phone (Office): 817-272-3610 (Note: voicemail is never checked, email me if you miss me)
Phone (Laboratory): 817-272-7409
Fax: 817-272-3784

Mailing Address:
Taylor Johnson
Box 19015
500 UTA Blvd., ERB 640
Department of Computer Science and Engineering
University of Texas at Arlington
Arlington, Texas 76019-0015

Lab Location:
Engineering Research Building, Room 105B

Taylor T. Johnson
high resolution; talk bio

Research Synopsis: Defects stemming from the interaction of software and physical processes in embedded and cyber-physical systems (CPS) are rampant and are becoming more prevalent as exemplified by frequent product recalls in industries such as automotive, medical devices, and consumer products. To address this challenge to ensure CPS meet the strictest safety, security, and reliability requirements, our research agenda is to develop formal verification techniques and tools for CPS, building on and advancing foundational results in formal methods, control theory, distributed systems, and real-time/embedded systems. For example, one technique we've developed is for verifying safety properties of distributed CPS where arbitrarily many agents participate in a protocol, such as in air traffic control protocols, network protocols, networked control systems, and swarm robotics. This uniform verification technique for parameterized systems verifies systems with arbitrarily many participants, and relies on a small model theorem we developed, which allows for reasoning about arbitrarily large instances using finite instances. Our implementation of this technique in an SMT-based verification software tool (called Passel) allowed us to prove automatically, that in one of NASA's conceptual air traffic control protocols in NextGen, all aircraft maintain a safe separation, regardless of the number of aircraft involved in the protocol. Other techniques we have developed include automated abstractions implemented in our Hyst tool, mixtures of static and dynamic analysis for Simulink/Stateflow models to infer cyber-physical specifications as implemented in our Hynger tool, the first reachability algorithm for hybrid automata that may be implemented with real-time guarantees, among others. Our verification methods have been applied across numerous CPS domains, including automotive, aerospace, power/energy systems, and robotics.

CV / Resume

My detailed curriculum vitae is available for viewing as a PDF file. (Please note, I have removed some information from the files posted here for privacy concerns. If you would like a complete copy, please contact me.)

Prospective Students: I am looking for ambitious and motivated graduate and undergraduate students. Research Assistantships (RAs) are available for competitive candidates. If you are a UTA student looking for an advisor, or if you are interested in applying to UTA for graduate studies in Computer Science and Engineering, please email me with your resume/CV (and your transcript if at UTA) if you are interested to do research in formal methods (especially), hybrid systems, embedded systems / cyber-physical systems, software engineering, distributed systems, and related areas. I also need strong programmers at all levels, especially in Java, C/C++, and Matlab. If you do not include your resume/CV (and transcript if at UTA), I will not respond. As I receive many such requests, I cannot reply to every email, but do my best to reply to competitive applicants.