Introduction

CPSGrader is an automatic grading and feedback generation tool (auto-grader) for laboratory courses developed at the University of California, Berkeley. CPSGrader uses temporal logics with quantative semantics, such as Metric Temporal Logic (MTL) or Signal Temporal Logic (STL) to define test benches to monitor simulation traces of student solutions for mistakes/faults. It is designed to work with any black-box simulator.
The test benches in CPSGrader are "parameterized" to be robust to certain allowed variations in student solutions. Each test bench serves as a classifier to detect presence/absence of a particular kind of fault and we automatically synthesize the classification boundaries (in terms of ranges of test bench parameters) using a sample set of previously known correct and faulty solutions.
The first version of our auto-grader is an independent library written in C++ that can plug into any simulator via an API, and our first version of the test bench synthesis is done in MATLAB using the Breach toolbox. Our newer auto-grader has been developed using the pyMTL and Scenic software tools.

Deployment

CPSGrader was used in conjunction with the physics-based simulation driven virtual robotics laboratory (CyberSim) for the laboratory component of the online Cyber-Physical Systems MOOC EECS 149.1x offered on edX. This is the first online course to use a physics-based virtual robotics laboratory and the first deployed auto-grader that uses formal verification. We received very positive feedback about the tool with 86% students reporting that the debugging information generated by CPSGrader was crucial for solving the lab exercises. CPSGrader is a significant step in furthering the broader agenda of use of formal methods in making engineering education fun and scalable to large number of students across the world.

CPSGrader has also been used on campus at Berkeley in the course "Introduction to Embedded Systems", and the newer version has been used to run a remote/virtual laboratory for this class during the COVID-19 pandemic.

Publications

  • Sanjit A. Seshia. Cyber-Physical Systems Education: Explorations and Dreams. In Principles of Modeling - Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday, pp. 407–422, 2018. [HTML]
  • Garvit Juniwal. CPSGrader: Auto-Grading and Feedback Generation for Cyber-Physical Systems Education. Masters Thesis, December 2014
    [PDF] [Details]
  • Garvit Juniwal, Alexandre Donzé, Jeff C. Jensen, 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
    [PDF] [Details]
  • Garvit Juniwal, Sakshi Jain, Alexandre Donzé, Sanjit A. Seshia. Clustering-Based Active Learning for CPSGrader. In Proceedings of the Second ACM Conference on Learning@Scale (L@S), March 2015
    [PDF] [Details]

Talks

  • CPSGrader: Auto-Grading a Cyber-Physical Systems Lab. Garvit Juniwal. At Embedded Systems Week (EMSOFT), New Delhi INDIA, Oct 13-17 2014
    [PPT] (for 30 min talk)
  • Towards Lab-Based MOOCs: Cyber-Physical Systems, Robotics, and Beyond. Sanjit A. Seshia. At National Instruments (NI) Week, August 2014
    [PDF] (for 30 min talk)
  • Towards Lab-Based MOOCs: Cyber-Physical Systems, Robotics, and Beyond. Sanjit A. Seshia. At Learning with MOOCs: A Practitioner's Workshop (LWMOOC), August 2014
    [PPT] (for 3 min overview talk) [Session Video (starts at minute 7:30)]

Licenses

Copyright ©2014-2020, Sanjit A. Seshia, Alexandre Donzé, Garvit Juniwal, Jeff C. Jensen, Bernard Chen, Edward Kim, Hazem Torfah, and Victoria Tuck. All rights reserved. CPSGrader is licensed under the BSD-3-clause license.

Acknowledgments

This work has been supported in part by TerraSwarm, one of the six centers of STARnet, a Semiconductor Research Corporation program sponsored by DARPA, by the NSF ExCAPE project (CCF-1139138), by the NSF VeHICaL project (CNS-1545126), and by National Instruments Corporation.