Parameter Synthesis for Reliable, Performant and Efficient Wireless Network Protocols

可靠、高性能和高效无线网络协议的参数综合

• 批准号: 433044889
• 负责人: Professor Dr. Joost-Pieter Katoen
• 金额: --
• 依托单位: Informatik 2 - Lehrstuhl Softwaremodellierung und Verifikation
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2019
• 资助国家: 德国
• 起止时间: 2018-12-31 至 2022-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/433044889?language=en
• 关键词: Parameter; Synthesis; Reliable; Performant; Efficient

Contemporary wireless technologies attempt to increase the level of reliability, performance and efficiency (RPE) of their services. This can be achieved by detecting faults in a very early stage of development. Therefore, it is of utmost importance that wireless protocols meet stringent specifications about functionality (``correct delivery within a few milliseconds in 99.999\% of the cases"), particularly when these technologies are employed in safety-critical scenarios, e.g., Mobile Ad-hoc Networks (MANETs) deployed in emergency response networks. Showing that a protocol adheres to such requirements cannot be guaranteed by typical protocol analysis techniques such as simulation. More rigorous, systematic approaches are needed. Formal model-based verification has an enormous potential in this regard.This project proposes a focused research effort to develop a formal framework to assist designing new wireless network protocols with provable guarantees on RPE. This is challenging in presence of characteristics such as real-time behaviour, uncertain environments, unreliable communication, energy efficiency, etc. In order to analyse the combination of different characteristics of wireless networks and their RPE, we will focus on the model of Probabilistic Timed Automata (PTA) and their extension with prices (Priced PTA). We are in particular interested in reasoning about unknown parameters in wireless systems. That is, probabilities and costs in the protocol model are not fixed, but can instead be given as expressions over some set of model parameters. Whereas formal verification evaluates RPE for a single, fixed instantiation of system parameters, analysing parametric protocol models focuses on synthesising many - all, almost all, or optimal - parameter values that establish a given reliability or performance specification. Such analysis answers queries such as what is the tolerable message loss probability such that the protocol guarantees correct delivery?, or what is the minimal expected energy consumption while still satisfying the overall protocol specification?Parameter synthesis gives provable - and not just statistical - guarantees. By synthesising parameters fulfilling requirements optimally, we will also be able to optimise RPE, e.g., minimising expected energy consumption. We aim at developing parameter synthesis algorithms for (P)PTA where parameters can be probabilities, timings, costs, or even their combination and apply these to automatically synthesise parameter values in wireless network protocols that attain the best RPE. In order to show the feasibility of our approach, we apply our framework to redesign and develop new variants of MANET and Vehicular Ad-hoc Network (VANET) routing protocols, e.g., AODV and OLSR protocols.

当代无线技术试图提高其服务的可靠性、性能和效率（RPE）水平。这可以通过在开发的早期阶段检测故障来实现。因此，无线协议满足关于功能的严格规范（"在99.999%的情况下在几毫秒内正确传递"）是极其重要的，特别是当这些技术被用于安全关键场景时，例如，部署在应急响应网络中的移动的Ad-hoc网络（MANET）。典型的协议分析技术，如仿真，不能保证一个协议遵守这样的要求。需要更严格、更系统的方法。基于模型的形式化验证在这方面具有巨大的潜力。本项目提出了一个集中的研究工作，以开发一个形式化的框架，以帮助设计新的无线网络协议与可证明的RPE保证。这是具有挑战性的存在的特点，如实时行为，不确定的环境，不可靠的通信，能源效率等，以分析无线网络及其RPE的不同特征的组合，我们将专注于概率时间自动机（PTA）的模型和他们的扩展与价格（定价PTA）。我们特别感兴趣的是在无线系统中的未知参数的推理。也就是说，协议模型中的概率和成本不是固定的，而是可以作为某组模型参数的表达式给出。而正式验证评估RPE的一个单一的，固定的系统参数的实例化，分析参数协议模型的重点是合成许多-所有，几乎所有，或最佳-参数值，建立一个给定的可靠性或性能规格。这样的分析回答了诸如什么是可容忍的消息丢失概率以使得协议保证正确的传递的查询，或者在仍然满足整个协议规范的同时最小预期能耗是多少？参数综合提供了可证明的--而不仅仅是统计上的--保证。通过最佳地合成满足要求的参数，我们还将能够优化RPE，例如，最小化预期的能源消耗。我们的目标是开发（P）PTA的参数合成算法，其中参数可以是概率、定时、成本甚至它们的组合，并应用这些来自动合成无线网络协议中的参数值，以获得最佳RPE。为了表明我们的方法的可行性，我们应用我们的框架重新设计和开发新的变体的移动自组网和车载自组网（VANET）路由协议，例如，AODV和OLSR协议。