Initially, he taught a combination of Z and CSP# due to the local curriculum requirement on concurrency. Despite engaging the students with several software platforms (PAT for CSP# concurrent models verification, CZT for typing Z schemas/programs and Z-Eves for proving), the feedback pointed out the weakness of Z-related tools, in addition to the loose connection between the two formalisms. Building on this initial phase, Gustavo continued with teaching a combination of Event-B and CSP<sub>M</sub>, attracting positive feedback on the Event-B related software tools, such as Rodin, ProB and B Motion Studio. The last and current phase consists in teaching only B, due to several developments: the possibility to drop the mandatory concurrency requirement and the recent availability of a B Massive Open Online Course (MOOC). The latter development allowed for changing from a classical teaching format to a flipped classroom, where students are required to follow the MOOC course and then implement in a laboratory the various exercises and projects, with teacher support. The feedback from students changed to an appreciation of the employed software tools (Atelier-B, ProB, B Motion Web and VS Code) together with the integrated nature of the course, since some of the projects involve code generation in C with embedding in various platforms of interest for students.
0 commit comments