【摘 要】
：
需求分析在软件工程中处于非常重要的地位,为设计起指导作用,是软件工程中的一个关键过程,需求分析的正确性直接关系到所开发系统的效率和质量。目前需求工程也已经研究出一系列需求分析的方法,金芝等提出的基于环境建模的需求工程方法（EBRE）被广泛应用,该方法显式地对交互环境进行建模,并基于环境模型为需求获取和分析提供系统的过程和需求模型。如何验证EBRE需求模型的正确性是备受关注的问题之一,目前存在相应工
论文部分内容阅读
需求分析在软件工程中处于非常重要的地位,为设计起指导作用,是软件工程中的一个关键过程,需求分析的正确性直接关系到所开发系统的效率和质量。目前需求工程也已经研究出一系列需求分析的方法,金芝等提出的基于环境建模的需求工程方法（EBRE）被广泛应用,该方法显式地对交互环境进行建模,并基于环境模型为需求获取和分析提供系统的过程和需求模型。如何验证EBRE需求模型的正确性是备受关注的问题之一,目前存在相应工具以环境本体为标准验证EBRE模型的完整性等,但对于需求模型自身的正确性仍缺少形式化证明手段,导致需求模型的正确性在数学逻辑证明层面无法得到保障。Event-B作为一种典型的形式化方法,其基于集合论和一阶逻辑,以精化的方式进行形式化建模与验证,并根据系统需求验证其正确性,可以作为EBRE需求模型正确性验证的一种途径。我们将EBRE方法和Event-B的方法结合起来,提出基于Event-B的EBRE需求模型的正确性验证方法。将EBRE模型转换为Event-B的初始模型,转换过来的Event-B模型可以为需求模型的正确性提供形式化证明。在此基础上,我们实现了EBRE模型到Event-B模型的自动化转换工具,并以Rodin插件的形式发布,从而实现EBRE需求模型的正确性的自动化验证。本文的主要工作如下:1.EBRE需求模型到Event-B模型的转换:通过分析EBRE模型元素与Event-B模型元素之间的对应关系,定义了一套转换规则,将EBRE需求模型转换为Event-B模型,确保EBRE需求模型与转换后的Event-B模型具有语义上的一致性。2.EBRE需求模型的正确性验证:转换后的Event-B模型会生成相应的证明义务,基于Rodin平台的定理证明机制,进行证明义务的自动证明或手动交互式证明,从而验证需求模型的正确性。通过分析证明义务与EBRE需求模型中所要满足的性质的一一对应关系,将Event-B的验证机制应用于EBRE模型的正确性验证,验证需求的正确性。3.基于Rodin平台的模型自动化转换插件:基于EBRE需求模型到Event-B模型的转换以及EBRE需求模型的正确性验证的方法,实现EBRE需求模型元素到Event-B模型元素的自动化转换工具,为EBRE需求模型的正确性验证提供技术支撑。
其他文献
随着循环神经网络（Recurrent Neural Network,RNN）的应用更加广泛,对抗序列的存在给这类安全攸关应用构成了极大的威胁,其中包含自动驾驶行为预测模型。RNN对抗序列生成是一种提升RNN鲁棒性的方法,然而目前现有的RNN对抗序列生成方法普遍存在着低效的问题。因此,针对上述问题,围绕自动驾驶行为预测模型,提出了一种基于权重自动机（Weighted Finite Automaton
气象条件是人民日常生活和农业生产的重要影响因素,随着各类气象灾害的频繁出现,人民群众的生命财产安全受到了严重威胁。因此,气象监测和预测变得越来越重要。随着传感器技术和通信技术的进一步发展,气象监测从人工记录数据逐步转为自动化记录和管理数据。气象数据的准确监测是开展气象工作的基础,也是准确预测各种突发性灾害天气的依据。目前市场上的气象监测系统,往往存在网络化能力不高、自动化能力欠缺以及设备部署复杂等
序列推荐（Sequential Recommendation）根据用户的历史交互序列预测用户的下一次交互物品,由于序列中复杂的物品依赖以及用户的多方面兴趣,想要准确预测用户的下一次交互的物品十分困难。现有的工作将序列中的每一个交互物品视作一个兴趣单元,并应用了最新的深度学习技术来学习到用户兴趣的统一表示。虽然这些方法在实验中取得了较好的效果,但它们仍存在一些缺陷:1)一个向量不足以表示用户多方面的
呼吸状态可以反映一个人的生理和心理状况,有助于相关疾病的筛查诊断和预后评估。本文对非接触式呼吸状态评估方法展开研究。具体来说,利用视觉传感器进行呼吸信号提取,结合多种信号处理技术对原始信号进行处理,借助机器学习技术对呼吸状态进行分类,并以此为研究框架,搭建了两套非接触式呼吸监控设备,深度研究人体向前走动时识别深呼吸的方法。主要研究内容及创新如下:（1）搭建基于彩色相机和标志物追踪的呼吸监控系统,结
在大数据时代,数据已成为比肩石油的基础性关键战略资源,正在颠覆全球社会的发展模式。数据流通是释放数据价值的关键环节,数据交易系统的建立是促进数据流通的重要举措。数据交易系统帮助卖方数据流入买方,增加数据的流动性,帮助释放数据价值。随着《数据安全法》等相关文件的发布,全社会对于数据安全和数据隐私的需求越来越高,对传统的数据交易系统提出了保护数据隐私等新要求。目前的数据交易系统存在三个问题:1.二次转
以图结构表示的数据广泛存在于各类应用场景,大规模图分析挖掘需要利用分布式图处理系统。图处理算法一般都是迭代的,且执行时间长。在此过程中,系统中节点出现故障是常见的现象。通常,分布式图处理系统利用检查点来处理故障。在正常执行期间,系统需要周期性地写入检查点。特别地,在写入检查点时,一些系统会暂停计算过程,即阻塞式写检查点。显然,这种阻塞式写检查点方法带来了额外的运行时开销。与此不同,非阻塞式写检查点
近年来,越来越多的计算机视觉系统被广泛地应用于人们生活中的方方面面,从日常生活到国家安全,计算机视觉系统起着重要的作用。这些视觉系统往往会受到部署环境的影响。雾是一种常见的恶劣天气,大量颗粒悬浮在大气中,导致视觉系统捕获的图像严重受损,出现部分信息丢失、纹理细节模糊、颜色失真等问题,这些问题会直接损害视觉系统的性能。因此,如何快速有效地对雾天降质图像进行复原,提升图像质量,消除雾霾天气对视觉系统的
在乡村振兴及美丽乡村建设的不断推进下,农村环境治理的发展现状落后于农业农村现代化发展的步伐,早已不能满足时代发展的新需求。“十三五”时期是我国农村环境保护的攻坚期,崇明在“世界级生态岛”战略目标的推动下,新建1.7万余座农村生活污水处理设施;但在长期运行过程中,大部分处理设施出水总氮、氨氮、总磷不达标,出水C/N较低,可生化性较差。本文通过实地调研,收集、计算、分析崇明农村户均人口、排放系数、处理
在大数据时代,随着电子商务交易和即时通讯平台的快速发展,网络上的短文本数据日益增长。所以,从这些数量巨大的短文本数据中提取出宝贵的知识是十分有必要的。短文本分类是自然语言处理领域的一个经典问题,它基于篇幅较短的文本数据学习其深层语义表征,同时用于分类任务。此类文本的长度通常较短,包含的有效信息较少且文本的口语化严重,具有极强的不规范性。所以,本文针对短文本特征稀少以及不规范的特点,从扩充短文本篇幅
自从进入互联网时代,如何保护信息安全就成为一种常态性的话题。密码在信息安全保护中尤为重要,网络数据的传输、数据库密码保护等都是通过密码算法来保护,一个好的密码算法能极大程度地保护我们想要保护的信息。密码算法主要可以分为对称密码和非对称密码,我们在选择密码时要考虑不同的情境,来决定是选择非对称密码还是对称密码。例如对加密解密的效率要求是否比较高,加密和解密密钥是否相同等。另外,选择密码时衡量效率和安