View source for Auto Generation of Embedded Controllers from High Level Specification

{{StudentProjectTemplate
|Title=Model-Based Design in Acumen
|Summary=Mode-based generation of embedded platform such as the Arduino or RaspberyPi
|Author=Yingfu
|Supervisor=Walid Taha, Thomas Lithen
|Level=Master
|Status=Open
}}
<b> Description: </b>

Model-based design is an approached to embedded software development. 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. Key ingredients of model-based design are accurate model of environment and platform, and the ability to automatically compliant generate embedded software from it from high-level specifications. 

This project will explore the extent to which it is possible to demonstrate that model-based design can be realized in Acumen. To this end, the project will build the basic infrastructure for modeling one or more environments (vehicles or quad-copters), the basic program generation of embedded controllers, and possibly explore advanced program generation techniques. The work can build on recent and ongoing work on connecting the Acumen environment with an inverted pendulum system that has its own embedded controller, but it could also use this experience simply as advisory.

<b> Milestones/Schedule: </b>

<ul><li>Operational hand-written target program for embedded platform.  It should function in a way that is consistent with the reference simulation model in Acumen
<ul><li>Requires learning how to program Arduin and/or RaspberyPi platform</li></ul></li>

<li>Translator (in Scala) from source (Acumen) to target (C for embedded platform)
<ul><li>Requires learning Scala and functional programming, writing translator, writing property-based tests</li></ul></li>

<li>Checking timing constraints statically</li>
<ul><li>(If there is time)</li></ul></li>

<li>Proving the correctness of the translation</li>
<ul><li>(If there is time)</li></ul></li>
</ul>
<b> Requirements:  </b>

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.

<b> References: </b>
<ul><li>Walid Taha, Verónica Gaspes, Rex Page: Accurate Programming: Thinking about programs in terms of properties. DSL 2011: 236-260.  [http://arxiv.org/pdf/1109.0786.pdf PDF]</li>
<li>Zhanyong Wan, Walid Taha, Paul Hudak: Real-Time FRP. ICFP 2001: 146-156.  [http://haskell.cs.yale.edu/wp-content/uploads/2011/02/rt-frp.pdf PDF]</li>
<li>Functional Programming Principles in Scala.  Martin Odersky.  [https://www.coursera.org/course/progfun MOOC Website]</li>
<li>Ex/Jobb project by Viktor Frimodig Martin Gustavsson, Halmstad University.  Expected 2014.  Available via the authors for Walid Taha.</li>