一种基于扩展不完全Kripke结构的三值逻辑模型检测方法

多值模型检测是解决形式化验证中状态爆炸问题的一种重要方法,三值模型检测是多值模型检测的基础,其中如何检验不确定状态的真值是一难点。针对不确定状态检验,提出了一种模型检测方法,首先对不完全Kripke结构PKS进行了扩展,然后在扩展后的模型上给出了检测不确定状态真值的方法,最后给出了基于扩展不完全Kripke结构的三值逻辑模型检测算法。与已有的三值逻辑模型检测算法相比,该算法降低了算法复杂度,完善了对于不确定或不一致信息的处理,从而增强了三值逻辑模型检测的实用性。     

可能性测度下的CTL符号化模型检测

随着系统复杂性的增加,系统中的不确定信息亟待处理,状态爆炸问题也越来越严峻,现有的模型检测技术已不能完全适用于复杂系统的验证。 对可能性测度下CTL符号化模型检测进行了研究。首先用多终端二值决策图和布尔公式分别描述系统模型和待验证性质,然后再对系统模型进行归一化和简化,最后利用不动点计算完成系统验证。该研究是对可能性测度下的模型检测技术和符号化模型检测技术的整合,不但能处理系统的不确定信息,而且保持了符号化模型检测对计算时空要求低的优点,对于复杂系统模型检测具有重要意义。     

基于J2EE的网络地理信息系统的设计与实现

WebGUS(网络地理信息系统)实现了GIS信息数据在Internet上的获取、共享和发布。首先分析了当代WebGUS的运行模式和基于J2EE开发WebGUS的优势及其体系结构。然后设计和实现一个组件化的、多层的、分布式的WebGUS系统——DigitaINWU，指出了该系统具有的优点。     

语义标记Petri网的组合Web服务建模与验证(英文)

随着Web服务组合的发展,整合业务过程成为可能。组合Web服务可以被看作是基于过程的工作流。由于死锁、不安全和不可达等流的设计错误会影响组合Web服务的有效执行,因此这些错误应在组合Web服务执行前被检测出并修改。提出了基于语义标记Petri网的组合Web服务建模与验证方法。首先提出语义标记Petri网(SaPNs),并给出其语义;用受限描述逻辑tableau算法获得组合Web服务;使用SaPNs描述组合Web服务及其组成部分;最后,使用基于SaPNs的分析方法验证了组合Web服务。使用该方法在开放的Internet环境下可以获得满足客户需求的、可靠的组合Web服务。     

基于CTL模型检测的胃腺癌核心路径形式化验证

胃腺癌是消化系统最常见的恶性肿瘤,死亡率居消化道各类癌症之首。其发生发展是多步骤、多因素参与的复杂过程,涉及到多种蛋白分子的改变以及信号通路的异常,但其确切发病机制目前尚不清楚,研究其发病机理,探索有效治疗方法一直是医学研究最重要的课题之一。因此,对胃腺癌信号转导网络的研究有助于阐明其发病机制。目前,在胃腺癌的发生发展过程中由于基因的改变而导致细胞功能的变化,以及癌细胞环境因子通过作用于其受体和信号转导通路而影响其他正常细胞的功能。胃腺癌的信号转导网络非常复杂,通过对胃腺癌信号转导网络离散值模型的分析和验证,说明靶向胃腺癌信号通路或蛋白治疗的优越性。应用符号模型检测技术自动分析靶向信号通路或蛋白是如何影响胃腺癌细胞命运,了解胃腺癌的发生发展机理,从中找到潜在靶点,为治疗胃腺癌提供建议,使研制新的抗癌药物成为可能。     

操作系统课程双语教学的实践与思考

针对在操作系统课程中开展双语教学所面临的学生专业英语基础差和教学与实践相脱离等问题,在分析教学目的的基础上,提出"学以致用,循序渐进"的教学方法,并将该方法应用于课程的理论教学和实验教学。     

一种基于扩展有限自动机验证组合Web服务的方法

为简化并自动化组合Web服务验证,提出一种基于扩展有限自动机(extended deterministic finite automata,简称EDFA)验证组合Web服务的方法.使用EDFA可以准确地描述Web服务:EDFA的状态表达Web服务在与用户交互的过程中维护的状态;EDFA的状态转移及其标注描述Web服务与用户间的消息交换.EDFA给出Web服务交互过程的所有消息交换序列,刻画出Web服务的动态行为.使用基于EDFA的组合Web服务验证方法不但可以验证组合Web服务是否满足系统需求,还可以验证组合Web服务运行过程是否有逻辑错误.与其他方法相比,该方法更适于验证开放式环境下的组合Web服务.     

使用扩展区间时序逻辑为并发工作流建模

针对集中式体系结构并发工作流的两种运行方式（活动并发执行和活动以任意顺序执行），对区间时序逻辑进行扩展，提出两个新操作符“交错”和“限制性交错”．根据工作流状态的偏序关系以及逻辑公式连接前后其模型的长度关系，证明用新操作符连接的区间时序逻辑公式适于表示并发工作流．结合一个并发工作流实例，说明如何用扩展区间时序逻辑表示活动及由活动组建的并发工作流，从而得到并发工作流的区间时序逻辑模型．利用并发工作流的区间时序逻辑模型验证并发工作流的活性和安全性，可大大提高并发工作流设计的可靠性．     

师范类专业操作系统课程实验教学探索

针对师范类专业操作系统课程实验教学目的无法较好实现的问题,分析师范类学生的操作系统课程学习现状及社会发展对培养师范类专业学生的要求,提出利用Scratch完成操作系统课程实验的新方法,详细介绍了实验教学设计,最后分析实验成绩说明教学效果.     

可能性测度下的LTL模型检测并行化研究

分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量LTL验证算法并行化问题还未得到有效解决。对此,展开两个方面的工作:提出一种新的动态系统状态空间划分方法;在定性LTL分布式验证算法的基础上给出了定量模型检测并行化验证算法。首先,将系统模型转化为可能的Kripke结构并选取一个并发分量,依据状态之间的关系完成系统状态的分割,使得关系紧密的状态尽可能分布在同一个计算节点上;其次,调整划分结果以使得计算负载平衡;然后,将划分结果与其他并发分量的状态进行叉乘,以完成系统状态空间的划分;最后,将待检测性质用自动机表示,在两者的乘积上,利用扩展的基于嵌套DFS的分布式验证算法完成系统的定量验证。