Auto Generation of Embedded Controllers from High Level Specification
| Title | Auto Generation of Embedded Controllers from High Level Specification |
|---|---|
| Summary | To develop, test, and verify a method for translating hybrid-models of controllers to controllers that work on an embedded platform such as the Arduino or RaspberyPi |
| Keywords | |
| TimeFrame | |
| References | |
| Prerequisites | |
| Author | Yingfu |
| Supervisor | Walid Taha, Thomas Lithen |
| Level | Master |
| Status | Open |
Description:
Embedded software is ubiquitous, and its correctness is essential for ensuring the safety of cars, airplanes, power grids, and a wide range of critical systems that we depend on in our daily lives. An important technology for ensuring the correctness of embedded software is to automatically generate it from high-level specifications. This project will start with building infrastructure for basic program generation of embedded controllers, and then provide the student with an excellent starting point to explore advanced program generation techniques. The work will build on recent and ongoing work on connecting the Acumen environment with an inverted pendulum system that has its own embedded controller.
Milestones/Schedule:
- Operational hand-written target program for embedded platform. It should function in a way that is consistent with the reference simulation model in Acumen
- Requires learning how to program Arduin and/or RaspberyPi platform
- Translator (in Scala) from source (Acumen) to target (C for embedded platform)
- Requires learning Scala and functional programming, writing translator, writing property-based tests
- Checking timing constraints statically
- (If there is time)
- Proving the correctness of the translation
- (If there is time)
Requirements:
The student must have taken a course on Cyber-Physical Systems or equivalent. In particular, the student should have a basic understanding of continuous and hybrid (continuous/discrete) modeling, quantization, discretization. The student should also be familiar with the C programming language, and be willing to gain expertise in functional programming and the Scala programming language.
References:
- Walid Taha, Verónica Gaspes, Rex Page: Accurate Programming: Thinking about programs in terms of properties. DSL 2011: 236-260. PDF
- Zhanyong Wan, Walid Taha, Paul Hudak: Real-Time FRP. ICFP 2001: 146-156. PDF
- Functional Programming Principles in Scala. Martin Odersky. MOOC Website
- Ex/Jobb project by Viktor Frimodig Martin Gustavsson, Halmstad University. Expected 2014. Available via the authors for Walid Taha.
