我的想法
模型檢測(cè)首先檢測(cè)的是模型，如果我們把立足點(diǎn)放在軟件代碼層次稽煤，那么將面對(duì)海量的狀態(tài)爆炸問(wèn)題，導(dǎo)致無(wú)法建模無(wú)法推進(jìn)工作模暗，同樣做出來(lái)的東西適用范圍小走搁，僅僅是自己的作為演示的例子府寒。
但是唱凯，如果能夠把思維擴(kuò)展尔许、層次提高之后喜庞，可以看到模型檢測(cè)在軟件設(shè)計(jì)建模階段將會(huì)發(fā)揮大作用诀浪。
現(xiàn)階段有人在研究從軟件設(shè)計(jì)模型到軟件實(shí)現(xiàn)的自動(dòng)化生成方法，并已經(jīng)有成果延都。
所以當(dāng)我們使用模型檢測(cè)的證明手段雷猪，在保證軟件設(shè)計(jì)模型的必然正確性的前提下，通過(guò)UML生成的所有軟件晰房，都將是完備的求摇，無(wú)缺的。
前景展望：這將會(huì)是顛覆性的創(chuàng)造殊者。淘汰的不僅是測(cè)試人員与境，還有底層寫(xiě)代碼的程序員。
資料收集
- UML類(lèi)圖和時(shí)序圖在軟件設(shè)計(jì)中的應(yīng)用猖吴，其中包括軟件的23種設(shè)計(jì)模式
http://design-patterns.readthedocs.io/zh_CN/latest/read_uml.html
時(shí)序圖
http://blog.51cto.com/smartlife/284874 - 相關(guān)的UML的工具 著重考慮強(qiáng)大的EA工具
論功能的強(qiáng)大摔刁，RSA仍然是第一位的，不過(guò)個(gè)頭很大海蔽、價(jià)格昂貴簸搞。近年來(lái)扁位，Enterprise Architect（簡(jiǎn)稱(chēng)EA）逐漸成為大多數(shù)開(kāi)發(fā)人員學(xué)習(xí)建模的首選工具。EA的使用風(fēng)格和以前的Rose接近趁俊，個(gè)頭又不大，很方便開(kāi)發(fā)人員自行安裝學(xué)習(xí)刑然，價(jià)格也適中寺擂，堪稱(chēng)性?xún)r(jià)比最好的工具。
實(shí)時(shí)系統(tǒng)開(kāi)發(fā)方面泼掠，Rational Rhapsody是目前最好的工具怔软，可以在類(lèi)圖、狀態(tài)圖層面上做設(shè)計(jì)級(jí)調(diào)試择镇，生成各RTOS下可直接運(yùn)行的代碼
https://blog.csdn.net/yangbindxj/article/details/12503763 - 稍微看一下從UML建模到代碼的自動(dòng)生成的相關(guān)技術(shù)和應(yīng)用
具體階段性的成果展示
將我的BBS系統(tǒng)挡逼，通過(guò)以上UML+時(shí)序圖+模型檢測(cè)工具，做成一個(gè)例子腻豌，找出傳統(tǒng)測(cè)試發(fā)現(xiàn)不了或需要耗費(fèi)大量人物力資源找到的Bug.
可行性調(diào)研
- 查找論文家坎，看是否已經(jīng)有人做了相關(guān)的工作，最前沿的工作目前推進(jìn)到了哪里吝梅？
重點(diǎn)任務(wù)Ｊ琛！苏携！
- 崔康樂(lè). UML時(shí)序圖模型到UPPAAL時(shí)間自動(dòng)機(jī)模型轉(zhuǎn)換方法研究和工具實(shí)現(xiàn)[D]. 華東師范大學(xué), 2011.
以上論文實(shí)現(xiàn)了從UML時(shí)序圖到UPPAAL模型檢測(cè)工具的轉(zhuǎn)換做瞪，并開(kāi)發(fā)了對(duì)應(yīng)工具 - 張頻, 羅貴明. UML模型檢測(cè)方法的研究[J]. 計(jì)算機(jī)應(yīng)用, 2007, 27(10):2493-2497.
以上論文實(shí)現(xiàn)了從UML狀態(tài)圖到SPIN工具的轉(zhuǎn)換，并開(kāi)發(fā)了對(duì)應(yīng)工具UMLChecker - 彭大天. 基于UML和UPPAAL的FAO系統(tǒng)典型運(yùn)營(yíng)場(chǎng)景的建模與驗(yàn)證[D]. 北京交通大學(xué), 2013.
上述論文針對(duì)具體場(chǎng)景：全自動(dòng)駕駛 使用UML和形式化結(jié)合的方式對(duì)實(shí)際應(yīng)用做了相應(yīng)的驗(yàn)證右冻，同樣開(kāi)發(fā)了UMLtoUPPAAL工具（時(shí)序圖） - 石嬌潔, 胡軍, 劉雪,等. 一種嵌入式系統(tǒng)模型的安全性分析驗(yàn)證方法[J]. 計(jì)算機(jī)技術(shù)與發(fā)展, 2015(10):7-12.
這個(gè)文章中重點(diǎn)是有個(gè)民用機(jī)的機(jī)輪剎車(chē)?yán)涌梢岳米芭睿M(jìn)行改造
- 調(diào)研UML等相關(guān)軟件設(shè)計(jì)建模工具在實(shí)際工業(yè)中的應(yīng)用比例？
考察UML建模的表達(dá)力纱扭，該建模形式是否可以完備的描繪軟件功能特征
https://en.wikipedia.org/wiki/List_of_Unified_Modeling_Language_tools
http://www.umlchina.com/Tools/Newindex1.htm - 考察現(xiàn)有的模型檢測(cè)工具
https://en.wikipedia.org/wiki/List_of_model_checking_tools - 建模工具與驗(yàn)證工具之間的橋梁是否容易打通
這部分建議多看論文牍帚，汲取營(yíng)養(yǎng)
