Jiawei Chen

Robotics PhD Candidate

Ann Arbor, MI, USA

chenjw [at] umich (dot) edu
GitHub: jchen-cs
Google Scholar
LinkedIn
CV

About Me

I’m a fifth-year Robotics PhD Candidate at the University of Michigan, advised by Jean-Baptiste Jeannin in the MARVL group. I was also an OSTEM intern at NASA Langley Research Center under the Safety-Critical Avionics Systems branch in Fall 2023 and Summer 2024. My research revolves around designing more reliable embedded systems, whether they are roving around on wheels, thrusted by propellers, or worn by migratory birds. Recently, my interest has been in applying formal methods to robotics and robotics-adjacent applications. Outside of research, I enjoy growing unique and interesting houseplants, playing the piano, and volunteering at robotics competitions. I have also designed and built a small fleet of remote-controlled aircraft, and currently maintain an electronics prototyping lab.

Education

• [in-progress] Robotics PhD University of Michigan, advised by Jean-Baptiste Jeannin, 2020-present
• Robotics MS University of Michigan, 2020-2022
• Computer Science + Physics BA Indiana University Bloomington, 2016-2020
  • Mathematics Minor
  • Graduated with Highest Distinction, Hutton Honors Notation, and Computer Science Departmental Honors

Work Experience

• OSTEM Intern, NASA Langley Research Center, August-December 2023; June-August 2024

Publications

Chen, J., Vargas de Mendonça, J. L., Ayele, B., Bekele, B., Jalili, S., Sharma, P., Wohlfeil, N., Zhang, Y., Jeannin, J-B.
Synchronous Programming with Refinement Types

In International Conference on Functional Programming (ICFP),2024.

CiteLink

Brown, G. M., Chen, J., Fudickar, A. M., Jahn, A. E.
An Open-Source Platform for Sub-g, Sub-µA Data Loggers

In Animal Biotelemetry,2023.

CiteLink

Chen, J., Vargas de Mendonça, J. L., Jalili, S., Ayele, B., Bekele, B., Qu, Z., Sharma, P., Shiferaw, T., Zhang, Y., Jeannin, J-B.
Synchronous Programming and Refinement Types in Robotics: From Verification to Implementation

In Formal Techniques in Safety-Critical Systems (FTSCS),2022.

CiteLink

Jeannin, J-B., Chen, J., Vargas de Mendonça, J. L., Mamouras, K.
Work-in-Progress: Towards a Theory of Robust Quantitative Semantics for Signal Temporal Logic

In International Conference on Embedded Software (EMSOFT),2022.

CiteLink

Chen, J., Brown, G., Fudickar, A.
Simulation-Based Validation of Activity Logger Data for Animal Behavior Studies

In Animal Biotelemetry,2021.

