Applying property-based testing in teaching safety-critical system programming

At the Universidad Politcnica de Madrid students attending a course on concurrency are taught a high-level formalism which permits concise specification of shared resources. This formalism is used to express safety-critical access policies for typical control problems such as robot plants. Students are moreover provided with programming recipes for implementing such shared resource specifications in programming languages (typically Java). The teachers of the course use various tools to ensure that the implementations developed by students for a shared resource are of an acceptable quality. Such tools include normal unit tests, but also the systematic application of property-based testing to judge the quality of the exercises. In this article we provide an overview of the tools, techniques and methods used in one particular exercise of the course: the implementation of a control system for an automated warehouse.