摘要：排队网络是一种常见的对供应链、生产线以及交通系统等进行建模的工具,可以被用来分析系统中各资源的利用率,并对系统结构的设计提供指导.相比较于利用仿真进行分析,排队网络可以更快速地得到系统的资源利用率.在实际中,常用闭环Jackson网络来对顾客总数不变的封闭系统进行建模.在本文中,首先利用闭环Jackson网络归一化参数的母函数,得到了网络中各节点利用率的解析表达式.通过对利用率解析表达式的分析,给出了在顾客总数趋于无穷时利用率的极限,并证明了利用率是饱和函数.在这些结论的基础上,进一步计算不同服务时间下达到饱和状态所需的顾客总数.最后将该方法应用于一个实际的自动化码头例子,将其建模为闭环Jackson网络,分析码头的瓶颈所在,计算系统饱和点对应的车辆数,并与仿真实验进行了对比.

摘要：随着硬件设计复杂性和规模的大幅度提升,硬件验证工作更加具有挑战性。模型检验技术作为一种自动化验证技术,可以自动构建反例路径,也因此成为硬件验证领域内最重要的研究方向之一。IC3算法是近些年来最成功的比特级别的硬件验证算法。为了提高验证的规模和效率,硬件验证算法设计逐渐从底层的比特级向更高的抽象级别转变。研究目标是设计一个新型有效的字级IC3算法。针对研究目标,提出了一种将变量隐藏抽象和隐式抽象结合的字级IC3算法IC3VA。该方法尝试将变量隐藏抽象和IC3算法相结合,并设计了对应的泛化和精化方案。在开源社区和硬件验证大赛收集的测试集上和基于谓词抽象的方法进行对比,实验结果显示了基于变量隐藏抽象的IC3算法的有效性。