CPATH-1: Collaborative Research: a Verification-Driven Learning Model that Enriches CS and Related Undergraduate Programs

大一和大二阶段的计算机科学基础课程是本科生学习的最大障碍。尽管对熟练专业人员的需求在增加，但全国范围内，计算机科学专业的学生入学率下降了60%以上。迫切需要一种更有效的计算机科学学习模式。本研究的主要目的是从动机和教育的角度丰富计算机科学学习过程的背景。该项目研究了一种验证驱动的学习模型，该模型可以促进学生从早期的计算课程开始参与到现实世界的计算任务中，并在整个计算学习中持续进行。这种模式可以显著降低学生在早期研究现实世界问题的先决条件。学生的任务是验证软件的功能，执行程序，测试系统的部分（预分解的子系统和组件），并找出可能的错误。这种看似复杂的高级任务可以由新手完成，因为软件验证不需要设计和实现，并且可以在充分准备的情况下变成一个通过实例学习的过程。这种准备工作被封装在验证驱动的学习用例中，它定义了支持验证驱动的学习活动的配置，并由诸如系统存在的证明、需求规范、功能描述、一组测试用例和系统分解等元素组成。验证驱动学习模型的基础在于软件测试理论和技术。频繁和渐进的验证练习将使学生为正式规范做好准备。为实现该学习模式，本计划将根据教师的研究成果制作学习案例，包括计算机安全、生物信息学、地理信息系统、数据库和数据挖掘技术、遥感和模糊集技术。学习案例将使学生接触到在科学研究、工程开发或社会网络中服务于现实世界目的的工作软件系统。这个项目将特别提倡在少数族裔和女性学生中进行计算机科学教育。这种学习方法也将帮助那些在各个领域有丰富经验但需要在工作中重新定位的成年学生。该项目的最终目标是振兴计算机科学项目，培养更多具有计算思维能力的毕业生。

Computer science foundation-building courses at the freshman and sophomore levels pose the greatest stumbling blocks to undergraduate students' learning. CS student enrollment has declined over 60% nationwide, even though the demand for skilled professionals was increasing. There is an urgent need for a more effective CS learning model. The main purpose of this research is to enrich the context of the CS learning process which is important from motivational and educational perspectives. This project investigates a verification-driven learning model that facilitates students' involvement in real-world computing tasks starting from their early computing courses and continuing throughout their entire studies in computing. This model can significantly reduce the prerequisites for students to study real-world problems in their early years. The students are tasked to validate the functionality of software, execute programs, test parts of systems (pre-decomposed subsystems and components), and locate possible errors. Such seemingly complex high-level tasks can be done by novice students because software verification does not require design and implementation, and can be turned into a learn-by-example process with adequate preparation. This kind of preparation is wrapped in a Verification-Driven Learning Case, which defines the configuration to support a verification-driven learning activity, and consists of elements such as the justification of the system's existence, the requirement specification, description of the functionality, a set of test cases, and the decomposition of the system. The foundation of the verification-driven learning model lies in software testing theories and techniques. Frequent and progressive exercises on verification will prepare the students for formal specifications. To realize the learning model, this project will produce Learning Cases based on faculty research including computer security, bioinformatics, geographic information systems, database and data mining techniques, remote sensing, and fuzzy set techniques. The Learning Cases will expose the students to working software systems that serve a real-world purpose in scientific research, engineering development, or social networks.This project will particularly advocate computer science education in under-represented minority and woman students. This learning approach will also help adult students who have rich experience in various areas but need to reposition themselves in the work force. The final goal of this project is to revitalize the CS programs and produce more competent graduates capable of computational thinking.