形式规约

作品数:24被引量:122H指数:3
导出分析报告
相关领域:自动化与计算机技术更多>>
相关作者:陈海明董韫美张强张荣华王戟更多>>
相关机构:中国科学院软件研究所南京大学国防科学技术大学中国科学院研究生院更多>>
相关期刊:《计算机工程与应用》《湖南大学学报(自然科学版)》《计算机应用与软件》《数码世界》更多>>
相关基金:国家自然科学基金国家高技术研究发展计划“九五”国家科技攻关计划国家重点基础研究发展计划更多>>
-

检索结果分析

结果分析中...
条 记 录,以下是1-10
视图:
排序:
复杂系统规约、分析与验证发展现状与展望被引量:2
《前瞻科技》2023年第1期7-22,共16页詹乃军 王戟 
国家重点研发计划(2022YFA1005101);国家自然科学基金(62192732,62032024,61732001);中国科学院稳定支持基础研究领域青年团队计划(YSBR-040)。
形式化方法包括计算系统(软硬件和网络)的规约、构造、分析与验证的数学基础、技术和工具。随着安全攸关系统在国民经济和国防等关键领域的应用越来越多,复杂系统可信性问题日益凸显。形式化方法已经成为开发安全可靠的安全攸关系统的...
关键词:形式化方法 安全攸关系统 形式规约 形式分析与验证 
模糊安全性和活性被引量:1
《计算机科学》2021年第4期31-36,共6页石铁柱 钱俊彦 潘海玉 
国家自然科学基金(61672023);广西自然科学基金(2018GXNSFAA281326);广西可信软件重点实验室基金(kx201911)。
形式规约使用形式语言构建所开发的软硬件系统的规约,刻画系统的模型和性质。其中,性质规约中的分支时间规约对于系统验证有着非常重要的作用。在经典情形下,系统性质规约是基于二值逻辑的,不能描述不一致或不确定的信息。因此,将其推...
关键词:形式规约 模糊逻辑 分支时间属性 安全性 活性 
形式化方法概貌被引量:91
《软件学报》2019年第1期33-61,共29页王戟 詹乃军 冯新宇 刘志明 
国家自然科学基金(61532007;61632005;61672435;61732019)~~
形式化方法是基于严格数学基础,对计算机硬件和软件系统进行描述、开发和验证的技术.其数学基础建立在形式语言、语义和推理证明三位一体的形式逻辑系统之上.形式化方法已经以不同程度和不同方式愈来愈多地应用在计算系统生命周期的各...
关键词:形式化方法 形式规约 形式验证 程序设计方法学 软件开发 
在线考试系统考生考试过程的形式化描述
《数码世界》2018年第9期223-223,共1页王可心 
为加深对用例模型形式化描述方法的理解,本文将以在线考试系统中学生在线考试过程为例,说明在一个应用中如何利用B方法对用例模型进行形式化描述。
关键词:用例模型 形式化方法 B形式规约 
形式化方法在藏文软件开发中的应用研究
《甘肃高师学报》2017年第3期28-30,共3页马小龙 
2014年度甘肃省高等学校科研项目"形式化软件开发方法在藏文软件开发中的应用"(2014A-115)
形式化方法有助于软件开发中发现其它方法不容易发现的系统描述的不一致、不明确或不完整,增加软件开发人员对系统的理解,利用形式化方法开发的软件系统具有较高的可信度和正确性,并能使系统具有良好的结构,使其易维护,关键是能较好地...
关键词:形式化方法 藏文软件 形式规约 形式化验证 
面向动作的上下文感知应用的规约与运行时验证被引量:3
《软件学报》2017年第5期1167-1182,共16页李晅松 陶先平 吕建 宋巍 
国家自然科学基金(61373011;61202003;61502225)~~
面向动作的上下文感知(activity-oriented context-aware,简称AOCA)应用组织环境中的资源,为用户动作的顺利进行提供支持.为应对环境和动作相关需求的开放性,这类应用采用轻量级、增量式的开发方法进行开发.相对于在开发阶段描述全局信...
关键词:普适计算 上下文感知 形式规约 运行时验证 
UML类图的形式规约与精化研究被引量:3
《计算机应用与软件》2017年第2期1-7,47,共8页王博文 盛枫 窦亮 杨宗源 
国家自然科学基金项目(61070226)
UML由于其广泛的应用和直观的图形化符号,成为了模型驱动工程的重要组成部分。但UML本身缺乏精确的形式语义定义,缺少对其模型精化关系的形式化规范定义,对UML模型进行形式验证变得尤为困难。UML类图作为描述系统结构的静态模型,不具备...
关键词:UML类图 模型精化 Coq机械语意 
浅析形式化描述方法的应用被引量:1
《电子技术与软件工程》2014年第10期107-108,共2页冯松军 
形式化方法是一种使用严格的数学模型和方法准确、抽象、规范地描述和验证软件系统的行为和性能的方法,其中主要包括软件的需求规格、设计和实现等。使用这种描述方法可以帮助开发者发现软件系统的设计、实现和程序中的问题和缺陷,能够...
关键词:软件工程 形式化描述 形式规约语言 Z语言 
基于顺序失效符的动态故障树形式规约被引量:2
《北京航空航天大学学报》2012年第9期1255-1260,共6页王波 刘东 李艺 
国家自然科学基金资助项目(60904082)
首先定义了顺序失效符(SFS,Sequence Failure Symbol)的形式化框架,包括SFS定义、性质、规则和定理,这是动态故障树(DFT,Dynamic Fault Tree)形式规约的基础.然后给出了任意形式的静态故障树(SFT,Static Fault Tree)和DFT在SFS形式化框...
关键词:动态故障树 顺序失效 形式规约 
一种结合UML和B的软件需求获取方法被引量:1
《重庆科技学院学报(自然科学版)》2012年第3期142-146,共5页王友 
安徽省社科联基金项目(B2011019);蚌埠学院校内基金项目(2010SK20)
精确的软件需求是软件质量的保证,UML在软件需求中起着重要的作用,它用于描述软件的需求模型、对象模型、动态模型和部署模型。然而UML缺乏形式化方法的准确语义,很难产生准确无歧义的软件规约。使用B和UML结合的方法,借助形式化方法的...
关键词:B方法 UML 形式规约 家庭智能控制系统 
检索报告 对象比较 聚类工具 使用帮助 返回顶部