Citation
Garvit Juniwal, Alexandre Donze, Jeff C. Jensen, Sanjit Seshia. "CPSGrader: Synthesizing Temporal Logic Testers for Auto-Grading an Embedded Systems Laboratory". EMSOFT14, October, 2014.

Abstract
We consider the problem of designing an automatic grader for a laboratory in the area of cyber-physical systems. The goal of this laboratory is to program a robot for specified navigation tasks. Given a candidate student solution (control program for the robot), our grader first checks whether the robot performs the task correctly under a representative set of environment conditions. If it does not, the grader automatically generates feedback hinting at possible er- rors in the program. The auto-grader is based on a novel notion of constrained parameterized tests based on signal temporal logic (STL) that capture symptoms pointing to success or causes of fail- ure in traces obtained from a realistic simulator. We define and solve the problem of synthesizing constraints on a parameterized test such that it is consistent with a set of reference solutions with and without the desired symptom. The usefulness of our grader is demonstrated using a large data set obtained from an on-campus laboratory-based course at UC Berkeley.

Electronic downloads

• https://www.src.org/library/publication/p071331/. (Link to paper on SRC website.)
• http://dx.doi.org/10.1145/2656045.2656053
• http://people.eecs.berkeley.edu/~sseshia/pubdir/emsoft14-cpsgrader.pdf. ("camera ready" version)
• http://escholarship.org/uc/item/9tb3k46m. (link to eScholarship site)

• HTML

  Garvit Juniwal, Alexandre Donze, Jeff C. Jensen, Sanjit
  Seshia. <a
  href="http://www.terraswarm.org/pubs/346.html"
  >CPSGrader: Synthesizing Temporal Logic Testers for
  Auto-Grading an Embedded Systems Laboratory</a>,
  EMSOFT14, October, 2014.

• Plain text

  Garvit Juniwal, Alexandre Donze, Jeff C. Jensen, Sanjit
  Seshia. "CPSGrader: Synthesizing Temporal Logic Testers
  for Auto-Grading an Embedded Systems Laboratory".
  EMSOFT14, October, 2014.

• BibTeX

  @inproceedings{JuniwalDonzeJensenSeshia14_CPSGraderSynthesizingTemporalLogicTestersForAutoGrading,
      author = {Garvit Juniwal and Alexandre Donze and Jeff C.
                Jensen and Sanjit Seshia},
      title = {CPSGrader: Synthesizing Temporal Logic Testers for
                Auto-Grading an Embedded Systems Laboratory},
      booktitle = {EMSOFT14},
      month = {October},
      year = {2014},
      abstract = {We consider the problem of designing an automatic
                grader for a laboratory in the area of
                cyber-physical systems. The goal of this
                laboratory is to program a robot for specified
                navigation tasks. Given a candidate student
                solution (control program for the robot), our
                grader first checks whether the robot performs the
                task correctly under a representative set of
                environment conditions. If it does not, the grader
                automatically generates feedback hinting at
                possible er- rors in the program. The auto-grader
                is based on a novel notion of constrained
                parameterized tests based on signal temporal logic
                (STL) that capture symptoms pointing to success or
                causes of fail- ure in traces obtained from a
                realistic simulator. We define and solve the
                problem of synthesizing constraints on a
                parameterized test such that it is consistent with
                a set of reference solutions with and without the
                desired symptom. The usefulness of our grader is
                demonstrated using a large data set obtained from
                an on-campus laboratory-based course at UC
                Berkeley. },
      URL = {http://terraswarm.org/pubs/346.html}
  }
  

Posted by Alexandre Donze on 14 Aug 2014.
Groups: tools