图像语义分割标注软件的设计与实现

数据标注是人工智能的基础,是机器学习得以训练的不可或缺的步骤。现有的数据标注软件并不能满足用户个性化的标注需求,因此,本文设计并实现了图像语义分割标注软件。该软件适用于任意场景图像的语义分割标注,可以有效提高标注员和审核员的工作效率,具有一定的推广应用价值。

Z规格说明自动生成器

形式化Z语言采用严格的数学理论可以有效提高软件的可靠性和鲁棒性,但是由于其包含的数学理论使得只有少数人能够熟练应用Z语言进行形式化规格说明书的编写.目前,多数对于Z语言的研究集中在理论阶段,还没有相应的工具支持Z规格说明的自动生成.本文中对于Z规格说明自动生成器的研究有助于降低Z规格说明书的编写难度,降低了形式化开发的难度及成本,对于形式化Z语言的推广具有重要的意义.

OpenGL图形规范的Z形式化描述

OpenGL图形系统的开发难度随着OpenGL应用的不断发展和深入而日益增大,潜在的错误也越来越多,其中不能准确理解OpenGL规范是重要原因之一。由于OpenGL规范的描述主要是以自然语言为主,而且规范繁多,使用形式化描述规范可增加规范的准确性。本文选择描述OpenGL光照规范。通过列举光照的实例,利用Z语言给出了OpenGL中光照的规格说明,为规范的一致性测试提供了依据。

军民融合战略下信息系统的可信度净评估研究

本文通过对军民融合战略分析,指出在技术层面缺乏准入与准出机制评估,所以,评估系统是否可信是军民融合必须面临的问题。本文以信息系统为研究对象,指出目前信息系统存在着巨大的信任危机。随后,结合"净评估"理论,说明了新形势下针对信息系统进行可信度评估的必要性以及基本方法。

Z规格说明的推理与验证

Z规格说明具有非形式规约不可比拟的严谨性、清晰性。这种描述对于系统内对象的状态描述、行为描述是非常有用的原始参照物。但是,形式化描述不可避免的可能会含有错误或者是矛盾,这些问题在后期必定会导致前期的形式化设计不能付诸实践。因此,有必要做一些形式化的推理与验证来确保Z规约的实施。形式化推理是基于Z规格说明对一个操作模式求其前置条件,即求一个操作成功执行的必要条件,然后对比客观条件是否满足必要条件;形式化验证是一个操作模式求其后置条件,从集合的角度出发验证一个操作成功执行之后所导致的状态量变化是否与操作模式描述一致。

射电望远镜馈源舱数字化模型的创建

FAST是中国科学家自主设计与实现的口径最大、最具威力的巨型射电望远镜,将为未来天文学的发展、未知星体的发现提供丰富的研究资源。FAST的结构复杂多样,对FAST的结构与工作原理进行简单的介绍,对FAST中的馈源舱、停靠平台的工作原理与结构进行详细描述,并基于中标麒麟操作系统,采用跨平台,根据这两部分的图纸,对这两部分进行模型的创建,管理者可根据馈源舱、停靠平台的模型来了解其结构,将有助于对这两部分的工作机制进行模拟、维护或改进。

大型钢结构的快速建模方法

虚拟仿真在大型钢结构的吊装安装以及科普展示中已成为一种趋势,建模是虚拟仿真的关键技术之一。基于3dsMax和AutoCAD,提出一种快速建模方法,提高建模效率。首先利用已有的测绘信息,以钢结构中的每一个节点作为建模的基础数据;然后利用AutoCAD在处理批量坐标点方面的优势,将离散的坐标点连接成线;最后在3ds Max中将线生成面。并成功将该方法应用于我国"五百米口径球面射电望远镜FAST(中国天眼)"的建模工程,验证方法的有效性。

探月工程遥操作系统的移植研究与实现

近年来,"棱镜门事件"、"XP停服"等网络安全事件频发,各国深感信息安全面临巨大威胁,国外操作系统的安全性遭到质疑。为落实信息安全自主可控战略,推动航天领域信息安全建设,文章结合中标麒麟系统,利用Qt技术,完成了探月工程遥操作系统国产化迁移。实验结果表明,所使用的移植方案是可行的,可为航天领域其他信息系统的移植提供可行的现实依据,有助于航天领域科技成果知识产权的保护。