一种自动的形式化验证技术——模型检测

1

作者 化志章 揭安全 薛锦云 《微计算机信息》 北大核心 2007年第33期254-256,222,共4页

模型检测是针对有限状态系统行为的逻辑性质的一种自动验证技术,已有许多工业应用.其主要缺陷是空间爆炸问题.本文通过一简单实例介绍其基本思想、检测步骤和相关理论,给出一些处理状态空间爆炸问题的优化技术,并与其它验证方法进行了比... 模型检测是针对有限状态系统行为的逻辑性质的一种自动验证技术,已有许多工业应用.其主要缺陷是空间爆炸问题.本文通过一简单实例介绍其基本思想、检测步骤和相关理论,给出一些处理状态空间爆炸问题的优化技术,并与其它验证方法进行了比较,最后简单介绍了软件模型检测的新进展. 展开更多

关键词 模型检测 形式验证 时态逻辑

在线阅读 下载PDF 职称材料

基于RBAC的高校办公自动化系统设计 被引量：11

2

作者 揭安全 化志章 +1 位作者 薛锦云 李云清 《计算机工程与设计》 CSCD 北大核心 2009年第11期2800-2802,2805,共4页

分析了基于角色的访问控制的工作原理,提出了一种基于Web应用的RBAC权限控制有效实现方法,并将其应用于高校办公自动化系统设计。介绍了OA系统的设计与配置方法,重点阐述了基于Web的RBAC控制模型在OA系统中的实现方法。基于该模式开发... 分析了基于角色的访问控制的工作原理,提出了一种基于Web应用的RBAC权限控制有效实现方法,并将其应用于高校办公自动化系统设计。介绍了OA系统的设计与配置方法,重点阐述了基于Web的RBAC控制模型在OA系统中的实现方法。基于该模式开发的系统具有较高的安全性与稳定性,很好地满足了高等学校办公自动化的需求。 展开更多

关键词 角色 权限 访问控制 RBAC 办公自动化

在线阅读 下载PDF 职称材料

形式推导支持的递归程序向非递归程序的转换 被引量：5

3

作者 化志章 揭安全 +1 位作者 李云清 薛锦云 《计算机工程与科学》 CSCD 2007年第10期145-147,F0003,共4页

本文提出一种递归消除的方法,适于一类基于递归数据结构的程序。该方法将递归程序作为初始规约,以求解过程的状态变迁序列作迭代模式;通过数据展开和变换实现初始规约向基于序列描述规约的变换,继而用PAR形式推导出序列规约的递推关系,... 本文提出一种递归消除的方法,适于一类基于递归数据结构的程序。该方法将递归程序作为初始规约,以求解过程的状态变迁序列作迭代模式;通过数据展开和变换实现初始规约向基于序列描述规约的变换,继而用PAR形式推导出序列规约的递推关系,并以之为核心近乎机械地构造出非递归算法。树和图的两个算法实例说明了本方法的有效性。 展开更多

关键词 算法推导 形式方法 递归程序变换 PAR方法

在线阅读 下载PDF 职称材料

软件模型检测新技术研究 被引量：3

4

作者 化志章 吴传孙 +1 位作者 揭安全 薛锦云 《微计算机信息》 北大核心 2007年第36期250-251,311,共3页

软件模型检测以其潜在的商业价值一直为学术界和工业界关注.本文通过剖析模型检测工具SLAM,探讨软件模型检测的机理、方法及若干核心技术,并总结出软件模型检测的一些新策略.

关键词 软件模型检测 形式验证 SLAM

在线阅读 下载PDF 职称材料

树非递归遍历统一的新解法及其形式证明 被引量：1

5

作者 化志章 杨庆红 揭安全 《江西师范大学学报（自然科学版）》 CAS 北大核心 2010年第2期123-127,共5页

