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

一年级和二年级的计算机科学基础课程是本科生学习的最大绊脚石。尽管对熟练专业人员的需求在增加，但全国CS学生的入学人数下降了60%以上。本研究的主要目的是丰富CS学习过程的背景，从动机和教育的角度来看，CS学习过程具有重要意义。这个项目研究了一种验证驱动的学习模式，该模式有助于学生从他们早期的计算课程开始，一直持续到他们在计算方面的整个学习过程，参与真实世界的计算任务。这种模式可以显著降低学生在早年学习现实世界问题的先决条件。学生的任务是验证软件的功能，执行程序，测试系统的部件(预先分解的子系统和组件)，并定位可能的错误。这种看似复杂的高级任务可以由新手学生来完成，因为软件验证不需要设计和实现，并且可以在充分准备的情况下变成一个样例学习的过程。这种准备被包装在验证驱动的学习用例中，该用例定义了支持验证驱动的学习活动的配置，并且由诸如系统存在的合理性、需求规范、功能描述、一组测试用例以及系统的分解等元素组成。为了实现学习模式，该项目将根据教师的研究产生学习案例，包括计算机安全、生物信息学、地理信息系统、数据库和数据挖掘技术、遥感和模糊集技术。学习案例将使学生接触到在科学研究、工程开发或社交网络中服务于现实世界目的的工作软件系统。这种学习方式也将帮助在各个领域拥有丰富经验但需要在劳动力中重新定位的成人学生。该项目的最终目标是振兴CS课程，培养更多有能力进行计算思维的毕业生。

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.