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

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

Citation formats  
  • 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

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.