基于时间着色Petri网的OpenFlow协议建模研究

Presentation on theme: "基于时间着色Petri网的OpenFlow协议建模研究"— Presentation transcript:

1 基于时间着色Petri网的OpenFlow协议建模研究
李元平1a,2 李华1a,b 赵俊岚2 (1 内蒙古大学 a 计算机学院; b 网络中心,呼和浩特 ; 2 内蒙古财经大学网络中心,呼和浩特010070) Concurrent system Model

2

3

4 国家“互联网+”的经济发展战略，新技术蓬勃涌现，发展日新月异。
1）研究背景 国家“互联网+”的经济发展战略，新技术蓬勃涌现，发展日新月异。 当前的网络研究范型主要有SDN 、ICN、移动互联网、工业互联网、农业互联网以及物联网 SDN特点：分离可管控 集中可定义 开放可编程，得到工业界，学术界，IT社区的支持，展现出蓬勃的活力。 scott shenker:三层抽象 对应 我们的关注点 OpenFlow协议的扩展

5 我们要做什么？What? 对OpenFlow协议进行测试 应该怎么做？ 通过形式化建模，我们希望得到什么?
1）研究背景 Test Dreams: 统一的测试理论 基于模型的测试(MBTCG) 100%的自动化 高效的测试引擎. Bertolino A. Software testing research: Achievements, challenges, dreams[C]//2007 Future of Software Engineering. IEEE Computer Society, 2007: 我们要做什么？What? 对OpenFlow协议进行测试 应该怎么做？ 通过形式化建模，我们希望得到什么? 对OpenFlow协议得到整体理解 如整体关系，重要变迁效率等，量化指标 由模型得到抽象测试例 整体关系 如交换机 控制器 怎么进行形式化建模?How?

6 2）层次建模 状态、迁移形式化描述 编程语言形式化描述 Hybrid Sunshine C. Formal techniques for protocol specification and verification[J]. Computer, 1979, 12(9): OpenFlow协议Top层建模 OpenFlow协议交换机子页建模

7 Agent&Driver功能建模 OpenFlow交换机流表检索建模 2）层次建模
Agent&Driver功能建模 实际中采用netty，本质上是socket，tcp链接 默认：6633 Agent&Driver功能建模 OpenFlow交换机流表检索建模

8 控制器功能建模 1`{opf_type=0 ,opf_cont="hello message"}++
2）层次建模 1`{opf_type=0 ,opf_cont="hello message"}++ 1`{opf_type=1 ,opf_cont="error message"}++ 1`{opf_type=2 ,opf_cont="echo req message"}++ 1`{opf_type=3 ,opf_cont="echo rep message"}++ 1`{opf_type=4 ,opf_cont="experiment message"}++ 1`{opf_type=5 ,opf_cont="function req message"}++ …… 控制器功能建模

9

10 Token选取与变量的定义需与业务需求相匹配，如无必要，勿增Token.Why?
OpenFlow模型变量定义 OpenFlow模型colour集定义 OpenFlow网络建模中函数定义

11

12 02 基于ASK-CTL（分支时序逻辑）的编程
1）验证方式 01 CPN Tools所提供查询函数 利用此部分进行模型验证最为简单实用，但是表达能力有时候欠缺。 02 基于ASK-CTL（分支时序逻辑）的编程 根据ASK-CTL分支时序逻辑，结合ML进行自定义编程，扩充CPN Tools功能。此方法表达能力强，但是相对复杂。 03 结合编程语言的验证方式 利用高级编程语言结合CPN Tools进行相关分析，此方法符合一般的编程人员思路，但是首先需要得到CPN Tools运行后的状态空间文件，且首先需要转换，相对耗时，但是转换之后可以利用熟悉的方式进行分析。

13 OpenFlow网络模型自定义验证函数分析
2）本次结果 OpenFlow网络模型自定义验证函数分析

14

15 transport agent message变迁执行次数与触发时钟参照表

16 transport controller message变迁执行次数与触发时钟参照表
f(x)=ax (a>1) f(x)=xa f(x)=ax (a>1) 指数函数 f(x)=xa 幂函数 随着变迁执行次数的增加，控制器会成为我们的瓶颈部件 transport controller message变迁执行次数与触发时钟参照表

17

18 由点及面 不断拓展 Openflow协议的形式化建模 测试生成工具集的开发 抽象测试例的产生 传统测试方法的应用创新，如适应性测试的考虑等

19