基于LTL预测语义的高效监控器构造

运行时验证中的一个重要研究内容就是从高层规约生成高效的监控器,并有效控制监控器的生成复杂度与监控器运行时开销.基于线性时序逻辑(LTL)的预测语义,通过删除与合并Büchi自动机中的大部分状态,提出一种高效的预测监控器构造技术.通过该方法,可以大大降低最终预测监控器的规模,提高监控器产生的效率;同时保证把监控器的运行时开销控制在合理的范围内.基于上述预测监控器构造技术,实现了相应工具monitor_tool,该工具比LTL3_tool工具更小,且能够为更多的LTL性质产生监控器. 同时,产生的监控器能够尽可能早的识别一个持续被监控的执行轨迹是否满足指定的正确性性质.     

跌倒防护机器人的用户接受度模型

跌倒防护机器人解决了老年群体由于跌倒造成伤亡的社会问题，为探究老年用户对其接受度问题，以基础技术接受模型为基础，将感知易用性、感知有用性、使用态度、行为意向、技术信任度、社会规范、个人创新意识、面子文化、舒适度9个变量纳入分析，提出12项假设，构建了跌倒防护机器人的接受度模型。通过李克特5点量表测量变量，并结合结构方程模型进行数学分析，探究变量间的相互作用关系。结果表明：9个变量之间的作用具有显著性，12项假设全部成立，跌倒防护机器人接受度模型具有较好的拟合性。可见，研究成果可以为进一步探讨跌倒防护机器人的设计、开发、推广和普及提供有效参考。