As another semester comes to a close, it’s time to reflect on the journey through the Formal Methods for Software Engineering course. This semester, we embraced change, introducing new teaching methods and tools to enhance the learning experience. One notable addition was the integration of GitHub Classroom for assignments, a decision that brought about unexpected insights and learning experiences.
GitHub Classroom and Automated Feedback
One notable shift this semester was the adoption of GitHub Classroom for assignments. Initially intended for its auto-grading feature, we found its true value in automated feedback generation. Navigating the limitations of GitHub Classroom and the GitHub workflow proved challenging, especially when interpreting the log files. Nevertheless, this exploration led to a wealth of knowledge on crafting more useful feedback and discreetly implementing Test-driven development (TDD) without revealing solutions. I intend to delve deeper into these technical details in a future post, sharing my learnings and experiences.
Automated Feedback
The Birth of the FM Playground
A significant endeavor this semester was the development of the Formal Methods (FM) Playground. The Formal Methods for Software Engineering course covers four chapters, each involving different tools- SAT solvers, SMT solvers, Alloy, and nuXmv. Recognizing the challenges students faced with publicly available tools—some lacking executables for all platforms—we embarked on creating an integrated platform. This platform, featuring tools like limboole for SAT solving and propositional logic, z3 as an SMT solver for first-order logic, Alloy for relational first-order logic and declarative specification, and nuXmv for LTL model checking, streamlined the learning process. This platform would allow students to access essential tools without the need for complex installations.
With only a week before the semester began, the race was on to develop a solution. A single JavaScript application was the starting point, and as the semester progressed, the FM Playground evolved. Motivated by the growing interest among students and their desire for additional features, the platform became an integral part of the course, also aiding in generating automated feedback for GitHub Classroom submissions.
An additional layer of innovation was introduced by anonymously storing student-written specifications. Looking towards the future, the intention is to make these specifications public, paving the way for accelerated research and knowledge sharing. By incorporating real-world examples from student work, we aim to contribute to the broader academic community and foster collaborative learning.
FM Playground
Christmas Break Transformation
Realizing its potential, I devoted time over the Christmas break to migrate the static JavaScript application to React for the frontend. On the backend, Flask (Python) played a crucial role, though the complexity increased due to the diverse languages used by the various tools incorporated.
As of now, the project remains under development with an extensive roadmap ahead. The goal is to make it more interactive and user-friendly, addressing the unique requirements of students engaged in Formal Methods for Software Engineering. The journey has been exhilarating, marked by the fusion of innovation, determination, and a commitment to improving the educational experience for students.
In the coming months, I look forward to sharing more insights into the technical intricacies of GitHub Classroom, as well as providing updates on the continuous evolution of the FM Playground. The commitment to enhancing education through technology is a journey that never truly concludes, and I am excited to see what the future holds for the intersection of formal methods and software engineering education.