CPSGrader: Synthesizing Temporal Logic Testers for Auto-Grading an Embedded Systems Laboratory

Garvit Juniwal, Alexandre Donzé, Jeff C. Jensen, and Sanjit A. Seshia. CPSGrader: Synthesizing Temporal Logic Testers for Auto-Grading an Embedded Systems Laboratory. In Proceedings of the 14th International Conference on Embedded Software (EMSOFT), October 2014.

Download

[pdf] 

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 errors in the program. The auto-grader is based on a notion of constrained parameterized tests based on Signal Temporal Logic (STL) that capture symptoms pointing to success or causes of failure 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 actual on-campus laboratory course.

BibTeX

@inproceedings{juniwal-emsoft14,
  author    = {Garvit Juniwal and Alexandre Donz{\'{e}} and Jeff C. Jensen and Sanjit A. Seshia},
  title     = {CPSGrader: Synthesizing Temporal Logic Testers for
           Auto-Grading an Embedded Systems Laboratory},
 booktitle = {Proceedings of the 14th International Conference on Embedded Software (EMSOFT)},
 month = "October",
 year = {2014},
 OPTpages = {1--10},
 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 
errors in the program. The auto-grader is based on a notion 
of constrained parameterized tests based on Signal Temporal Logic 
(STL) that capture symptoms pointing to success or causes of failure 
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 actual on-campus 
laboratory course.},
}