提出树遍历统一的新解法,使其非递归算法像递归算法一样简单.首先以后序遍历为例,基于结点状态标记和遍历规则提取,从遍历定义导出遍历的递推公式,由此机械获得非递归算法和循环不变式,并用形式化方法证明其正确性.之后按不同遍历定义... 提出树遍历统一的新解法,使其非递归算法像递归算法一样简单.首先以后序遍历为例,基于结点状态标记和遍历规则提取,从遍历定义导出遍历的递推公式,由此机械获得非递归算法和循环不变式,并用形式化方法证明其正确性.之后按不同遍历定义变换公式参数,获得二叉树前序、中序和K叉树前序、后序的递推公式,所得算法比传统算法更简洁直观,表明本解法的有效性和通用性. 展开更多

关键词 树遍历 非递归算法 循环不变式

在线阅读 下载PDF 职称材料

面向综合实践能力培养的OOP课程教学新实践 被引量：1

6

作者 化志章 揭安全 +3 位作者 王岚 石海鹤 钟林辉 万中英 《计算机教育》 2022年第4期155-158,共4页

为实现面向对象程序设计(OOP)课程的培养目标,针对综合实践能力培养,提出以“举一反三”能力作为突破口,用OBE理念指导基于案例的内容重塑和教学设计,形成以“精通基础设计框架、拥有丰富实践经验、具备专业思维能力”为特色的教学实施... 为实现面向对象程序设计(OOP)课程的培养目标,针对综合实践能力培养,提出以“举一反三”能力作为突破口,用OBE理念指导基于案例的内容重塑和教学设计,形成以“精通基础设计框架、拥有丰富实践经验、具备专业思维能力”为特色的教学实施方案;通过六轮实践的结果分析,说明学生学习的主动性被有效激发,综合设计水平显著提升。 展开更多

关键词 OOP 学为中心 过程性考核 能力培养

在线阅读 下载PDF 职称材料

计算机程序设计教学辅助平台设计初探 被引量：2

7

作者 化志章 揭安全 甘登文 《计算机与现代化》 2002年第12期1-3,8,共4页

吸收了几何实验室教学智能平台的一些先进思想 ,将之应用于计算机程序设计 ,提出以研究、提炼程序设计知识元件为基础 ,研发计算机程序设计教学辅助平台的设想。并对平台的内容、特色及框架作了初步探讨 ,对实现的可行性也作了简单的分析。

关键词 计算机 程序设计 教学辅助平台 设计 计算机辅助教学

在线阅读 下载PDF 职称材料

计算机程序设计ICAI教学决策实验系统研究 被引量：1

8

作者 化志章 揭安全 薛锦云 《计算机与现代化》 2002年第8期1-5,55,共6页

PAR方法是一种实用统一的形式化程序设计方法 ,并有以PAR方法为指导思想的计算机程序设计ICAI模型。本文实现该模型的教学决策部分。首先基于建构主义等认知理论以及程序设计知识的自身特点 ,研究设计了领域知识库、学生知识库和教师知... PAR方法是一种实用统一的形式化程序设计方法 ,并有以PAR方法为指导思想的计算机程序设计ICAI模型。本文实现该模型的教学决策部分。首先基于建构主义等认知理论以及程序设计知识的自身特点 ,研究设计了领域知识库、学生知识库和教师知识库 ,并按照启发式教学方式 ,归纳整理出一些教学决策规则 ,选用适当的方式组织、描述相关知识、规则 ,建立系统决策模型。已经在PC机上用Java语言结合Access数据库实现了此实验系统。此实验系统能够根据配套的测试实验系统的测试结果 ,选取相应的教学策略和教学内容 。 展开更多

关键词 计算机 程序设计 ICAI 教学决策实验系统 知识库

在线阅读 下载PDF 职称材料

基于遍历序列恢复二叉树的新解法及其证明 被引量：2

9

作者 化志章 《江西师范大学学报（自然科学版）》 CAS 北大核心 2013年第3期268-272,共5页

