NeTS: Small: Exploring the Design, Implementation, Operation Issues of Cellular IoT via Formal Analysis and Empirical Validation

物联网正在进入我们的日常生活。作为唯一一种与互联网相提并论的大规模无线网络基础设施，蜂窝网络在互联各种事物方面发挥着关键作用。从2015年（4亿）到2021年（15亿），连接蜂窝物联网（CIoT）设备预计将增长近四倍。随着CIoT设备的爆炸式增长，CIoT标准的任何设计缺陷，CIoT设备的实施问题以及CIoT服务运营商的操作失误都可能导致全球范围内的灾难性后果。本项目旨在从设计、实施和运营的角度对CIoT服务进行全面调查。该项目的成功完成不仅将为识别CIoT服务的设计缺陷、实施问题和操作失误提供新的技术，还将促进CIoT服务的部署，推动美国CIoT经济的发展。研究结果还可能影响即将到来的5G无线网络中CIoT的设计。首先，它的目的是开发一个CIoT控制平面协议验证工具的形式化方法的基础上，识别CIoT标准的功能不正确，性能降级和安全问题方面的设计缺陷。其次，它旨在开发一种严格的测试方法，用于探索CIoT实践的实施问题和操作失误，其中包括CIoT一致性测试标准，CIoT实践以及CIoT行业SQA（软件质量保证）专家的反馈。第三，它旨在开发一个开源的CIoT测试平台，包括CIoT终端和基础设施，以验证可能的设计缺陷，实现问题和操作失误，这些问题由于安全，业务和其他问题而在实践中很难得到验证。该CIoT测试平台将发布给研究社区，用于未来的CIoT研究。除了技术贡献外，拟议的项目还允许研究人员将他们的研究成果整合到电气和计算机工程以及计算机科学专业的本科和研究生课程中。最后，该项目将通过培训学生获得移动的系统、无线网络和正式方法方面的技术专长，为国家的劳动力做出贡献。该奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

The Internet of Things is coming into our daily life. As the only large-scale wireless network infrastructure on a par with the Internet, the cellular network plays a critical role in interconnecting a variety of things. Connected cellular IoT (CIoT) devices are forecast to grow almost four-fold from 2015 (0.4 billion) to 2021 (1.5 billion). With the explosive growth of CIoT devices, any design defects of CIoT standards, implementation issues of CIoT devices, and operational slips of CIoT service operators could lead to devastating consequences on a global scale. This project seeks to conduct a full investigation of CIoT services from their design, implementation and operation perspectives. The successful completion of this project will not only contribute new techniques to identify design defects, implementation issues, and operational slips of CIoT services, but also facilitate the deployment of CIoT services and boost the CIoT economy in the U.S. The research findings may also influence the design of CIoT in the upcoming 5G wireless networks.The proposed research has three key areas of technical contributions. First, it aims to develop a CIoT control-plane protocol verification tool based on formal methods, which identifies design defects of CIoT standards in terms of functional incorrectness, performance downgrade, and security issues. Second, it aims to develop a rigorous testing methodology for exploring the implementation issues and operational slips of CIoT practice, which covers CIoT conformance testing standards, CIoT practice, and feedbacks from SQA (Software Quality Assurance) experts in the CIoT industry. Third, it aims to develop an open-source CIoT test-bed including CIoT terminals and infrastructure to verify the possible design defects, implementation issues, and operational slips which are hardly to be validated in practice due to security, business, and other concerns. This CIoT test-bed will be released to the research community for future CIoT research. Besides technical contributions, the proposed project allows the researchers to integrate their research findings into both undergraduate and graduate curricula for both Electrical and Computer Engineering and Computer Science majors. Finally, this project will contribute to the nation's workforce by training students to obtain technical expertise in mobile systems, wireless networking, and formal methods.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.