分布式流处理程序的分析与验证

Due to the rapid development of IoT and online social networks, the data volume in the information society is increasing tremendously everyday. How to process rapidly and precisely the huge volume of data is greatly challenging the IT professionals. Distributed stream processing platforms have recently received great focus from the IT academia and industry, and they are seen as a new means of implementing critical data-driven business logics, attributed to the fact that they can process in real time the continuous and unbounded data streams. Therefore, it becomes vital to guarantee the correctness and reliability of these programs. This project plans to seek unified automata models to model the functionalities of distributed stream processing programs, propose proper specification languages to describe the behaviours of these programs, and investigate the corresponding verification techniques and methodologies. Meanwhile, this project plans to formalise the typical fault tolerance mechanisms of distributed stream processing programs as well as the reliability guarantees, and analyse/verify whether these programs can fulfil a given reliability guarantee under a certain fault-tolerance mechanism. Furthermore, this project will also develop prototype tools and do extensive case studies.

由于物联网、在线社交网络等新型应用需求的推动，信息社会中的数据量每天都在急剧增长。如何对这些超大规模的数据进行快速准确的处理对于计算机从业人员提出了很大的挑战。分布式流处理平台由于可以对连续无限的数据流进行实时处理，最近引起了计算机学术界和产业界的极大关注，已经成为实现数据驱动的关键业务逻辑的一种新途径。因此，保证分布式流处理程序的功能正确性与可靠性变得日益重要。本项目计划寻找统一的自动机模型来对分布式流处理程序的功能进行建模，提出合适的规约语言来描述流处理程序的行为，并发展相应的验证技术与方法。同时，本项目计划对分布式流处理程序的典型容错机制和可靠性保障等级进行形式化，并进一步对分布式流处理程序在某种容错机制下能否达到给定的可靠性保障等级进行分析与验证。而且，本项目计划开发原型工具，进行广泛的实例研究。

本项目针对分布式流处理程序功能正确性的形式验证问题，在面向流处理程序的自动机模型和基于分布式快照回滚的容错机制及可靠性保障等级的形式化等方面展开研究，取得了以下进展：.1).提出了数据流转换器的自动机模型，对Flink平台上的复杂事件处理程序进行了形式建模，并通过大量测试用例验证了形式建模与Flink平台复杂事件处理程序的实际语义的一致性。.2).提出了一种面向大数据处理框架的高效数据缓存替换方法，即最小分区权重(Least partition weight, LPW)算法，实验结果表明LPW算法能够最高减少75%的应用执行时间。.3).针对在线离线数据流聚类算法，我们提出了一种序敏感的可扩展性良好的分布式框架DistStream，并在DistStream中实现了四种有代表性的数据聚类算法，实验结果表明基于DistStream的数据流聚类算法能够实现亚线性的吞吐量收益，而且聚类质量与单机版本相当(99%)。.4).我们对Flink平台的基于分布式快照回滚的容错机制进行了形式建模，并对三种可靠性保障等级(恰好一次、至少一次、至多一次)进行了形式化。