Difference between revisions of "Old Name of the new project"

From CERES
Jump to: navigation, search
m (Nicholas moved page Name of the new project to Old Name of the new project without leaving a redirect)
 
(4 intermediate revisions by one user not shown)
Line 1: Line 1:
 
{{StudentProjectTemplate
 
{{StudentProjectTemplate
|Summary=(High Priority) Rigorous Real-time Network Modeling and Verification
+
|Summary=Model-based Design of a Sailboat Autopilot
 
|Programme=EIS Masters 15hpc
 
|Programme=EIS Masters 15hpc
 +
|Keywords=Smart homes, pervasive computing, DiaSuite
 
|TimeFrame=6 months
 
|TimeFrame=6 months
 
|References=Contact instructor
 
|References=Contact instructor
 +
|Prerequisites=DA8003 Cyber-Physical Systems
 
|Supervisor=Walid Taha
 
|Supervisor=Walid Taha
 
|Examiner=Mohammad Reza Mousavi
 
|Examiner=Mohammad Reza Mousavi
|Level=Flexible
+
|Level=Master
|Status=Finished
+
|Status=Open
 
}}
 
}}
The core research question is to demonstrate that state of the art modeling and verification methods can be used to help design the communication infrastructure at the AstaZero test track.
+
The core research question is to whether we can use Acumen for model-based design. This thesis aims to demonstrate this using a case study with a prototype sailboat. Technical challenges include modeling, instrumentation, localization, communication, and control
  
This project will be aligned with the KK AstaMoCA project involving professors Taha, Mousavi, and Vinel.
+
The first component of the work is build a prototype compiler that can target an embedded microcontroller platform (such as an arduino, raspberry pi, etc). This involves first selecting a series of more sophisticated examples that illustrate key features of controllers written within one Acumen object. For the purposes of synthesis the Acumen language itself may be extended with some specialized annotations that support this generation task and do not interfere with the semantics of Acumen models otherwise. Examples of such annotations may include special variable names that can be found on the target platform, special characteristics such as clock rate, etc.  Next, corresponding "generated" C or Java code is written by hand and tested extensively. Then, a BNF for a sufficient subset of C or Java is defined in Scala. Next, an interpreter is written for this subset (to enable fast testing of the translator). Then, a translator that automates this translation is written. Then, property-based tests are built for this interpreter. Next, a pretty-printer that generates an ASCII file for compilation on the target domain is built, and all collected examples are used to generate this translation. Finally, a collection of performance benchmarks are developed and used to evaluate the timing accuracy of of the results of the compiler. It should be noted here that this not raw performance, but rather, accuracy in terms of consistency of the timing characteristics and overall behavior of what happens on the target platform compared to what happens on the model. Some data logging and data download capabilities may be added to support this type of comparison.
  
The research question involves primarily modeling communication systems, and extending verification tools to handle such models.
+
The second component is to identify related work about sail boat control, to read it, and write a coherent overview of this literature, and position the results in the context of this literature.
  
The first component of the work is to build models of communication systems, starting from queuing systems and building up to full systems.
+
The third component of the work is to model the robot in Acumen based on a suitable physical prototype that can be used for physical testing. Data-collection facilities developed in the first part should be used to evaluate the accurate of the simulations and the actual performance of the boat. A clear method should be developed to separate error from measurement and actual error in performance (such as the actual position and direction of the boat).
  
The second component is the evaluation of current verification tools using these models. This involves using the models to test the tools to see if they are able to produce the expected results in a satisfactory manner.
+
The fourth component is writing up the results of the work.
  
The third component of the work is extension of current verification technologies to improve the state of the art.
+
References:
  
The fourth component is scholarship, consisting of reading related research papers and writing up the results of the work.
+
* https://www.ensta-bretagne.fr/jaulin/paper_jaulin_irsc12.pdf
 
+
* https://www.youtube.com/watch?v=ZkMAR5gP-bw
The deliverables are a) a series of communication systems models that are mathematically valid and practically relevant, b) an extensive table evaluating the extent to which the verification technology is able to function on the benchmarks, c) an extension of the verification technology to handle key features of the benchmarks (which are relevant to the scientific community), and d) a thesis document and presentation.
+
* https://www.archives-ouvertes.fr/hal-00628434/document
 +
* https://www.ensta-bretagne.fr/jaulin/paper_lebars_irsc12.pdf

Latest revision as of 13:26, 11 November 2016

Title Old Name of the new project
Summary Model-based Design of a Sailboat Autopilot
Keywords Smart homes, pervasive computing, DiaSuite
TimeFrame 6 months
References Contact instructor
Prerequisites DA8003 Cyber-Physical Systems
Author
Supervisor Walid Taha
Level Master
Status Open

Generate PDF template

The core research question is to whether we can use Acumen for model-based design. This thesis aims to demonstrate this using a case study with a prototype sailboat. Technical challenges include modeling, instrumentation, localization, communication, and control

The first component of the work is build a prototype compiler that can target an embedded microcontroller platform (such as an arduino, raspberry pi, etc). This involves first selecting a series of more sophisticated examples that illustrate key features of controllers written within one Acumen object. For the purposes of synthesis the Acumen language itself may be extended with some specialized annotations that support this generation task and do not interfere with the semantics of Acumen models otherwise. Examples of such annotations may include special variable names that can be found on the target platform, special characteristics such as clock rate, etc. Next, corresponding "generated" C or Java code is written by hand and tested extensively. Then, a BNF for a sufficient subset of C or Java is defined in Scala. Next, an interpreter is written for this subset (to enable fast testing of the translator). Then, a translator that automates this translation is written. Then, property-based tests are built for this interpreter. Next, a pretty-printer that generates an ASCII file for compilation on the target domain is built, and all collected examples are used to generate this translation. Finally, a collection of performance benchmarks are developed and used to evaluate the timing accuracy of of the results of the compiler. It should be noted here that this not raw performance, but rather, accuracy in terms of consistency of the timing characteristics and overall behavior of what happens on the target platform compared to what happens on the model. Some data logging and data download capabilities may be added to support this type of comparison.

The second component is to identify related work about sail boat control, to read it, and write a coherent overview of this literature, and position the results in the context of this literature.

The third component of the work is to model the robot in Acumen based on a suitable physical prototype that can be used for physical testing. Data-collection facilities developed in the first part should be used to evaluate the accurate of the simulations and the actual performance of the boat. A clear method should be developed to separate error from measurement and actual error in performance (such as the actual position and direction of the boat).

The fourth component is writing up the results of the work.

References: