利田小子

RPE做完后，这段时间老板没有给我新的活，而且看样子好像不会继续做RPE时做的东西，这样有点可惜，毕竟整了大半年，总不能没有什么产出就放弃了。老板政务缠身，学术方面已经不再那么热衷了，这可以从他从不和我提发paper的事看出。倒是我自己，一直想着什么时候能发我的第一篇论文，目前还是鸭蛋，这学期一过，来美也算两年了，一年TA，一年RA，一篇paper都没有，说出去有点丢人。来美读了两年PhD的而没有发paper的人，应该没有多少，我不想成为其中一员。咱不是大牛，但不能因此放弃努力，该争取的还是要去争取。

某天，忍不住了，就跑去和老板谈，看看能不能将RPE做的东西整成一篇论文。老板说可以，但得对实验部分稍作修改。虽然成功地对系统进行了模拟，模拟结果也和我们预想的一样，但实际上，Uppaal不适合模拟我们这类系统（Highway Collision Warning System Based on Wireless Sensor Network），因为它的很多功能达不到要求，和我们预想的偏差有点大。所以光有模拟不行，一方面模拟本身做了很多假设，把一些重要参数都做了假设，比如broadcast参数（没办法，Uppaal做不到）；另一方面，只对少数vehicle进行了模拟，但如果要验证这类系统的performance，那得做大量的模拟，而不是几辆vehicle，但几辆vehicle的模拟已经快把Uppaal系统给整垮了，做大量的模拟问题会有一大堆。此外，鉴于我们的那些假设，做这些模拟也没多大意义，因为假设本身就是模拟的重要部分，但我们都忽略了。因此，我们的实验展示不能从模拟入手，不能验证系统的performance，而且Uppaal也做不到。我们只能把出发点定在我们的协议上，Uppaal提供了属性检验功能，也就是可以对协议的某一方面属性进行验证，比如协议的有效性，相关车辆是否收到了warning message，broadcast的连续性，即只要有问题车辆存在，就得有warning message在广播。如果我能验证一些关键的属性，那可以把这些内容放入实验展示部分，起码说明了系统的正确性和有效性。

但验证系统没那么简单，事实上，在我们已经完成的系统中，我已经对一些属性进行了验证，某些能验证出来对错，某些会搞垮系统，导致out of memory。因为我们建的几个自动机模型都挺大，而且实验中会生成9个以上的自动机，这些自动机的执行过程互相交叉，再加上定了很多变量，导致系统的state非常多，使得Uppaal验证不了。如果验证某属性是否存在成立的可能性，一般都可以验证成功，因为验证存在性不需要遍历整个系统。但要验证某属性是否永远成立，就我们验证的情况来看，都会导致out of memory，而这些属性对我们的系统来说又有点重要（这一点，Uppaal比Spin差一些）。虽然在RPE Presentation中，我向committee解释了这一情况，并且我也没有解决办法，但现在，如果我想发paper，非得把这个问题解决。我能做的就是修改程序，尽可能的缩小系统，并减少可能的系统状态数目，这是个大工程啊。

和老板谈完之后，自己上网搜了相关会议，发现IEEE的一个关于Intelligent Transportation Systems的会议，我们做的东西正好在这一范围内。今年这个会议将在葡萄牙举行，九月份的时候，Paper提交的截止日期是3月15日。也许我可以试试，就发邮件问老板，老板说可以，但时间挺紧。差不多15天的时间，我得这周把程序改好，然后写paper，修改之后提交。构想挺好，但摆在眼前的还是老问题，程序。得绞尽脑汁把问题解决了，不然就么的希望了。之后老板又发了个会议给我看，WiCOM。今年的WiCOM会议在成都举行，老板说我也可以试试这个。嗯，如果能搞定程序，前途一片光明啊。这周拼了！

转载请注明出处: 利田小子[http://www.zhuhuang.com]

本文链接: http://www.zhuhuang.com/2010/03/wish-to-publish-first-paper/