机器人平台的硬件/软件接口工程--Prolog和Alloy的应用模型检验的比较
Engineering the Hardware/Software Interface for Robotic Platforms - A Comparison of Applied Model Checking with Prolog and Alloy
摘要：
机器人平台服务于不同的用例，从原型辅助应用的实验到在各个领域实现网络物理系统的嵌入式系统。我们正在使用1：10比例的微型车辆作为机器人平台，在自动驾驶汽车和协作车队领域进行研究。因此，使用不同传感器的实验，例如~超声波、红外线和旋转编码器需要使用我们的车辆平台来准备和实现。对于每个设置，我们需要配置硬件/软件接口板来处理所有传感器和执行器。因此，我们需要为接口板的每个引脚找到一个特定的配置设置，既可以处理我们当前的硬件设置，又足够灵活，可以为未来的用例支持更多的传感器或执行器。在本文中，我们展示了如何建模的硬件/软件接口板的配置空间域，使模型检验解决任务，找到任何，所有，最好的可能的引脚配置。我们提出了一个正式的实验结果，应用声明性语言合金和Prolog来指导工程的硬件/软件接口的机器人平台上的配置复杂性高达10引脚的配置空间大于1450万的可能性的例子的过程。我们的研究结果表明，我们的领域模型在合金相比，Prolog更好地找到可行的解决方案，为更大的配置，平均时间为0.58秒。为了找到最佳解决方案，我们的Prolog模型在最大所需配置下的性能更好，仅需1.38秒;然而，本文中作为示例使用的现有硬件工具目前没有涵盖这个重要的用例。
英文摘要：
Robotic platforms serve different use cases ranging from experiments for prototyping assistive applications up to embedded systems for realizing cyber-physical systems in various domains. We are using 1:10 scale miniature vehicles as a robotic platform to conduct research in the domain of self-driving cars and collaborative vehicle fleets. Thus, experiments with different sensors like e.g.~ultra-sonic, infrared, and rotary encoders need to be prepared and realized using our vehicle platform. For each setup, we need to configure the hardware/software interface board to handle all sensors and actors. Therefore, we need to find a specific configuration setting for each pin of the interface board that can handle our current hardware setup but which is also flexible enough to support further sensors or actors for future use cases. In this paper, we show how to model the domain of the configuration space for a hardware/software interface board to enable model checking for solving the tasks of finding any, all, and the best possible pin configuration. We present results from a formal experiment applying the declarative languages Alloy and Prolog to guide the process of engineering the hardware/software interface for robotic platforms on the example of a configuration complexity up to ten pins resulting in a configuration space greater than 14.5 million possibilities. Our results show that our domain model in Alloy performs better compared to Prolog to find feasible solutions for larger configurations with an average time of 0.58s. To find the best solution, our model for Prolog performs better taking only 1.38s for the largest desired configuration; however, this important use case is currently not covered by the existing tools for the hardware used as an example in this article.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
