Taylor Johnson & Adam Zimmerman

Version 1 by Fan Wu
on Jan 27, 2012 21:23.

compared with
Current by Fan Wu
on Jan 27, 2012 21:28.

This line was removed.
This word was removed. This word was added.
This line was added.

Changes (11)

View Page History
*Taylor* *Johnson* [\[website\]|http://www.taylortjohnson.com]
*Taylor Johnson & Adam Zimmerman* [\[website\]|http://www.taylortjohnson.com]

*Research Area:* Controls and Computer Engineering 
*Contact:* [johnso99@illinois.edu|mailto:johnso99@illinois.edu] 
Our research group works on the [formal modeling and verification|http://en.wikipedia.org/wiki/Formal_methods] of a class of systems called [hybrid systems|http://en.wikipedia.org/wiki/Hybrid_system]. The general [formal verification|http://en.wikipedia.org/wiki/Formal_verification] problem we study is, given a mathematical model of a system and some logical property it should satisfy, verify (prove automatically, manually, combinations thereof) that the model satisfies that property. Hybrid systems are a formalism for modeling systems which have combinations of continuous and discrete dynamics, which includes nearly any embedded system, [cyber-physical system|http://en.wikipedia.org/wiki/Cyber-physical_system], or control system implemented today. An example verification problem we would study is, given a hybrid system model of a group of robots that travel toward a destination in the real plane, verify that no robots ever collide. To verify such properties, we use manual reasoning (i.e., proofs by hand), automated tools like [model checkers|http://en.wikipedia.org/wiki/Model_checking], and semi-automated tools like [theorem provers|http://en.wikipedia.org/wiki/Automated_theorem_proving]. Mentees often work on simulators for such systems, which can help provide insight in how these complex systems operate, but can only provide tests (single runs) and not verification (all possible runs).{excerpt}
Our research group has built a distributed robotic system using iRobot
Create platforms controlled by Android smartphones and a vision
tracking system. The robots communicate wirelessly to cooperatively
accomplish tasks. The current application being developed is a
distributed painting program, in which the robots divide and draw a
large scale version of a user provided image. For instance, a user
can specify their initials in a paint program, then the robots will
draw the image after subdividing the image into tasks for each
individual robot.{excerpt}

h6. *More Information:*

Our group has worked with PURE mentees for about five six semesters, and in the past, mentees have worked on a variety of hybrid systems problems that we're thinking about in our group. Last semester, we had three PURE projects. The first involved modeling and verifying properties of a DC-to-AC power converter called a multilevel converter in the model checker for timed automata [UPPAAL|http://en.wikipedia.org/wiki/Uppaal_Model_Checker]. Another was to implement an existing (i.e., on paper) algorithm in Matlab which finds the boundary of a set of robots in the real plane. The third was to implement a simulation of a distributed robot system in Matlab. Extensions of these projects and others are available, so anyone interested in control theory, robotics, or distributed systems could apply. For instance, we've got hardware for a distributed robot system which we likely will need help with writing code and running experiments.  Other past projects have involved the hybrid systems model checkers [PHAVer|http://www-verimag.imag.fr/~frehse/phaver_web/] and [HyTech|http://embedded.eecs.berkeley.edu/research/hytech/], and there's a new model checker called [SpaceEx|http://spaceex.imag.fr/] that we've recently used and would like to use more.
{panel:title=Information for Mentees| borderStyle=dashed| borderColor=#ccc| bgColor=#FFFFCE}
*Mentee's Major Activities:*
Writing code (Matlab, C, C++, or java), reading papers, attending group meetings

*Apply if interested in:*
[Cyber-physical systems|http://en.wikipedia.org/wiki/Cyber-physical_system]; control systems; robotics; [distributed computing|http://en.wikipedia.org/wiki/Distributed_computing]; embedded and real-time systems; [hybrid systems|http://en.wikipedia.org/wiki/Hybrid_system]; [formal methods|http://en.wikipedia.org/wiki/Formal_methods]

*Desired Coursework:*
Some programming background in Matlab, C, C++, or Java would be useful for all potential projects.
Programming in Java/Android, interest and excitement in robotics

*Expectations of mentee:*
Ideally a mentee should commit at least five hours a week, as there is a weekly meeting with me for about an hour, and completing whatever tasks we have assigned will usually take at least a few hours, particularly if it's programming and getting something working. There will likely be a few papers to read over the semester as well, which we'll help you get through and understand the relevant portions.
The assistant would be responsible for running tests of the system to
find problems in the latest version of the code. This will involve
learning about the operation of the system, including the vision based
tracking system and possibly some programming in Java for Android
smartphones. The assistant would also repair and modify the iRobot
Create robot chassis and construct environments needed for testing the
system. One possible robot modification the assistant would be
responsible for is designing and constructing a phone mount for the
robot chassis, allowing the smartphones to be easily mounted on the
*More Information:*
Feel free to contact me about potential projects via email and/or we can schedule a meeting. Please also see [my website|http://www.taylortjohnson.com], [my adviser's website|http://users.crhc.illinois.edu/mitras/], [an overview of distributed cyber-physical systems problems we've worked on|http://hsver.crhc.illinois.edu/index.php/Distributed_Algorithms_for_Cyber-Physical_Systems], and [an overview of the hybrid systems verification problems we've considered|http://hsver.crhc.illinois.edu/index.php/Hybrid_System_Verification].