互联网内容分级服务技术标准体系的形式化设计与验证

摘要

互联网内容分级服务正得到政府部门和研究机构的关注和重视，内容分级产品的开发和市场应用也日渐增长，但已有的产品各自采用私有解决方案，相互间无法互联互通，不利于互联网内容分级服务技术的产业化和大规模推广应用。开发统一、完备和相容的内容分级服务技术标准体系是解决该问题的有效技术手段。
　　互联网内容分级服务是由许多功能服务主体所构成的大型分布式系统，在相关业务目标实现过程中，这些构成主体间将表现出复杂的、并发的协同交互行为。为确保系统功能正确实现，必须对所有构成主体的功能及其交互行为进行严格规范。现有技术标准体系主要采用工程经验方法来实现上述任务，其完备性和一致性没有得到充分验证。因此，运用形式化方法来完成相关技术标准体系的建模、设计和验证是必要的，并能为后续的各组成技术标准详细设计和系统开发提供坚实的理论基础。
　　为此，本论文主要从以下四个方面对互联网内容分级服务技术标准体系进行了研究:(1)业务环境形式化目标建模和系统目标提取;(2)系统内部构成主体及其协同交互目标提取和形式化描述;(3)各组成技术标准及其相互关系的提取和形式化描述;(4)技术标准体系形式化验证和能力比较。
　　本论文取得了以下四项成果:
　　(1)构建了业务环境的形式化目标模型
　　分析并提取各项核心业务目标，给出这些目标的形式化描述;对这些目标进行逐层精化，推得完整的业务环境形式化目标模型;从该模型提取出各项系统目标、环境假设和领域属性，并给出它们的形式化描述。该建模策略从理论上可确保，在各项环境假设和领域属性都被满足的前提下，只要正确实现各项系统目标，各项核心业务目标就确定会实现。
　　(2)构建了技术标准体系的形式化目标模型
　　采用目标中介状态提取和形式化目标精化技术，对各项系统目标进行逐层精化，得到完整的技术标准体系形式化目标模型;基于该模型中的叶目标及其承载主体，推得系统内部构成主体及其形式规约，由此确定对应的功能服务类技术标准;同时基于该模型的所有分支目标，推得相关构成主体问的交互行为形式规约，由此确定对应的协同交互类技术标准;最后，基于该模型中的目标精化关系，推得这些技术标准间的贡献关系。
　　(3)完成了技术标准体系的形式化设计
　　对每个功能服务类和协同交互类技术标准，给出了包括形式规约在内的完整描述;从这些技术标准形式规约中提取信息实体变量，由此确定对应的信息表示类技术标准，并给出包括信息实体属性说明在内的完整描述;由技术标准形式规约与信息实体变量的包含关系，推得信息表示类技术标准对其他类型技术标准的贡献关系;基于技术标准间的贡献关系，得到技术标准体系层次结构，并对其进行了完整描述。
　　(4)严格证明了技术标准体系设计的完备性和一致性
　　运用形式推理方法，对本技术标准体系的完备性和一致性给予了严格证明，为后续技术标准体系详细设计提供了坚实基础。同时，归纳并提炼出内容分级服务的各项基础能力，对每项能力分别给出标准支持与标准缺失的形式化描述，并由此得到本技术标准体系和其他已有技术标准体系在基础能力支持抽象层次上的形式化描述，最终推得它们在核心业务目标支撑能力方面的完整评价结果，结果表明，本技术标准体系相对其他已有技术标准体系，能对互联网内容分级服务各项业务目标提供更完整的支撑。

目录

声明

摘要

1．绪论

1．1 研究背景

1．2 研究现状

1．2．1 PICS技术标准体系

1．2．2 POWDER技术标准体系

1．2．3 绿色上网技术标准体系

1．3 待解决技术问题和研究目标

1．4 研究内容

1．5 主要研究成果和创新点

1．6 论文结构

2．形式化目标建模与技术标准体系开发策略

2．1 引言

2．2 形式化开发方法

2．2．1 形式化方法概述

2．2．2 形式规约

2．2．3 线性时态逻辑

2．3 目标建模技术

2．3．1 目标建模概述

2．3．2 行为目标模型表示

2．3．3 行为目标建模方法

2．3．4 行为目标精化模式

2．4 目标驱动的技术标准体系开发技术基本思想和策略

2．4．1 技术标准概念辨析

2．4．2 技术标准体系概念辨析及其开发阶段划分

2．4．3 基于技术标准规约逐层精化的技术标准体系整体设计

2．4．4 技术标准体系整体设计中的目标精化方法

2．4．5 技术标准体系整体设计描述方法

2．5 目标驱动的技术标准体系开发流程

2．5．1 技术标准体系整体设计的开发思路

2．5．2 目标驱动的技术标准体系整体设计开发流程

2．6 本章小结

3．互联网内容分级形式化目标建模

3．1 引言

3．2 基于自律的互联网内容自由传播业务环境目标建模

3．2．1 基于自律的互联网应用环境行为描述

3．2．2 登录用户使用互联网的基础行为模式

3．2．3 基于自律的互联网应用环境行为目标模型构建

3．3 互联网内容分级业务目标分析

3．3．1 基于自律的互联网应用环境问题分析

3．3．2 期望互联网应用环境业务目标分析

3．4 期望系统目标建模

3．4．1 不良内容接收过滤目标建模

3．4．2 互联网内容接收定制目标建模

3．4．3 不良内容举报处理目标建模

3．5 互联网内容分级服务行为目标

3．6 本章小结

4．互联网内容分级服务技术标准体系的形式化目标建模

4．1 引言

4．2 互联网内容分级技术标准体系目标建模方法

4．3 不良内容接收过滤类系统目标建模

4．3．1 顶层目标精化

4．3．2 1级目标精化

4．3．3 2级目标精化

4．3．4 不良内容接收过滤类系统目标模型

4．4 互联网内容接收定制类系统目标建模

4．4．1 顶层目标精化

4．4．2 1级目标精化

4．4．3 2级目标精化

4．4．4 互联网内容接收定制类系统目标模型

4．5 不良内容举报处理类系统目标建模

4．5．1 顶层目标精化

4．5．2 1级目标精化

4．5．3 不良内容举报处理类系统目标模型

4．6 本章小结

5．互联网内容分级服务技术标准体系形式化设计

5．1 引言

5．2 技术标准体系构建方法

5．3 组成技术标准提取和定义

5．4 技术标准体系层次结构

5．5 技术标准体系应用实例

5．5．1 互联网内容分级服务的上下文环境

5．5．2 基于本技术标准体系的顶层协同交互行为建模

5．5．3 基于本技术标准体系的第2层协同交互行为建模

5．5．4 基于本技术标准体系的第3层协同交互行为建模

5．6 本章小结

6．互联网内容分级服务技术标准体系形式化验证

6．1 引言

6．2 验证方法和前提条件

6．2．1 基于线性时态逻辑的系统形式化验证方法

6．2．2 技术标准体系验证前提条件说明

6．3 技术标准体系正确性证明

6．4 技术标准体系能力验证和分析

6．5 本章小结

7．总结与展望

7．1 论文工作总结

7．2 后续工作展望

7．2．1 各组成技术标准详细设计和验证

7．2．2 互联网内容分级服务协议栈开发和验证

参考文献

附录

读博期间发表及录用的论文

致谢