一、所属领域
计算机科学与技术
二、技术或产品名称
国产操作系统应用软件形式化设计方法
三、技术水平
本成果的核心技术处于同类研究的国内领先水平。
四、技术简介
为了满足国家在信息产业领域中的核心战略需求和发展我国航天领域自主可控和安全可信的操作系统及局域应用软件，推广和使用国产操作系统已经迫在眉睫。然而在国产操作系统的推广和使用方面，一直存在着系统兼容性差、相关应用软件产业链不完善、缺乏技术体系和软件工程方法等问题。
本成果以计算机科学与技术为主要领域，以软件工程和理论为研究方向，涉及了国产操作系统、应用软件开发、方法论设计框架、信息组织、数据处理、可视化技术等方面，属于应用基础研究。立足于软件工程环节的形式化描述方法，研究局域应用软件设计和开发过程子过程及其工具，建立了支撑i18n、l10n、g11n、m17n的技术规范，促进国产操作系统的推广和使用。重点研究了可视化Z形式描述方法，采用软件工程中的Z-理论和规范对软件产品设计和生产、过程管理、测试等问题进行抽象和规范描述，力求为安全可信的软件设计提供技术保障。本成果作为一种在国产操作系统上使用形式化描述的方式构建应用软件的方法，对软件系统的设计和生产、过程管理、测试等问题进行抽象和规范描述，为安全可信的航天测控软件设计提供技术保障，同时还解决了航天工程任务中软件系统国际化的问题。
本成果已成功应用于探月工程遥操作操控三维可视化平台，并于2013年在北京航天飞行控制中心参加并圆满完成了探月工程二期嫦娥三号落月探测任务的飞行控制与指挥的实时三维可视化，圆满地向世界展示了我国探月工程的成就，具有显著的社会效益和广泛的应用前景。
五、创新点及性能指标
本成果的主要创新点如下：
1、提出基于Z语言的软件全生命周期形式化描述方法，研发了Z规格说明自动生成器，对软件产品设计和生产、过程管理、测试等问题进行抽象和规范描述，有助于保障软件产品质量与实施进度。
2、将复杂网络理论引入国产操作系统的推广方面，建立基于应用软件格式的小世界网络模型，解决既有操作系统下的应用软件的迁移问题，有助于促进国产操作系统的推广应用。
六、知识产权情况
1. 软件著作权，2016SR134675，Z规格说明自动生成器软件
2. 软件著作权，2013SR066446，函数调用网络复杂性分析软件
3. 软件著作权，2016SR206690，基于国产操作系统的多源统计数据融合可视化系统
七、合作方式
技术服务、合作开发
八、投资概算及经济效益分析
项目总投资额为50万元。
效益分析：本成果立足于软件工程环节的形式化描述方法，采用软件工程中的Z-理论和规范对软件产品设计和生产、过程管理、测试等问题进行抽象和规范描述，力求为安全可信的软件设计提供技术保障；针对提升国产局域应用软件产品的全球化竞争能力，包括支撑i18n、l10n、g11n、m17n的技术规范和局域应用软件的开发平台及配套的软件工程开发工具，缩小各种局域应用软件产业链在区域、文化、语言、制度、习俗等方面的功能差异；助推国产操作系统的进化与完善，形成具有自主知识产权的软件生产过程中的工程规范和技术体系。
九、负责人
负责人：赵正旭
十、技术或产品的关键词
软件工程、形式化描述、Z语言
软件著作权-Z规格说明自动生成器软件
软件著作权-函数调用网络复杂性分析软件
软件著作权-基于国产操作系统的多源统计数据融合可视化系统
