检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

形式化方法在高中算法教学中的应用研究

计算机与现代化 2010年第7期 87-92页

作者：苏昭薛锦云杨晨江西师范大学省高性能计算技术重点实验室江西南昌330022

国家教育部制定的高中新课程标准将算法初步作为高中数学课程的必修内容,算法与程序设计也首次纳入到选修课之列。全国大部分普通高中均按新课标开展教学实验,不少省份还把算法内容纳入高考。同时现有算法初步和算法与程序设计教材在介... 详细信息

国家教育部制定的高中新课程标准将算法初步作为高中数学课程的必修内容,算法与程序设计也首次纳入到选修课之列。全国大部分普通高中均按新课标开展教学实验,不少省份还把算法内容纳入高考。同时现有算法初步和算法与程序设计教材在介绍算法与算法设计方法时,无法说清楚算法设计的过程;在教学实践中,这一问题更加突出。这给高中生学习、理解及掌握算法和算法设计方法带来很大的困难。本文从新课程实验教材中及数学高考题中选取两个问题,用支持算法程序形式化开发的PAR(Partition And Recur)方法与PAR平台,从待求解问题的精确功能描述出发,经过一系列等价数学变换,最后得到正确的算法和程序。实践说明PAR方法与PAR平台可以在高中算法教学及学生能力评测中发挥建设性作用。

关键词：可信软件形式化方法 PAR方法

多视图下的REST及SA-REST的形式化方法研究

在线全文

学校读者我要写书评

暂无评论

多视图下的REST及SA-REST的形式化方法研究

作者：唐翊婷华东师范大学

学位级别：硕士

REST架构自2000年由Fielding在其博士论文中提出后,近十数年得到了广泛的展,因此遵循REST架构风格的服务和应用的数量正以极快的速度在增加。但是Fielding指出目前有部分声称是RESTful的服务并不完全符合REST的约束,REST架构被误用一定... 详细信息

REST架构自2000年由Fielding在其博士论文中提出后,近十数年得到了广泛的展,因此遵循REST架构风格的服务和应用的数量正以极快的速度在增加。但是Fielding指出目前有部分声称是RESTful的服务并不完全符合REST的约束,REST架构被误用一定程度上是因为缺少对其的形式化研究。本文用形式化的方法,并将REST架构从三个视图：过程、连接器、数据分别进行建模和分析,三个视图分别对应REST的三种架构元素：组件、连接器、数据。利用多视图不仅能够给出更精确更完整的架构描述,还提高了模型的可读性及可扩展性。本文的模型在PAT中实现并验证了REST六条基本约束,且利用多视图的优势,着重分析验证了REST无状态性与应用状态及资源状态之间的关系、统一接口与统一方法之间的区别,以及超媒体驱动等性质。随着语义网的发展,REST结合语义后出现了SA-REST。通过给REST添加语义注释的方法,如添加RDF (Resource Description Framework)三元组,可以得到能够被机器理解和调用的SA-REST。在Mashup中利用SA-REST,可以使Mashup的性能和智能化得到大幅提升,称其为SMashup。本文介绍了SA-REST,并且用形式化方法研究了SMashup。通过用CSP语言建模和PAT工具实现验证,主要分析了SMashup中服务链的特性、服务糅合过程中的数据仲裁过程、添加语义后输入输出流的性质等。

关键词：形式化方法软件架构架构视图 REST SA-REST Mashup

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

可生存性网络的形式化建模与分析方法

通信学报 2006年第z1期27卷 48-52页

作者：赵国生王慧强李明军哈尔滨工程大学计算机学院黑龙江哈尔滨150001 哈尔滨工程大学计算机学院黑龙江哈尔滨150001 哈尔滨师范大学网络中心黑龙江哈尔滨150080

首次提出一种基于随机进程代数的网络可生存性形式化建模方法,该方法把形式化建模与性能分析相结合,从而可以在形式化建模同时分析得到系统的各种生存性能参数.在简单介绍随机进程代数的语法和操作语义的基础上,用进程表达式对生存性系... 详细信息

首次提出一种基于随机进程代数的网络可生存性形式化建模方法,该方法把形式化建模与性能分析相结合,从而可以在形式化建模同时分析得到系统的各种生存性能参数.在简单介绍随机进程代数的语法和操作语义的基础上,用进程表达式对生存性系统进行形式化描述;然后利用PEPA Workbench工具实现对可生存性网络稳态可用性和瞬时可用性测度的实验,仿真结果验证了该形式化建模与分析方法的有效性和可行性.

