虚拟机在计算机实践教学中的应用

针对目前计算机实践教学中存在的问题,提出了一种虚拟机技术的解决方法。该方法不仅充分有效地利用现有设备,而且对硬件及系统具有很好的安全性,并能够增加学生的实践动手机会。教学上更加灵活、方便地设计实践项目,从而提高实践教学的质量。     

基于场景行为的需求建模及质量特性检测

为在需求分析阶段验证软件是否满足非功能质量要求,本文提出一种基于场景行为的需求建模及质量特性检测方案。该方案首先定义能够建立高精度、可推理、易理解的需求行为模型的行为描述语言BDL。然后构造需求行为模型到状态迁移模型CCS的模型转换函数。接着以互模拟的定义为前提,验证转换函数的正确性,进而开发可信建模检测工具MTS。该工具导出的行为模型能够与质量特性表达式一起导入特性检测工具CWB实现质量检测。最后,本文使用该工具对手机软件升级这一需求进行行为建模,成功验证手机软件的一致性、安全性、行为可信性及行为非终止性。     

代码/需求行为差异检测

为解决软件开发后期（维护/演化）程序代码与需求模型不一致的问题,本文面向逆向需求工程,重点研究检测变更代码与原始需求模型之间行为差异的算法：首先沿用模型/代码转换技术,分析模型/代码比较原理,设计比早期连续型单向串行检测算法快2N倍（N为路径数）的离散型双向并行检测算法。然后采用该算法开发图形化需求/代码比较工具RCCT,并将其集成进综合需求建模系统（RMTS）,使动画建模、特性检测、模型转换、需求/代码差异检测等功能融为一体。最后,通过电子转账案例演示该工具的使用方法,并编写测试程序证明离散型双向并行算法不但比原始算法高效,而且更加可靠。     

序列折半划分问题的形式化推导

形式化推导是在程序正确性证明理论下所进行的程序开发,最终得到完全正确的算法程序。针对序列折半划分问题,现有的形式化推导方法将推导与证明交替进行,推导过程繁琐且大多无法直接获得可执行程序。为解决上述问题,提出了一种新的序列折半划分问题的形式化推导方法。该方法基于分划递推的核心思想,应用规约变换技术对问题规约进行变换并严格保证一致性,使得在推导过程中无需交替证明,进而导出递推关系式并得到高可靠性抽象算法程序Apla,最终通过转换工具自动生成可执行程序。实现了从程序规约到具体可执行程序的完整程序求精过程。以2个序列算法为例,验证了该方法的有效性和可行性,对相关问题的形式化推导具有指导意义。     

南宁市居住建筑能耗调查与综合能耗定额分析

为了更好地了解南宁市居住建筑夏季用能水平和能耗结构,本文采用单位综合能耗作为能耗评价指标,结合相关调研结果,应用统计分析方法进行计算分析,得出了南宁市居住建筑夏季的用能特征及其单位综合能耗定额范围,并用SPSS软件分析了该指标的适用性和意义。     

命令式动态规划类算法程序推导及机械化验证

动态规划是一种递归求解问题最优解的方法,主要通过求解子问题的解并组合这些解来求解原问题.由于其子问题之间存在大量依赖关系和约束条件,所以验证过程繁琐,尤其对命令式动态规划类算法程序正确性验证是一个难点.基于动态规划类算法Isabelle/HOL函数式建模与验证,通过证明命令式动态规划类算法程序与其的等价性,避免证明正确性时处理复杂的依赖关系和约束条件,提出命令式动态规划类算法程序设计框架及其机械化验证.首先,根据动态规划类算法的优化方法(备忘录方法)和性质(最优子结构性质和子问题重叠性质)描述问题规约、归纳递推关系式和形式化构造出循环不变式,并且基于递推关系式生成IMP (Minimalistic Imperative Programming Language)代码;其次,将问题规约、循环不变式和生成的IMP代码输入VCG (Verification Condition Generator),自动生成正确性的验证条件;然后,在Isabelle/HOL定理证明器中对验证条件进行机械化验证.算法首先设计为命令式动态规划类算法的一般形式,并进一步实例化得到具体算法.最后,例证了所提框架的有效性,为动态规划类算法的自动化推导和验证提供参考价值.     

基于模型驱动的分治并行函数式程序生成及自动验证

并行计算作为人工智能发展的动力,使得并行算法的可解释性和安全性成为人工智能领域重要研究方向。形式化方法以数理逻辑为基础,已经成为复杂安全苛求系统可信构建的重要方法,而函数式编程则在算法领域中具有更强的数学表达性。本文旨在提出一种基于模型驱动的分治并行函数式程序生成及自动验证方法,融合形式化方法,以解决目前分治并行程序生成和验证中缺乏可解释性、易错、低可信度等问题。首先,采用分划递推法和循环不变式等新策略推导出串行算法;然后,利用辅助函数和算法连接函数将其提升为并行算法,并使用我们提出的并行算法设计语言Radl⁺进行描述;进而,采用同态定理验证框架在Isabelle中验证算法连接函数满足同态定理,即提升后的算法可并行化;最后,提出了Radl⁺→Haskell转换规则,设计了“Radl⁺→Haskell并行程序生成系统”软件原型。实验结果表明,本文能够生成和验证一系列算法的并行函数式程序,并且能够产生良好的加速比。本文方法不仅具有一定的可解释性,而且自动验证减少了传统手工验证易错性和繁琐的工作量,保证算法正确性和提高安全性,对大幅度提升高可信并行函数式程序的开发效率具有重要意义。     

新闻纸的扫描电镜分析

利用扫描电镜观察新闻纸中纤维及填料的微观形态,结合图像数字化处理技术和分区随机取样法,确定纤维数平均值、填料数平均值、纤维数的变异系数和填料数的变异系数4个数据作为新闻纸的量化指标.建立了一种纸张的量化方法,并比较出不同新闻纸具有一定差异性.该方法有效,可靠和稳定,可为纸张进行同种类鉴别提供依据.     

夏热冬暖地区超高层办公楼大温差空调设计

南宁市位于夏热冬暖地区。本文以该市的一个城市综合体项目为例,重点介绍了其中的超高层办公楼的大温差空调系统设计。文章结合了对该项目的空调冷热源设计,空调水系统竖向分区,大温差小流量下风机盘管修正以及新风系统分区设计等的分析,探讨了超高层大温差空调设计需要关注的问题,提供了一些设计思路。     

基于现行规范的公共建筑内走道排烟设计探讨

我国国家标准《建筑防烟排烟系统技术标准》(GB51251-2017)已于2018年8月1日实施。本文针对高层公共建筑内走道排烟系统的设计,对比了相关的新、旧规范,结合国外相关规范对新规范的一些争议内容进行了分析。此外,还通过实例计算,对新规范应用中存在的一些问题进行了探讨。