The Michigan Engineer News Center

Shayan Jalili awarded 2020 NASA fellowship for safety verification of parallel cyber-physical systems

Aerospace PhD pre-candidate Shayan Jalili is one of the few students in the nation awarded the 2020 NASA fellowship for his work on safety verification of cyber-physical systems, which is the formal verification of the safety of software systems that control physical and mechanical devices. | Short Read

Under the advisorship of Professor Jean-Baptiste Jeannin, Jalili has been working on safety verification of parallel cyber-physical systems to ensure that multiple machines can function when interacting in the same environment. He combines techniques from computer science, aerospace engineering, mechanical engineering, and electrical engineering to guarantee the safety of a model. The proposed work models cyber-physical systems in the programming language Zelus, a synchronous programming language that enables parallelism, and adds verification capabilities to Zelus to guarantee the safety of critical components. The developed techniques will be applicable to many domains, such as ensuring collision avoidance for airplanes, cars or robots, as well as low-level control software present on aircraft.

Enlarge
IMAGE:  Portrait of Shayan Jalili

“No matter how technology advances, “if we cannot verify and guarantee the safety of a system, it is not a good idea to use it in critical scenarios. But in the realm of cyber-physical systems, such critical scenarios where we need safety guarantees appear more and more often,” Jalili explained.

As part of his 2020 NASA fellowship, Jalili will continue his research over the summer at Langley Research Center in Hampton, Virginia to work alongside other fellows in the Formal Methods Group.

Before pursuing his PhD in Aerospace Engineering at the University of Michigan, Shayan received his Bachelors in Computer Engineering from the University of Maryland, College Park.

The electrons absorb laser light and set up “momentum combs” (the hills) spanning the energy valleys within the material (the red line). When the electrons have an energy allowed by the quantum mechanical structure of the material—and also touch the edge of the valley—they emit light. This is why some teeth of the combs are bright and some are dark. By measuring the emitted light and precisely locating its source, the research mapped out the energy valleys in a 2D crystal of tungsten diselenide. Credit: Markus Borsch, Quantum Science Theory Lab, University of Michigan.

Mapping quantum structures with light to unlock their capabilities

Rather than installing new “2D” semiconductors in devices to see what they can do, this new method puts them through their paces with lasers and light detectors. | Medium Read