关键词：形式化方法随机进程代数可生存性网络性能分析

基于Event-B的软件工程形式化方法综述

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

计算机系统应用 2021年第9期30卷 12-23页

作者：彭寒张晓丽刘洲洲曹国震景月娟王瑾李添锐西安航空学院计算机学院西安710077 西安石油大学计算机学院西安710065

在当今泛在计算和软件定义的大趋势下,形式化方法逐步成为指导软件需求定义、分析软件设计方案、验证软件制品正确性的重要方法,渗透到软件工程的全寿命周期. Event-B作为一种"构造即正确"的方法,为软件工程形式化方法的应用提供了支撑... 详细信息

在当今泛在计算和软件定义的大趋势下,形式化方法逐步成为指导软件需求定义、分析软件设计方案、验证软件制品正确性的重要方法,渗透到软件工程的全寿命周期. Event-B作为一种"构造即正确"的方法,为软件工程形式化方法的应用提供了支撑.本文对现有的基于Event-B的软件工程形式化方法进行了分类阐述,主要分为Event-B控制结构、面向对象的Event-B、可重用的Event-B以及实时Event-B模型,并对各种Event-B模型对软件开发全寿命周期的支持进行了汇总,为软件工程形式化方法提供参考和借鉴.

关键词：软件工程形式化方法面向对象可重用形式化模型

一种面向UEFI模块的形式化建模与验证方法

在线全文

学校读者我要写书评

暂无评论

计算机技术与发展 2021年第12期31卷 116-121页

作者：王冠郝晓星北京工业大学信息学部北京100124 北京市可信计算重点实验室北京100124

固件作为一种固化在ROM中的特殊软件程序,主要负责加电自检,硬件设备初始化,引导操作系统等基础功能,运行级别和安全等级较高,亟需一种高效、可靠的UEFI模块安全检测方法。采用形式化方法对UEFI模块进行规约与验证,对于提高固件的安全... 详细信息

固件作为一种固化在ROM中的特殊软件程序,主要负责加电自检,硬件设备初始化,引导操作系统等基础功能,运行级别和安全等级较高,亟需一种高效、可靠的UEFI模块安全检测方法。采用形式化方法对UEFI模块进行规约与验证,对于提高固件的安全性具有重要意义。基于现有的有限状态自动机和下推自动机基础,分别对UEFI模块中的安全漏洞属性和UEFI模块程序控制流进行形式化建模,利用模型检验对上述模型进行形式化验证。其中利用数据抽象思想将UEFI模块抽象为程序控制流且压缩其状态规模来缓解模型检验时的状态爆炸问题,并给出了相关模型的定义以及模型间转换、组合的算法。实验结果表明,对UEFI模块的抽象及压缩能够很好地缓解模型检验中的状态爆炸问题,并且该形式化验证方法能够实现对UEFI模块安全漏洞的自动化验证,且能够达到较低的漏报率。

关键词： UEFI 形式化方法模型检验安全漏洞有限状态自动机下推自动机

算法形式化方法在三类组合数学问题求解中的应用研究

在线全文

学校读者我要写书评

暂无评论

算法形式化方法在三类组合数学问题求解中的应用研究

作者：游颖江西师范大学

学位级别：硕士

算法设计是计算机科学研究的重要领域之一。目前计算机科学处理的大部分数据都是离散的数据,而组合数学是研究离散数据的科学,因此研究以组合数学为基础的算法的可靠性、正确性和生产效率就成为算法设计领域中的关键问题。对于求解组合... 详细信息

