我的想法
模型检测首先检测的是模型，如果我们把立足点放在软件代码层次，那么将面对海量的状态爆炸问题，导致无法建模无法推进工作，同样做出来的东西适用范围小，仅仅是自己的作为演示的例子。
但是，如果能够把思维扩展、层次提高之后，可以看到模型检测在软件设计建模阶段将会发挥大作用。
现阶段有人在研究从软件设计模型到软件实现的自动化生成方法，并已经有成果。
所以当我们使用模型检测的证明手段，在保证软件设计模型的必然正确性的前提下，通过UML生成的所有软件，都将是完备的，无缺的。
前景展望：这将会是颠覆性的创造。淘汰的不仅是测试人员，还有底层写代码的程序员。
资料收集
- UML类图和时序图在软件设计中的应用，其中包括软件的23种设计模式
http://design-patterns.readthedocs.io/zh_CN/latest/read_uml.html
时序图
http://blog.51cto.com/smartlife/284874 - 相关的UML的工具 着重考虑强大的EA工具
论功能的强大，RSA仍然是第一位的，不过个头很大、价格昂贵。近年来，Enterprise Architect（简称EA）逐渐成为大多数开发人员学习建模的首选工具。EA的使用风格和以前的Rose接近，个头又不大，很方便开发人员自行安装学习，价格也适中，堪称性价比最好的工具。
实时系统开发方面，Rational Rhapsody是目前最好的工具，可以在类图、状态图层面上做设计级调试，生成各RTOS下可直接运行的代码
https://blog.csdn.net/yangbindxj/article/details/12503763 - 稍微看一下从UML建模到代码的自动生成的相关技术和应用
具体阶段性的成果展示
将我的BBS系统，通过以上UML+时序图+模型检测工具，做成一个例子，找出传统测试发现不了或需要耗费大量人物力资源找到的Bug.
可行性调研
- 查找论文，看是否已经有人做了相关的工作，最前沿的工作目前推进到了哪里？
重点任务！！！
- 崔康乐. UML时序图模型到UPPAAL时间自动机模型转换方法研究和工具实现[D]. 华东师范大学, 2011.
以上论文实现了从UML时序图到UPPAAL模型检测工具的转换，并开发了对应工具 - 张频, 罗贵明. UML模型检测方法的研究[J]. 计算机应用, 2007, 27(10):2493-2497.
以上论文实现了从UML状态图到SPIN工具的转换，并开发了对应工具UMLChecker - 彭大天. 基于UML和UPPAAL的FAO系统典型运营场景的建模与验证[D]. 北京交通大学, 2013.
上述论文针对具体场景：全自动驾驶 使用UML和形式化结合的方式对实际应用做了相应的验证，同样开发了UMLtoUPPAAL工具（时序图） - 石娇洁, 胡军, 刘雪,等. 一种嵌入式系统模型的安全性分析验证方法[J]. 计算机技术与发展, 2015(10):7-12.
这个文章中重点是有个民用机的机轮刹车例子可以利用，进行改造
- 调研UML等相关软件设计建模工具在实际工业中的应用比例？
考察UML建模的表达力，该建模形式是否可以完备的描绘软件功能特征
https://en.wikipedia.org/wiki/List_of_Unified_Modeling_Language_tools
http://www.umlchina.com/Tools/Newindex1.htm - 考察现有的模型检测工具
https://en.wikipedia.org/wiki/List_of_model_checking_tools - 建模工具与验证工具之间的桥梁是否容易打通
这部分建议多看论文，汲取营养
