期刊文献+
共找到17篇文章
< 1 >
每页显示 20 50 100
软件形式化与可视化软件模型的转换 被引量:8
1
作者 周彦晖 张为群 《计算机科学》 CSCD 北大核心 2003年第7期106-109,共4页
It is an important issue in Software Engineering that combined the formal development method with the vi-sual development method. This study is about the transform method and rules between the UML model and theRAISE m... It is an important issue in Software Engineering that combined the formal development method with the vi-sual development method. This study is about the transform method and rules between the UML model and theRAISE model. At last try to put this technology and the common software develop process together. 展开更多
关键词 面向对象 软件开发 软件形式化 可视化软件模型
下载PDF
软件形式化建模方法探析 被引量:1
2
作者 周建儒 《河北软件职业技术学院学报》 2016年第2期48-50,共3页
传统软件开发流程存在各种缺陷。软件形式化方法是建立在严格数学基础上的软件开发方法,该方法为从根本上解决传统软件开发过程中存在的主要缺陷提供了可能,其中Pi验算就是比较典型的一种形式化语言,结合实例来分析Pi验算进行形式化建... 传统软件开发流程存在各种缺陷。软件形式化方法是建立在严格数学基础上的软件开发方法,该方法为从根本上解决传统软件开发过程中存在的主要缺陷提供了可能,其中Pi验算就是比较典型的一种形式化语言,结合实例来分析Pi验算进行形式化建模的过程,可以帮助我们更好地了解这种形式化语言建模方式。 展开更多
关键词 软件形式化 Pi验算 软件工程 建模方式
下载PDF
实验设备管理软件形式化描述方法研究
3
作者 章昱 邹成武 《电子技术与软件工程》 2017年第21期41-43,共3页
针对常规的软件描述方法不够严谨,本文介绍了软件形式化方法的特点和技术类别,介绍了Z语言的表达方式及其各自的特点。然后本文使用Z语言分析了实验设备管理软件,给出了部分形式化分析结果。结果表明,Z语言能够将数理逻辑完备用于的描... 针对常规的软件描述方法不够严谨,本文介绍了软件形式化方法的特点和技术类别,介绍了Z语言的表达方式及其各自的特点。然后本文使用Z语言分析了实验设备管理软件,给出了部分形式化分析结果。结果表明,Z语言能够将数理逻辑完备用于的描述软件的功能,有效避免描述的模糊性。 展开更多
关键词 软件形式化 Z语言 设备管理
下载PDF
一个机载软件需求形式化建模与分析实例研究 被引量:2
4
作者 胡军 吕佳润 +3 位作者 王立松 康介祥 王辉 高忠杰 《软件学报》 EI CSCD 北大核心 2022年第5期1652-1673,共22页
现代民机机载软件系统的功能与复杂度在快速增长的同时还必须满足更严格的安全标准,使得在机载软件需求层级必须进行诸如一致性、完整性等分析与验证成为重要的挑战.工作基于一个自主设计实现的面向机载软件自然语言需求形式化建模与分... 现代民机机载软件系统的功能与复杂度在快速增长的同时还必须满足更严格的安全标准,使得在机载软件需求层级必须进行诸如一致性、完整性等分析与验证成为重要的挑战.工作基于一个自主设计实现的面向机载软件自然语言需求形式化建模与分析工具平台(ART)展开对座舱显控软件子系统(EICAS)需求的建模与分析,包括:ART工具平台所采用的变量关系(VRM)理论模型、平台架构和平台工具链,基于多范式的需求一致性、完整性形式化分析方法,EICAS系统的条目化初始自然语言需求的形式化建模和需求模型的自动化分析过程,如:需求条目的预处理、规范化处理、需求模型自动生成以及多范式分析等;给出了工程需求实例研究的经验总结和思考. 展开更多
关键词 机载软件形式化建模 变量关系模型 自然语言需求建模 形式化方法
下载PDF
基于问题模式的形式化软件规格说明生成方法 被引量:5
5
作者 王昌晶 罗海梅 左正康 《计算机研究与发展》 EI CSCD 北大核心 2013年第2期352-360,共9页
精确的形式化软件规格说明是软件描述、开发与验证的基础,而工业界普遍使用非(半)形式化的表示定义与描述用户需求,如何由非(半)形式化的用户需求生成形式化软件规格说明是需求工程的难点之一.将设计模式的概念进行扩展,定义了问题模式... 精确的形式化软件规格说明是软件描述、开发与验证的基础,而工业界普遍使用非(半)形式化的表示定义与描述用户需求,如何由非(半)形式化的用户需求生成形式化软件规格说明是需求工程的难点之一.将设计模式的概念进行扩展,定义了问题模式,提出了一种基于问题模式形式化软件规格说明生成方法.该方法从结构化自然语言SNL描述的高层问题需求出发,通过选择知识库中的问题模式逐步精化得到各个新的子问题对应的形式化规格说明,之后对各个子问题组合并进行优化以得到最终的形式化规格说明.进一步,使用模型精化演算的原理与概念给出了该生成方法的理论基础.采用算法程序领域作为研究对象并使用Radl语言作为形式化规格说明语言.通过算法程序领域中的典型实例对这一方法进行了详细的描述,实际效果表明该方法能有效地生成高质量形式化规格说明. 展开更多
关键词 形式化软件规格说明 生成方法 问题模式 模型精化演算 算法程序
下载PDF
形式化软件功能分解的交互式规则 被引量:1
6
作者 李彤 王黎霞 +1 位作者 柳青 孔兵 《计算机工程与应用》 CSCD 北大核心 2000年第7期44-46,共3页
形式化功能分解是软件形式化设计的基本手段。文章基于前后断言形式定义的软件功能,提出了一组将该功能定义分解为3种基本控制结构之一的交互式分解规则,并证明了这组分解规则的正确性。分解规则构成的规则库是支持软件形式化设计的... 形式化功能分解是软件形式化设计的基本手段。文章基于前后断言形式定义的软件功能,提出了一组将该功能定义分解为3种基本控制结构之一的交互式分解规则,并证明了这组分解规则的正确性。分解规则构成的规则库是支持软件形式化设计的知识库的重要组成部分。 展开更多
关键词 功能分解 面向对象 交互式规则 形式化软件
下载PDF
基于Event-B和Rodin开展形式化软件工程教学 被引量:1
7
作者 李梦君 《计算机工程与科学》 CSCD 北大核心 2016年第A01期143-145,共3页
形式化软件工程是软件工程的重要组成部分。Event-B方法是一种软件形式化开发方法,Rodin是支持Event-B方法的开放工具集。基于Event-B方法和Rodin开展形式化软件工程教学,有益于学生正确理解精化等重要的软件工程概念,理解并掌握开发可... 形式化软件工程是软件工程的重要组成部分。Event-B方法是一种软件形式化开发方法,Rodin是支持Event-B方法的开放工具集。基于Event-B方法和Rodin开展形式化软件工程教学,有益于学生正确理解精化等重要的软件工程概念,理解并掌握开发可信软件的方法,是软件工程教学的重要补充。 展开更多
关键词 形式化软件工程 Event—B方法 Rodin
下载PDF
交互式环境下基于知识的形式化软件设计技术
8
作者 李彤 柳青 +1 位作者 孔兵 王黎霞 《计算机工程》 CAS CSCD 北大核心 2000年第4期41-43,共3页
提出了一种将前后断言形式定义的非过程化的软件功能转换为过程化算法描述的技术。在由范例库、基元库和规则库构成的知识库支持下,交互式地不断分解细化软件功能,直至所有的功能定义都能由基元库中的语义子程序转换为算法性的目标代... 提出了一种将前后断言形式定义的非过程化的软件功能转换为过程化算法描述的技术。在由范例库、基元库和规则库构成的知识库支持下,交互式地不断分解细化软件功能,直至所有的功能定义都能由基元库中的语义子程序转换为算法性的目标代码为止。设计过程由分解树来描述。 展开更多
关键词 交互式环境 知识库 形式化软件设计 分解树
下载PDF
软件工程中的形式化方法研究综述 被引量:3
9
作者 李婉璐 《数字技术与应用》 2015年第10期108-109,共2页
软件工程中的形式化方法是以数学理论为基础,建立的一种用来解决软件工程领域问题的系统性分析方法。形式化方法通过具有明确语义的形式语言来描述目标软件系统的行为和特征,为目标系统开发提供了一个模型化的有效设计和分析途径,保障... 软件工程中的形式化方法是以数学理论为基础,建立的一种用来解决软件工程领域问题的系统性分析方法。形式化方法通过具有明确语义的形式语言来描述目标软件系统的行为和特征,为目标系统开发提供了一个模型化的有效设计和分析途径,保障了系统的安全性和可靠性。本文简单介绍了形式化方法的研究内容及分类,在软件方法学的研究背景下,对形式化方法在软件系统开发每一个阶段的应用进行了详细分析和综合评价。 展开更多
关键词 形式化方法 软件方法学 形式化软件开发
下载PDF
面向程序可达性验证的数组处理循环压缩方法
10
作者 许良晨 孟昭逸 +1 位作者 黄文超 熊焰 《信息网络安全》 CSCD 北大核心 2024年第3期374-384,共11页
计算机软件的安全性和健壮性逐渐成为一个非常重要的问题,而自动软件形式化验证是一种验证软件程序安全性和健壮性的可靠性较高的方法。在自动软件形式化验证中,大规模数组和复杂循环导致状态爆炸,使得验证器无法在规定时间内完成验证,... 计算机软件的安全性和健壮性逐渐成为一个非常重要的问题,而自动软件形式化验证是一种验证软件程序安全性和健壮性的可靠性较高的方法。在自动软件形式化验证中,大规模数组和复杂循环导致状态爆炸,使得验证器无法在规定时间内完成验证,因此如何在保证验证正确性的前提下压缩数组规模是一个值得研究的课题。文章提出复杂循环等价类的定义和相关命题,并提出一种面向程序可达性验证的数组处理循环压缩方法,先利用控制流自动机和系统依赖图进行静态分析划分等价类,再根据循环依赖关系对等价类进行压缩,用压缩后程序的验证结果代替原始程序的验证结果。实验结果表明,文章提出的方法能够在保证验证正确性的前提下压缩程序的规模,提高验证效率。 展开更多
关键词 等价类分析 软件形式化验证 静态分析 系统依赖图
下载PDF
第16届软件工程国际会议综述
11
作者 郑国梁 陈钟 《国际学术动态》 1995年第1期49-53,共5页
关键词 软件工程 软件形式化 软件体系结构
下载PDF
软件演化过程建模中的开发人员度量方法
12
作者 陈展 《计算机工程与设计》 CSCD 北大核心 2007年第21期5305-5307,共3页
提出了一种在构建形式化的软件演化过程模型(formal software evolution process model,FSEPM)中使用X-S图来度量开发人员的统计控制方法。开发人员是构建模型的核心角色,度量其相关属性可以透析和严格管理开发过程。通过一个实例说明... 提出了一种在构建形式化的软件演化过程模型(formal software evolution process model,FSEPM)中使用X-S图来度量开发人员的统计控制方法。开发人员是构建模型的核心角色,度量其相关属性可以透析和严格管理开发过程。通过一个实例说明如何度量处在构建过程中的开发人员,利用度量结果来分析开发过程的稳定性、找出可归属原因、进行预测和估计、并为整个开发过程的演化奠定基础。 展开更多
关键词 形式化软件演化过程模型 度量开发人员 X-S图 稳定性 开发过程的演化
下载PDF
基于信息约束的数据库查询界面的自动生成
13
作者 卢雷 万建成 《计算机工程》 CAS CSCD 北大核心 2002年第6期77-79,共3页
在分析了现有数据库用户查询界面和条件生成在数据库应用中存在的问题后,基于面向对象的概念,提出了可视对象数据描述表结构、信息来源和取值方式等约束的用户查询界面和条件的生成方法,并给予了形式化描述。查询条件的生成采用的是合... 在分析了现有数据库用户查询界面和条件生成在数据库应用中存在的问题后,基于面向对象的概念,提出了可视对象数据描述表结构、信息来源和取值方式等约束的用户查询界面和条件的生成方法,并给予了形式化描述。查询条件的生成采用的是合取范式的标准形式,用户界面的生成采用了标准的可视对象。该方法已经得到了实现,并在实际系统中获得了应用。 展开更多
关键词 信息约束 数据库查询界面 自动生成 图形用户界面 软件形式化方法
下载PDF
软件工程中的形式化方法研究概述
14
作者 熊小超 《汽车世界》 2020年第7期168-168,共1页
软件工程中的形式化方法是以数学理论为基础,建立的一种用来解决软件工程领域问题的系统性分析方法。形式化方法通过具有明确语义的形式语言来描述目标软件系统的行为和特征,为目标系统开发提供了一个模型化的有效设计和分析途径,保障... 软件工程中的形式化方法是以数学理论为基础,建立的一种用来解决软件工程领域问题的系统性分析方法。形式化方法通过具有明确语义的形式语言来描述目标软件系统的行为和特征,为目标系统开发提供了一个模型化的有效设计和分析途径,保障了系统的安全性和可靠性。本文简单介绍了形式化方法的研究内容及分类,在软件方法学的研究背景下,对形式化方法在软件系统开发每一个阶段的应用进行了详细分析和综合评价。 展开更多
关键词 形式化方法 软件方法学 形式化软件开发
下载PDF
SRLtoRadl生成系统及其范畴论语义 被引量:11
15
作者 王昌晶 薛锦云 左正康 《电子学报》 EI CAS CSCD 北大核心 2014年第1期137-143,共7页
形式化软件规约技术是保证软件质量和提高软件生产率非常有用和重要的手段,但是形式化软件规约的获取是需求工程中一项相当困难的任务.本文针对问题需求自动化转换为形式化规约这个重要问题,研究从结构化需求语言SRL到形式化规约语言Rad... 形式化软件规约技术是保证软件质量和提高软件生产率非常有用和重要的手段,但是形式化软件规约的获取是需求工程中一项相当困难的任务.本文针对问题需求自动化转换为形式化规约这个重要问题,研究从结构化需求语言SRL到形式化规约语言Radl自动生成系统及其高可靠性理论.为此,设计了一种受控自然语言-结构化需求语言SRL来描述问题需求;使用基于规则的方法,将结构化需求语言SRL通过分析-转换-综合三阶段生成为形式化软件规约Radl;在该方法的指导下,设计并实现了从结构化需求语言SRL到形式化软件规约Radl的生成系统SRLtoRadl;进一步,使用范畴论框架建立了SRLtoRadl生成系统生成过程的语义模型.实际效果表明该系统能有效的生成高质量形式化软件规约Radl. 展开更多
关键词 结构化需求语言 形式化软件规约 自动生成系统 高可靠 范畴论语义
下载PDF
Aspect-Oriented Design Method for Embedded Systems Based on Timed Statecharts
16
作者 文欣秀 虞慧群 郑红 《China Communications》 SCIE CSCD 2013年第9期33-42,共10页
The formal modelling and verification method has become an effective way of improving the reliability and correctness of complex,safety-critical embedded systems.Statecharts are widely used to formally model embedded ... The formal modelling and verification method has become an effective way of improving the reliability and correctness of complex,safety-critical embedded systems.Statecharts are widely used to formally model embedded applications,but they do not realise the reasonable separation of system concerns,which would result in code scattering and tangling.Aspect-Oriented Software Development(AOSD)technology could separate crosscutting concerns from core concerns and identify potential problems in the early phase of the software development life cycle.Therefore,the paper proposes aspect-oriented timed statecharts(extended timed statecharts with AOSD)to separately model base functional requirements and other requirements(e.g.,scheduling,error handling),thereby improving the modularity and development efficiency of embedded systems.Furthermore,the dynamic behaviours of embedded systems are simulated and analysed to determine whether the model satisfies certain properties(e.g.,liveness,safety)described by computation tree logic formulae.Finally,a given case demonstrates some desired properties processed with respect to the aspect-oriented timed statecharts model. 展开更多
关键词 embedded systems model check-ing timed statecharts computation tree logic
下载PDF
一种基于SEPM的过程片断效率度量和改进
17
作者 陈展 李彤 《云南大学学报(自然科学版)》 CAS CSCD 北大核心 2006年第S2期40-44,共5页
提出了一种支持形式化的软件演化过程模型的效率度量方法和改进策略.效率度量可以帮助我们了解模块的执行效率和并行度.对于一个从SEPM中被截取下来的过程片断,介绍了如何通过定制它的效率度量原则、方法、步骤来进行定量分析和评价,... 提出了一种支持形式化的软件演化过程模型的效率度量方法和改进策略.效率度量可以帮助我们了解模块的执行效率和并行度.对于一个从SEPM中被截取下来的过程片断,介绍了如何通过定制它的效率度量原则、方法、步骤来进行定量分析和评价,根据SEPM的特点制定改进策略,挖掘和拓延活动内和活动间的并行性,从而提高该过程片断的效率,使它有能力,为评价整个软件演化模型的效率奠定基础. 展开更多
关键词 形式化软件演化过程模型 过程片断 效率度量 改进策略 挖掘拓延并行性
原文传递
上一页 1 下一页 到第
使用帮助 返回顶部