算法设计是计算机科学研究的重要领域之一。目前计算机科学处理的大部分数据都是离散的数据,而组合数学是研究离散数据的科学,因此研究以组合数学为基础的算法的可靠性、正确性和生产效率就成为算法设计领域中的关键问题。对于求解组合数学相关的问题,目前存在多种算法设计方法,形式化开发方法是其中之一。形式化方法的本质是基于数学的方法来描述、开发和验证目标软件系统的一种技术,使用形式化方法开发算法程序能有效提高算法程序设计的规范化、自动化程度以及算法的可靠性和正确性。基于递推技术的算法形式化方法在部分形式化或者是完全形式化描述问题程序规约的基础上,通过对问题的程序规约进行数学变换,得到问题求解的递推关系,在此基础上得到最终的算法程序。由于求解问题的递推关系建立在严格数学变换的基础上,因而递推关系的正确性得到了保证,从而也有效确保最终的算法程序的正确性;另外,使用该方法开发算法程序,均是以寻找问题求解序列的递推关系为出发点,先得到较小的子问题的解,再在之前已获得的较小子问题解的基础上直接或间接得到较大问题的解,这样可以避免很多不必要的重复计算,从而有效提高算法程序的效率,并为算法程序的开发提供一条较为统一的途径。本文重点研究了基于递推关系的算法形式化方法在三类典型组合数学问题求解中的应用。本文分析了当前形式化开发方法的需求以及发展状况;介绍了基于递推技术的形式化开发方法的开发语言、开发步骤以及关键技术等,同时研究了它在组合数学问题开发上的有效性;接着,本文针对组合数学问题进行分类研究,使用基于递推技术的形式化方法开发了三类有代表性的组合数学问题:整除问题、排列组合问题以及NP完全问题中的0-1背包变形问题,同时在分析每一类问题形式化开发过程共性的基础上提炼得到了求解该类问题的统一策略,并将其推广到相似问题的求解;最后对基于递推关系的形式化开发方法在组合数学上的应用进行了总结。研究表明,基于递推技术的算法形式化开发方法有效保证了算法程序的正确性,提高了算法程序的执行效率。

关键词：形式化方法递推技术组合数学算法设计

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

形式化方法对构件库管理系统支持的探讨

电子技术应用 2006年第4期32卷 18-21页

作者：边小凡朱建林王倩河北大学数学与计算机学院河北保定071002 华北电力大学就业指导服务中心河北保定071003

依据网上信息收集系统构件库中构件的开发和管理经验,提出一种构件模型。

关键词：构件模型构件库形式化方法形式化描述

基于B方法的在线考试软件需求规格形式化方法的研究

在线全文

学校读者我要写书评

暂无评论

基于B方法的在线考试软件需求规格形式化方法的研究

作者：王可心东北师范大学

学位级别：硕士

随着网络技术的发展,在线考试软件正成为人们的研究热点。由于目前在线考试软件的开发人员,通常采用传统的非形式化或半形式化开发方法作为软件需求的描述段.而在线考试系统是一种基于业务流程的实时性软件,传统的非形式化或半形式化方... 详细信息

随着网络技术的发展,在线考试软件正成为人们的研究热点。由于目前在线考试软件的开发人员,通常采用传统的非形式化或半形式化开发方法作为软件需求的描述段.而在线考试系统是一种基于业务流程的实时性软件,传统的非形式化或半形式化方法中基于状态转换的表达并不完整,缺少精确语义信息,缺乏有效的推理机制,所以不足以确保在线考试软件在需求分析阶段的一致性和完整性。UML模型包括用例图与用例规约,因此直观、简洁。但UML缺乏精确的语义,会引起二义性;UML同时又不具备好的推理及模型检测机制。本文选择了B方法作为形式规约的方法,一方面是因为形式化B方法是以严格的数学理论为基础;另一方面是因为它贯穿程序设计的全过程。选择B方法进行规约描述,能避免二义性,保证一致性。有助于开发人员对系统的理解,减少后期维护的压力。本文主要研究对象为在线考试软件、用例模型和B方法。分析用例模型的构成元素,与B方法之间的关系。建立了用例模型与B方法之间的映射,将其应用在在线考试软件。实现了需求规格的形式化说明,解决了在线考试系统存在大问题。最后,对考生在线考试过程进行需求分析,建立用例模型。用定义的映射规则对用例模型进行描述,并用工具验证其正确性。

关键词：形式化方法 B方法在线考试软件 UML 用例模型

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

形式化方法在软件开发中的应用

计算机光盘软件与应用 2014年第12期17卷 269-270页

作者：曹斌刘栓黄淮学院信息工程学院河南驻马店463000

形式化方法是把概念、判断、推理转化成特定的形式符号后,对形式符号表达系统进行研究的方法。是用具有精确语义的形式语言书写的程序功能描述,它是设计和编制程序的出发点,也是验证程序是否正确的依据。形式化方法就是用符号化的数学... 详细信息

形式化方法是把概念、判断、推理转化成特定的形式符号后,对形式符号表达系统进行研究的方法。是用具有精确语义的形式语言书写的程序功能描述,它是设计和编制程序的出发点,也是验证程序是否正确的依据。形式化方法就是用符号化的数学变换把需求分析给准确的表述出来,这样可以确保和需求的一致性,并能用于分析和验证应用程序。

关键词：形式化方法软件开发