CiteLink

 @article{chen_synchronous_2024,
 title = {Synchronous {Programming} with {Refinement} {Types}},
 volume = {8},
 url = {https://dl.acm.org/doi/10.1145/3674657},
 doi = {10.1145/3674657},
 abstract = {Cyber-Physical Systems (CPS) consist of software interacting with the physical world, such as robots, vehicles, and industrial processes. CPS are frequently responsible for the safety of lives, property, or the environment, and so software correctness must be determined with a high degree of certainty. To that end, simply testing a CPS is insufficient, as its interactions with the physical world may be difficult to predict, and unsafe conditions may not be immediately obvious. Formal verification can provide stronger safety guarantees but relies on the accuracy of the verified system in representing the real system. Bringing together verification and implementation can be challenging, as languages that are typically used to implement CPS are not easy to formally verify, and languages that lend themselves well to verification often abstract away low-level implementation details. Translation between verification and implementation languages is possible, but requires additional assurances in the translation process and increases software complexity; having both in a single language is desirable. This paper presents a formalization of MARVeLus, a CPS language which combines verification and implementation. We develop a metatheory for its synchronous refinement type system and demonstrate verified synchronous programs executing on real systems.},
 number = {ICFP},
 urldate = {2024-09-08},
 author = {Chen, Jiawei and de Mendonça, José Luiz Vargas and Ayele, Bereket Shimels and Bekele, Bereket Ngussie and Jalili, Shayan and Sharma, Pranjal and Wohlfeil, Nicholas and Zhang, Yicheng and Jeannin, Jean-Baptiste},
 month = aug,
 year = {2024},
 pages = {268:938--268:972}, }

@article{brown_open-source_2023,
 title = {An open-source platform for sub-$${\textbackslash}textrm{g}$$, sub-$${\textbackslash}upmu$${A} data loggers}, volume = {11},
 issn = {2050-3385},
 url = {https://animalbiotelemetry.biomedcentral.com/articles/10.1186/s40317-023-00327-0},
 doi = {10.1186/s40317-023-00327-0},
 abstract = {Background  Rapid improvements in inexpensive, low-power, movement and environmental sensors have sparked a revolution in animal behavior research by enabling the creation of data loggers (henceforth, tags) that can capture fine-grained behavioral data over many months. Nevertheless, development of tags that are suitable for use with small species, for example, birds under 25 g, remains challenging because of the extreme mass (under 1 g ) and power (average current under 1µ   A) constraints. These constraints dictate that a tag should carry exactly the sensors required for a given experiment and the data collection protocol should be specialized to the experiment. Furthermore, it can be extremely challenging to design hardware and software to achieve the energy efficiency required for long tag life. Results  We present an activity monitor, BitTag, that can continuously collect activity data for 4–12 months at 0.5–0.8g , depending upon battery choice, and which has been used to collect more than 500,000 h of data in a variety of experiments. The BitTag architecture provides a general platform to support the development and deployment of custom sub-g tags. This platform consists of a flexible tag architecture, software for both tags and host computers, and hardware to provide the host/tag interface necessary for preparing tags for “flight” and for accessing tag data “postflight”. We demonstrate how the BitTag platform can be extended to quickly develop novel tags with other sensors while satisfying the 1g/1µ A mass and power requirements through the design of a novel barometric pressure sensing tag that can collect pressure and temperature data every 60s for a year with mass under 0.6g.},
 language = {en},
 number = {1},
 urldate = {2023-05-08},
 journal = {Animal Biotelemetry},
 author = {Brown, Geoffrey M. and Chen, Jiawei and Fudickar, Adam and Jahn, Alex E.},
 month = may,
 year = {2023},
 pages = {19}, } 

@inproceedings{chen2022synchronous,
 address = {New York, NY, USA},
 series = {{FTSCS} 2022},
 title = {Synchronous {Programming} and {Refinement} {Types} in {Robotics}: {From} {Verification} to {Implementation}},
 copyright = {All rights reserved},
 isbn = {978-1-4503-9907-4},
 shorttitle = {Synchronous {Programming} and {Refinement} {Types} in {Robotics}},
 url = {https://doi.org/10.1145/3563822.3568015},
 doi = {10.1145/3563822.3568015},
 abstract = {Robots and other cyber-physical systems are held to high standards of safety and reliability, and thus one must be confident in the correctness of their software. Formal verification can provide such confidence, but programming languages that lend themselves well to verification often do not produce executable code, and languages that are executable do not typically have precise enough formal semantics. We present MARVeLus, a stream-based approach to combining verification and execution in a synchronous programming language that allows formal guarantees to be made about implementation-level source code. We then demonstrate the end-to-end process of developing a safe robotics application, from modeling and verification to implementation and execution.},
 urldate = {2023-02-27},
 booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} {International} {Workshop} on {Formal} {Techniques} for {Safety}-{Critical} {Systems}},
 publisher = {Association for Computing Machinery},
 author = {Chen, Jiawei and Vargas de Mendonça, José Luiz and Jalili, Shayan and Ayele, Bereket and Bekele, Bereket Ngussie and Qu, Zhemin and Sharma, Pranjal and Shiferaw, Tigist and Zhang, Yicheng and Jeannin, Jean-Baptiste},
 month = dec,
 year = {2022},
 keywords = {refinement types, cyber-physical systems, formal verification, robotics, synchronous programming},
 pages = {68--79}, }

 @inproceedings{jeannin2022work--progress,
 title = {Work-in-{Progress}: {Towards} a {Theory} of {Robust} {Quantitative} {Semantics} for {Signal} {Temporal} {Logic}},
 shorttitle = {Work-in-{Progress}},
 doi = {10.1109/EMSOFT55006.2022.00013},
 abstract = {Several quantitative semantics of temporal logics have been investigated recently. We propose a general form to model those quantitative semantics, establish requirements for soundness, and evaluate the framework on a few examples.},
 booktitle = {2022 {International} {Conference} on {Embedded} {Software} ({EMSOFT})},
 author = {Jeannin, Jean-Baptiste and Chen, Jiawei and de Mendonça, José Luiz Vargas and Mamouras, Konstantinos},
 month = oct,
 year = {2022},
 note = {ISSN: 2771-571X},
 keywords = {Embedded software, Quantitative Semantics, Semantics, Signal temporal logic},
 pages = {11--12}, } 

 @article{chen2021simulation-based,
 title = {Simulation-based validation of activity logger data for animal behavior studies},
 volume = {9},
 copyright = {All rights reserved},
 issn = {2050-3385},
 url = {https://animalbiotelemetry.biomedcentral.com/articles/10.1186/s40317-021-00254-y},
 doi = {10.1186/s40317-021-00254-y},
 abstract = {Bio-loggers are widely used for studying the movement and behavior of animals. However, some sensors provide more data than is practical to store given experiment or bio-logger design constraints. One approach for overcoming this limitation is to utilize data collection strategies, such as non-continuous recording or data summarization that may record data more efficiently, but need to be validated for correctness. In this paper we address two fundamental questions—how can researchers determine suitable parameters and behaviors for bio-logger sensors, and how do they validate their choices? We present a methodology that uses software-based simulation of bio-loggers to validate various data collection strategies using recorded data and synchronized, annotated video. The use of simulation allows for fast and repeatable tests, which facilitates the validation of data collection methods as well as the configuration of bio-loggers in preparation for experiments. We demonstrate this methodology using accelerometer loggers for recording the activity of the small songbird Junco hyemalis hyemalis.},
 language = {en},
 number = {1},
 urldate = {2021-09-13},
 journal = {Animal Biotelemetry},
 author = {Chen, Jiawei and Brown, Geoffrey and Fudickar, Adam},
 month = dec,
 year = {2021},
 pages = {31}, }