计算机网络精品课程建设经验

针对广西区级计算机网络精品课程在改革和建设中所取得的成果,本文从课程教学内容、方法与手段、教材、网站和师资队伍等几个方面总结相关的建设经验并进行分析,为改进计算机网络课程教学提供具有借鉴意义的经验并指出进一步提升该课程教学质量的工作方向。     

回答集程序设计在TTP求解中的应用

课程表问题是一个应用广泛、典型的组合优化和不确性调度问题,目前存在的求解算法多数缺乏声明性。一种基于回答集程序设计的TTP求解方法,可成功生成正确解集（答案）,并用实验结果论证了算法的可行性。     

一种基于自动机理论的LTL检验符号优化方法

模型检验是一种重要的形式化自动验证技术。检验一个模型是否满足LTL公式,可以把LTL公式转换为一个表示相同无穷状态序列的ω自动机,通过转换后的ω自动机与系统自动机的乘积判空来进行模型检验。由于自动机的体积是模型检验的一个关键性问题,为了得到尽可能小的自动机,在LTL公式转换为ω自动机之前,对LTL公式进行预处理来减少冗余,然后基于ROBDD,通过布尔技术优化自动机。     

基于关键迹和ASP的CSP模型检测

模型检测是通信顺序进程(communicating sequential processes,简称CSP)形式化验证的重要手段.当前, CSP模型检测方法基于操作语义,需将进程转化为迁移系统,进而提取语义模型,但转化过程较为复杂;待验证性质采用CSP语言进行描述,虽然有利于精炼检测(refinement checking),但描述能力较弱,通用性不强.鉴于此,提出了一种新的CSP指称语义模型——关键迹模型(critical-trace model)及基于该指称语义模型的CSP模型检测方法,并证明了其验证的可靠性,避免了上述问题.关键迹模型采用递归策略计算,待验证性质采用线性时态逻辑(linear temporal logic,简称LTL)描述.基于回答集程序设计(answer set programming,简称ASP)实现了关键迹模型的自动生成及LTL的自动验证,并开发了一个CSP模型检测原型系统——T_ASP.实验结果表明:与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,且可同时验证多条性质,在性质不满足时还可提供多条反例.     

基于ASP的CSP进程描述与组合研究

前期工作中,为解决CSP模型检测不支持一次运行验证多条性质的问题,构建了基于ASP的CSP模型检测框架,但其存在着可描述并发进程形态不完善与可验证并发系统规模受限的问题。构建了全新的并发系统ASP描述体系,其解决了前期工作中前缀描述不允许出现类环状结构的问题,可完整描述各种形态的CSP进程。研究了并发组合进程生成技术,它可使多个进程自动化并发组合,并生成一个满足所有行为特性、具有一致结构特性的新进程,保持了验证框架内进程描述的一致性,有利于并发进程的抽象与验证。实验表明了基于ASP的CSP进程描述与组合进程生成技术的有效性,以及基于该ASP描述体系的系统性质验证的可行性。     

一种基于熵的OBDD变量排序算法

有序二叉决策图（OBDD）是一种有效表示布尔函数的数据结构，其大小依赖于所采用的变量序。熵是定量描述布尔函数中变量重要性的一种方法。基于变量的熵值分析了高质量变量序的特征，给出了一种基于熵的OBDD变量排序算法。实验结果表明：该算法与模拟退火算法和遗传算法结果相当。时间仅为相应算法的80．84％和29．79％。     

基于启发式搜索的 ASP程序支撑原因分析算法

为了尽快找到一个错误及其来源,以加快 ASP程序调试的效率,把启发式搜索技术引入 ASP程序支撑原因分析算法.在生成支撑原因分析图时利用启发式函数,仅搜索对回答集产生影响且有可能更快找到一个支撑原因的规则.改进算法在搜索关于某个回答集的支撑原因时,其时间和空间复杂度明显下降.实例分析表明了该算法的有效性.     

基于ASP的程序切片

针对程序切片在程序理解和程序测试方面的应用,提出了一种基于ASP的程序切片方法.ASP是一种声明性问题解决方法,它可以高效地描述程序切片问题,基于ASP的切片方法,可以把切片的查找转化为回答集的求解.另外,对传统数据流切片算法进行了改进;改进后的算法可以减少重复计算,提高了运行效率.通过实验表明了此改进法的正确性和高效性;并且比较了3种ASP求解器(DLV、Smodels、Cmodels)的执行效搴,基于Cmodels的改进算法的运行效率是最高的.