我对模型检测有了新的认识，这是一个值得尊敬的技术。而且在安全性验证领域将会有极其强力的表现。
形式化验证手段，体现出来的就是模型检测技术。这个方向，在研究生期间都不一定能达成某种成绩，企业更需要精通某点的博士生来做研究。
确定研究方向的三个层次：
- 最基本的最核心的产生最大效益的底层理论研究
针对模型检测，就有以下方向可以选择：- 系统的自动化、程序化建模
- 改进遍历算法
- 改进构建约束的演算方法
- 针对模型检测中的重大问题：状态爆炸 现有的技术：偏序规约，组合推理，抽象，对称，归纳
- ...
底层方面的开题，范围太大，足够支撑两个博士毕业论文。可行性不高。不建议把落脚点放在这里。
- 现有技术的新场景的应用
其实这也是一个很大的话题，比如之前将形式化方法验证放在区块链处，这显然是一个非常有想法的可行性高的方向。这就是一种创新。
模型检测的应用范围的确有限，但是在这个有限的空间中，我们已经可以解决一大部分自动验证的问题。
其实这一块，我们已经基本确定，我们要做软件的模型检测。老师的想法是，针对C语言的遍历。 - 某种新技术与模型检测技术结合应用在某种场景
- 针对具体代码做模型检测，然后证明该方法的重要性，可行性。
最终还是回到老师的开题上。饭要一口口吃。和写项目的一个原理，先从最核心的入手，做出一些成果。起步都是模仿。
做研究都是这样，先学会用，然后才能对之有更深层的认识，才能对底层技术提出改进措施。
我的开题：基于uppaal的xxx类软件面向某类安全性约束的形式化建模与仿真
创新处：在满足XXX约束下的某类软件系统，我们都可以通过这种方法，进行自动化测试，确定是否存在这种类型的软件缺陷。
说服力：用传统的软件测试方法，无法发现该类问题，或者将耗费极大的人力物力。
入手点：
- 从UPPAAL的成功案例中，选取合适软件案例，修改适应，扩大应用范围到该类。