提出了一种基于前序和中序遍历序列恢复二叉树的解法,算法以数学公式形式呈现,反映了建树过程中相关数据变化的一般规律,具备数学上的引用透明性,由此能机械获得非递归程序和循环不变式,并进行了正确性证明.通过简单变换,获得了后序+中... 提出了一种基于前序和中序遍历序列恢复二叉树的解法,算法以数学公式形式呈现,反映了建树过程中相关数据变化的一般规律,具备数学上的引用透明性,由此能机械获得非递归程序和循环不变式,并进行了正确性证明.通过简单变换,获得了后序+中序、前序+后序恢复二叉树的可信算法.实验效果表明了该解法的有效性. 展开更多

关键词 状态变迁 二叉树遍历 恢复二叉树 循环不变式

在线阅读 下载PDF 职称材料

数据结构实践教学体系的设计与实施 被引量：8

10

作者 揭安全 李云清 +2 位作者 杨庆红 化志章 王岚 《计算机教育》 2010年第17期85-88,共4页

数据结构是一门理论性与实践性都很强的课程,数据结构实践教学体系的建设对于学生实践能力和创新能力的培养起着重要的作用。该文结合数据结构课程的特点,从实践内容的设计优化、教学模式和教学手段几个方面出发,探讨了数据结构实践体... 数据结构是一门理论性与实践性都很强的课程,数据结构实践教学体系的建设对于学生实践能力和创新能力的培养起着重要的作用。该文结合数据结构课程的特点,从实践内容的设计优化、教学模式和教学手段几个方面出发,探讨了数据结构实践体系的建设思路、建设过程和取得的主要成效。 展开更多

关键词 数据结构 实践教学体系 教学改革 教学模式

在线阅读 下载PDF 职称材料

项目教学模式指导的“数据结构与算法”教学改革 被引量：8

11

作者 揭安全 李云清 +2 位作者 杨庆红 化志章 王岚 《计算机教育》 2008年第22期21-23,40,共4页

“数据结构与算法”是计算机科学技术专业重要的专业课程，该课程的教与学都有相当的难度。近年来，我们在该课程中引入了项目式教学方法，通过精心设计项目，以软件工程思想指导项目式教学过程，将师范教师教育与专业教育相融合等一系... “数据结构与算法”是计算机科学技术专业重要的专业课程，该课程的教与学都有相当的难度。近年来，我们在该课程中引入了项目式教学方法，通过精心设计项目，以软件工程思想指导项目式教学过程，将师范教师教育与专业教育相融合等一系列教学改革，取得了显著的教学成效。本文介绍了我院的这些经验。 展开更多

关键词 数据结构与算法 教学改革 项目 教学模式

在线阅读 下载PDF 职称材料

“数据结构”课程教学改革与创新 被引量：5

12

作者 揭安全 李云清 +2 位作者 杨庆红 化志章 王岚 《计算机教育》 2008年第10期132-133,共2页

本文介绍了江西师范大学“数据结构”课程组以课程建设为主线，以全面提高课程教学质量为目标，以促进教学团队建设为宗旨，以现代教育理论为指导，对该课程进行一系列的教学综合改革的实践体会。

关键词 数据结构 教学改革 课程建设 网络协作教学模式

在线阅读 下载PDF 职称材料

接口技术课虚拟实验环境的设计与实现 被引量：2

13

作者 揭安全 化志章 薛锦云 《计算机与现代化》 2002年第8期56-58,共3页

利用软件技术构建硬件虚拟实验环境 (VEE)是提高计算机硬件教学及实验效率、降低实验成本的一条有效途径。本文以接口技术课CAI为例 ,首先介绍了VEE的概念及特征 ,总结出VEE的一些开发原则及开发策略。并最终以接口技术CAI课件的形式部... 利用软件技术构建硬件虚拟实验环境 (VEE)是提高计算机硬件教学及实验效率、降低实验成本的一条有效途径。本文以接口技术课CAI为例 ,首先介绍了VEE的概念及特征 ,总结出VEE的一些开发原则及开发策略。并最终以接口技术CAI课件的形式部分实现了VEE环境 。 展开更多

