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.