期刊文献+
共找到11篇文章
< 1 >
每页显示 20 50 100
基于回答集语义复杂信息系统表单驱动需求规约的描述与验证
1
作者 万海 陈寅 +1 位作者 郑云翔 李磊 《小型微型计算机系统》 CSCD 北大核心 2011年第12期2345-2352,共8页
高品质的复杂信息系统软件设计与开发源自合理的、完整的和准确的软件需求.为了描述需求领域的非确定问题,并在需求获取不完全的情况下对需求规约进行非单调推理,本文将回答集逻辑程序和基于因果关系的动作理论应用于需求描述与验证.针... 高品质的复杂信息系统软件设计与开发源自合理的、完整的和准确的软件需求.为了描述需求领域的非确定问题,并在需求获取不完全的情况下对需求规约进行非单调推理,本文将回答集逻辑程序和基于因果关系的动作理论应用于需求描述与验证.针对复杂信息系统需求问题空间规模较大的特点,将动作描述语言C与动作查询语言Q结合形成动作语言Lo,作为需求描述的基础;通过分析需求领域各个元素及其相互关系,以表单驱动引导需求,并作为需求描述依据与核心,提出了描述需求问题空间静态关系和动态行为关系的"主谓宾状"需求模型MRspoa.利用回答集逻辑程序求解器SMODELS,可以对需求规约进行多层次规划与检测.本文的研究来自工程项目实践的总结与提高,研究成果得到具体应用. 展开更多
关键词 复杂信息系统 表单驱动 回答集语义 需求规约 需求描述验证
下载PDF
数字签名过程的一个形式描述和验证
2
作者 刘益和 《河南师范大学学报(自然科学版)》 CAS CSCD 北大核心 2005年第2期26-28,共3页
通过引入一些新概念,利用Biba模型思想,对一般的数字签名方案形式化描述和验证,并且该模型具有完整性.
关键词 BIBA模型 数字签名 形式化描述验证 完整性
下载PDF
基于组件的信息物理系统描述语言
3
作者 时雨霖 慈轶为 杨秋松 《计算机系统应用》 2017年第11期1-10,共10页
本文设计实现了一种基于组件的信息物理系统描述语言CDL(CPS Description Language).基于面向参量模型,将信息物理系统中的传感器、执行器和计算组件封装成具有统一抽象的组件,将系统描述分解为系统中包含的组件、组件之间的关联以及系... 本文设计实现了一种基于组件的信息物理系统描述语言CDL(CPS Description Language).基于面向参量模型,将信息物理系统中的传感器、执行器和计算组件封装成具有统一抽象的组件,将系统描述分解为系统中包含的组件、组件之间的关联以及系统约束三部分.实现了基于CDL的信息物理系统的设计实现工具,提供CDL生成、验证和安装的功能.最后设计实现了两个应用实例,验证了通过CDL来实现系统,可以减少开发者编写的代码量,提高编程效率,一定程度上降低系统设计实现的难度. 展开更多
关键词 信息物理系统 面向参量 系统描述 描述验证 图形化编辑 XML
下载PDF
一种验证数控系统软件安全可靠性的建模方法
4
作者 曹宇男 张辉 +1 位作者 叶佩青 王田苗 《系统仿真学报》 CAS CSCD 北大核心 2011年第3期425-432,共8页
作为一个典型的离散计算机控制系统,CNC(数字控制)系统在运行中需要满足可靠性和安全性。因此如何设计出安全可靠的系统软件以及如何有效地对CNC系统的安全性和可靠性进行验证成为一个非常重要的问题。基于此给出一个新的建模方法TTM/... 作为一个典型的离散计算机控制系统,CNC(数字控制)系统在运行中需要满足可靠性和安全性。因此如何设计出安全可靠的系统软件以及如何有效地对CNC系统的安全性和可靠性进行验证成为一个非常重要的问题。基于此给出一个新的建模方法TTM/ATRTTL(时间转化模型/全时轴实时时态逻辑)来描述和验证CNC系统。TTM/ATRTTL提供了一整套方法用于描述CNC系统建模的硬实时特性和反馈特性,也提供了一个包括一整套验证规则和定理的验证模型并且应用工具STeP和SF2STeP来实现之。这个验证模型可以用于对TTM/ATRTTL表达的系统的可靠性,安全性进行验证。使用该建模和验证方法可以对OAC(开放式体系结构CNC)系统进行分析和验证,并设计出OAC的逻辑控制器,该控制器是OAC系统的核心部分。验证结果表明,该形式化建模与验证方法可以有效地对CNC系统进行分析和建模。在此基础上,可以开发出能够保证系统可靠性和安全性的CNC系统软件。 展开更多
关键词 CNC 形式化描述验证方法 TTM/ATRTTL 可靠性 安全性
下载PDF
一种验证数控系统软件安全可靠性的建模方法
5
作者 曹宇男 陈友东 +1 位作者 魏洪兴 王田苗 《系统仿真学报》 CAS CSCD 北大核心 2009年第15期4572-4578,4582,共8页
作为一个典型的离散计算机控制系统,CNC(数字控制)系统在运行中需要满足可靠性和安全性。因此如何设计出安全可靠的系统软件以及如何有效地对CNC系统的安全性和可靠性进行验证成为一个非常重要的问题。基于此给出一个新的建模方法TTM/AT... 作为一个典型的离散计算机控制系统,CNC(数字控制)系统在运行中需要满足可靠性和安全性。因此如何设计出安全可靠的系统软件以及如何有效地对CNC系统的安全性和可靠性进行验证成为一个非常重要的问题。基于此给出一个新的建模方法TTM/ATRTTL(时间转化模型/全时轴实时时态逻辑)来描述和验证CNC系统。TTM/ATRTTL提供了一整套方法用于描述CNC系统建模的硬实时特性和反馈特性,也提供了一个包括一整套验证规则和定理的验证模型并且应用工具STeP和SF2STeP来实现之。这个验证模型可以用于对TTM/ATRTTL表达的系统的可靠性,安全性进行验证。使用该建模和验证方法可以对OAC(开放式体系结构CNC)系统进行分析和验证,并设计出OAC的逻辑控制器,该控制器是OAC系统的核心部分。验证结果表明,该形式化建模与验证方法可以有效地对CNC系统进行分析和建模。在此基础上,可以开发出能够保证系统可靠性和安全性的CNC系统软件。 展开更多
关键词 CNC 形式化描述验证方法 TTM/ATRTTL 可靠性 安全性
下载PDF
基于常规逻辑门和原理图方式的可逆逻辑描述
6
作者 郭荣田 赵曙光 梁晓雄 《电子科技》 2016年第9期139-141,144,共4页
针对可逆逻辑综合在设计较大规模可逆逻辑电路(ALU)时遇到的瓶颈问题。文中借用现行EDA技术的逻辑描述和验证能力,可逆逻辑门的功能表达式为依据,设计具有等功能的常规逻辑组合电路,通过等功能代换的方法,设计实现以常规原理图方式描述... 针对可逆逻辑综合在设计较大规模可逆逻辑电路(ALU)时遇到的瓶颈问题。文中借用现行EDA技术的逻辑描述和验证能力,可逆逻辑门的功能表达式为依据,设计具有等功能的常规逻辑组合电路,通过等功能代换的方法,设计实现以常规原理图方式描述的可逆ALU。仿真图中显示的16种运算结果表明,该方法具有一定的可行性和有效性。 展开更多
关键词 原理图方式 常规逻辑 可逆逻辑 等功能代换 功能性描述验证
下载PDF
开放式体系结构数控系统实时性的建模与分析 被引量:5
7
作者 曹宇男 张辉 +1 位作者 叶佩青 王田苗 《机械工程学报》 EI CAS CSCD 北大核心 2011年第1期108-116,共9页
给出一个新的用于描述开放式体系结构数控系统(Open architecture computerized numerical control system,OAC)的建模方法——时间转化模型/全时轴实时时态逻辑(Timed transition model/all-time real-time temporal logic,TTM/ATRTTL)... 给出一个新的用于描述开放式体系结构数控系统(Open architecture computerized numerical control system,OAC)的建模方法——时间转化模型/全时轴实时时态逻辑(Timed transition model/all-time real-time temporal logic,TTM/ATRTTL)。TTM/ATRTTL提供一整套方法用于对OAC系统的硬实时性和反馈特性进行建模并使用该形式化方法在系统层对OAC系统进行建模。分别给出开环OAC,系统级逻辑控制器以及任务间通信和同步机制的TTM模型,并最终给出具有调度机制的闭环OAC系统TTM模型。该模型为系统验证体系结构的基础。最后,给出系统验证体系结构并用模型验证工具STeP和CAD工具SF2STeP实现之。在系统验证过程中,首先解决STeP中遇到的若干模型验证问题,这些问题包括重写规则,验证规则,状态爆炸问题,以及时间约束限制问题。通过模型验证试验解决OAC系统运行过程中出现的死锁以及系统各模块执行时间约束检验问题。试验结果表明该方法可以有效地对OAC系统进行建模并对系统的实时特性进行验证。 展开更多
关键词 开放式体系结构数控系统 形式化描述验证方法 时间转化模型/全时轴实时时态逻辑 实时性 建模
下载PDF
基于安全本体的信息安全知识聚合技术研究 被引量:2
8
作者 梁中 周嘉坤 +1 位作者 朱汉 陈波 《信息网络安全》 CSCD 2017年第4期78-85,共8页
在信息安全教育资源的构建中,为使主题爬虫更全面、准确、快速地获取教育所需的信息安全领域知识,文章通过建立信息安全领域本体,为主题提供高度专业化的精准领域定义描述;通过安全本体描述中概念间的关系,扩展主题信息的语义范围,基于... 在信息安全教育资源的构建中,为使主题爬虫更全面、准确、快速地获取教育所需的信息安全领域知识,文章通过建立信息安全领域本体,为主题提供高度专业化的精准领域定义描述;通过安全本体描述中概念间的关系,扩展主题信息的语义范围,基于最大相关度引导下的深度优先遍历方法,对爬取的网页在语义概念层进行相关性分析,以提高主题爬虫信息爬取的准确率;采用广度优先搜索策略与链接相关度计算相结合的混合爬取策略,指导主题爬虫进行页面信息的爬取,以有效提升主题爬虫的爬取效率。通过与基于关键词描述的主题爬虫的对比实验验证了该方法的有效性。 展开更多
关键词 描述的主题爬虫的对比实验验证了该方法的有效性.关键词安全本体 安全教育 知识聚合 主题爬虫 信息安全
下载PDF
一种新的动态指配光网络资源的接口信令协议 被引量:1
9
作者 姚劲 迟彩霞 +2 位作者 郑小平 李艳和 张汉一 《电子学报》 EI CAS CSCD 北大核心 2003年第10期1441-1445,共5页
本文提出了一种新的用户光网络接口 (UNI)信令协议 ,以实现动态指配光网络资源的功能 .该协议支持多种类客户寻址 ,考虑了光网络的特殊要求 .采用通信有限状态机 (CFSM)模型对协议进行了形式化描述和验证 ,分析了协议设计的出错处理 .... 本文提出了一种新的用户光网络接口 (UNI)信令协议 ,以实现动态指配光网络资源的功能 .该协议支持多种类客户寻址 ,考虑了光网络的特殊要求 .采用通信有限状态机 (CFSM)模型对协议进行了形式化描述和验证 ,分析了协议设计的出错处理 .分析和验证结果表明 ,协议在网络正常和超时故障条件下均能确保对光通道的建立、修改、拆除和查询等操作无误 ,具有无死锁、无活锁。 展开更多
关键词 光网络 UNI接口 信令协议 形式化描述验证
下载PDF
A FVCOM-Based Unstructured Grid Wave, Current,Sediment Transport Model,I.Model Description and Validation 被引量:15
10
作者 WU Lunyu CHEN Changsheng +3 位作者 GUO Peifang SHI Maochong QI Jianhua GE Jianzhong 《Journal of Ocean University of China》 SCIE CAS 2011年第1期1-8,共8页
An effort was made to couple FVCOM (a three-dimensional (3D),unstructured grid,Finite Volume Coastal Ocean Model) and FVCOM-SWAVE (an unstructured grid,finite-volume surface wave model) for the study of nearshore ocea... An effort was made to couple FVCOM (a three-dimensional (3D),unstructured grid,Finite Volume Coastal Ocean Model) and FVCOM-SWAVE (an unstructured grid,finite-volume surface wave model) for the study of nearshore ocean processes such as tides,circulation,storm surge,waves,sediment transport,and morphological evolution.The coupling between FVCOM and FVCOM-SWAVE was achieved through incorporating 3D radiation stress,wave-current-sediment-related bottom boundary layer,sea surface stress parameterizations,and morphology process.FVCOM also includes a 3D sediment transport module.With accurate fitting of irregular coastlines,the model provides a unique tool to study sediment dynamics in coastal ocean,estuaries,and wetlands where local geometries are characterized by inlets,islands,and intertidal marsh zones.The model was validated by two standard benchmark tests: 1) spectral waves approaching a mild sloping beach and 2) morphological changes of seabed in an idealized tidal inlet.In Test 1,model results were compared with both analytical solutions and laboratory experiments.A further comparison was also made with the structured grid Regional Ocean Model System (ROMS),which provides an insight into the performance of the two models with the same open boundary forcing. 展开更多
关键词 FVCOM COUPLING radiation stress wave-current-sediment-related bottom boundary layer MORPHOLOGY
下载PDF
专用短程通信协议描述方法的研究及应用
11
作者 唐咏慧 钟慧玲 徐建闽 《通信技术》 2003年第12期91-93,96,共4页
DSRC协议是为ITS中短距离间通信的系统专门开发的通信协议。通过应用SDL语言对DSRC协议的描述和验证,提出了建立抽象化模型、环境模块化、循环开发等方法,并进行了MAC子层的概要性设计和MAC子层中的transmission模块的过程化设计,重点... DSRC协议是为ITS中短距离间通信的系统专门开发的通信协议。通过应用SDL语言对DSRC协议的描述和验证,提出了建立抽象化模型、环境模块化、循环开发等方法,并进行了MAC子层的概要性设计和MAC子层中的transmission模块的过程化设计,重点论述了如何将上述方法应用到实际开发工作中去。 展开更多
关键词 专用短程通信 DSRC协议 SDL 描述验证
原文传递
上一页 1 下一页 到第
使用帮助 返回顶部