关键词 接口技术课 虚拟实验环境 设计 计算机辅助教学

在线阅读 下载PDF 职称材料

基于嵌入式平台的并发虚拟机研究 被引量：1

14

作者 揭安全 化志章 +1 位作者 杜大威 薛锦云 《微计算机信息》 北大核心 2008年第23期88-90,共3页

并发程序对提高应用系统的处理能力具有重要作用,基于嵌入式平台的并发程序开发尚无统一的工具支持。本文提出了一种基于嵌入式平台的并发虚拟机(CVM)设计思想,并采用标准C实现了一个CVM模型。研究表明,它可以支持嵌入式平台中的并发程... 并发程序对提高应用系统的处理能力具有重要作用,基于嵌入式平台的并发程序开发尚无统一的工具支持。本文提出了一种基于嵌入式平台的并发虚拟机(CVM)设计思想,并采用标准C实现了一个CVM模型。研究表明,它可以支持嵌入式平台中的并发程序,实现了嵌入式平台中并发程序的平台无关性和可移植性。 展开更多

关键词 嵌入式平台 并发 虚拟机 CVM

在线阅读 下载PDF 职称材料

MAFDNet:复杂环境下图像自适应分类新方法

15

作者 叶继华 黎欣 +3 位作者 陈进 江爱文 化志章 万文涛 《数据采集与处理》 CSCD 北大核心 2023年第6期1392-1405,共14页

复杂环境下,往往困难样本和简单样本并存,现有分类方法主要针对困难样本进行设计,所构建网络用于分类简单样本时会造成计算资源的浪费;而网络修剪和权重量化等方法则不能同时兼顾模型的准确度和存储开销。为提升计算资源的使用效率并有... 复杂环境下,往往困难样本和简单样本并存,现有分类方法主要针对困难样本进行设计,所构建网络用于分类简单样本时会造成计算资源的浪费;而网络修剪和权重量化等方法则不能同时兼顾模型的准确度和存储开销。为提升计算资源的使用效率并有更好的准确率,本文着眼于输入样本的空间冗余,提出了复杂环境下图像自适应分类网络MAFDNet,并引入置信度作为分类准确性的判断,同时提出了由内容损失、融合损失和分类损失组成的自适应损失函数。MAFDNet由3个子网组成,输入图像首先被送入到低分辨率子网中,该子网有效提取了低分辨率的特征,具有高置信度的样本先被识别并从网络中提前退出,低置信度的样本则需要依次进入更高分辨率的子网中,而网络中的高分辨率子网具有识别困难样本的能力。MAFDNet将分辨率自适应和深度自适应结合在一起,通过实验表明,在相同计算资源条件下,MAFDNet在CIFAR?10、CIFAR?100和ImageNet这3个复杂环境数据集上的top?1准确率均得到提升。 展开更多

关键词 MAFDNet 复杂环境 自适应分类 自适应损失 置信度

在线阅读 下载PDF 职称材料

UNITY与典型程序设计模型的比较

16

作者 肖美华 薛锦云 化志章 《计算机工程与应用》 CSCD 北大核心 2003年第32期52-54,104,共4页

UNITY是一种简单统一的理论、计算模型和证明系统,而且具有很强的把UNITY程序映射成不同的计算机体系结构模式的能力。该文在简述UNITY机理的基础上,分析UNITY与几种典型的程序设计模型(函数式、命令式、逻辑式、基于规则式、Petri网、C... UNITY是一种简单统一的理论、计算模型和证明系统,而且具有很强的把UNITY程序映射成不同的计算机体系结构模式的能力。该文在简述UNITY机理的基础上,分析UNITY与几种典型的程序设计模型(函数式、命令式、逻辑式、基于规则式、Petri网、CSP)的区别,并给出它们对应的等价UNITY程序转换,最后,介绍Seuss对完善UNITY的新策略。 展开更多

关键词 程序设计模型 UNITY形式语义 程序转换 Seuss

在线阅读 下载PDF 职称材料