作者：叶玲玲; 钱俊彦; 查显伟运行时验证javamop监控器线性时态逻辑buchi自动机
摘要：为了提高JavaMOP对程序运行时验证的效率,提出一种基于Büchi自动机化简的JavaMOP监控器构造方法,降低JavaMOP运行时验证的时间和内存开销。该方法将线性时态逻辑(linear temporal logic,简称LTL)描述的属性规范转化为Büchi自动机,利用自动机化简规则对Büchi自动机进行冗余化简,化简后的Büchi自动机再转化为确定性有限自动机,并由此得到监控器的抽象表示。实验结果表明,与JavaMOP现有监控器的方法相比,该方法能够得到更小的Büchi自动机,从而加速JavaMOP监控器的构造过程。
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
《桂林电子科技大学学报》（CN：45-1351/TN）是一本有较高学术价值的大型双月刊，自创刊以来，选题新奇而不失报道广度，服务大众而不失理论高度。颇受业界和广大读者的关注和好评。 《桂林电子科技大学学报》主要刊载信息与通信工程、信号与信息处理、计算机应用技术、仪器科学与技术、控制理论与控制工程、机械设计制造及其自动化、电磁场与微波技术、机械电子工程、工业艺术设计、材料加工工程、信息与计算科学、应用数学、工商管理等方面的学术论文。
杂志详情
