利田小子

周五时基本上把程序改到最小了，系统能砍的我都看了，变量能不用的我都删了，能做的我都做了，但不是所有的system properties都能验证出来，还是一个属性验证时会出现out of memory的错误。能验证出来的属性对验证系统的正确性没有什么帮助，比如证明某属性是否可能存在时（即Uppaal的Possibly属性，E<>p），我们要求的是“肯定的”，比如Invariantly属性（A[]p），Potentially always属性（E[]p），和Eventually属性（A<>p）”，而不是“可能的”。此外，Uppaal的这些属性验证似乎也达不到我们想要的效果，他们的验证方法和我们预想的不大一样。我想，也许，可能，我们的系统不适合在Uppaal上模拟。看过一些别人用Uppaal做验证的paper之后，发现我们的model的确过于复杂，而且数量太多。普通的paper最多只用了两三个，但模拟中，我们用了至少9个automata。
Read more…

查了一遍原来写的系统模拟代码，在代码和自动机上做了写必要的修改，没什么大的问题。但到模拟时，出现了一个exception，提示range error，好像是数值的范围问题，但没有指出在哪出的错。Uppaal没提供调试工具，我也不知错在哪，通查了一遍程序，没找到可能的出错点。这样耗着也不是办法，最后我新建了一个系统，将原系统一块一块分割出来，分别调试。最开始测试了Timer自动机，模拟timeout的，同时测试了消息的插入和删除，车辆位置关系确定，不变式判断等函数，并在自动机上调用，发现了一些问题，改过之后就能模拟了。Timer自动机和原系统的差不多是一样的，另外一个自动机则是后来新建的，没什么移植性可言。第二次尝试，只添加了三个自动机，一个Timer，一个Message，一个Trigger Vehicle，和相应的定义声明，在没有syntax error的情况下，进行模拟，出现了range error的exception，看来问题可能就在这三个自动机里。于是一个一个测试，先测Timer，这个Timer和我已经测过的就在自动机参数上有所区别，原来的Timer定义了一个整型值，并通过值传递的方式传给Timer，新加的Timer定义的是const整型值，用引用传递（带const），觉得应该不会有什么问题。但测试结果并非如此，提示有syntax error，依旧没指出在哪。为了简单，就把该整型值设成普通的，而不是const，及完全按测过的Timer自动机进行修改，进行模拟，可以了。于是把原系统的三个Timer自动机都改了一下，check syntax，没问题，试着simulation，居然成功了，再没有什么exception和syntax error。虽然比较偶然，但能出结果还是很高兴的，跑去跟老板说了一下。至今还没搞清楚为什么这些参数会导致那个exception，不过无所谓了，现在要的是结果，因为赶着做presentation。剩下的事就稍微好办些了，在原系统基础上进行修改，一是完善一下系统的功能，二是确定要要验证的东西，并在系统里实现。因为做presentation时，不能光给个系统实现，之所以做这个系统实现是有目的的，就是要验证我的系统在给定or假设的环境下能够work，所以我得prove。至于怎么prove，今天在给老板看模拟过程时讨论了一下，有了个idea，就先按着做吧。打算后周做Presentation，下周老板没空，这周把程序弄完，下周写report和ppt。

RPE还剩最后一个presentation，原定于1月26日做的，但目前来看，恐怕得推迟了。最近在做系统的模拟，Uppaal这工具功能实在让人憋屈，很多东西都无法实现。模型，函数等都弄好了，但运行不起来，说是有syntax error，但用Uppaal自带的Syntax Check功能根本就无法找出错误的地方。没有办法，现在的打算是，把所有函数和自动机模型重新翻查一遍，看能不能找到问题。看过一些用Uppaal做模拟工具的paper，和他们的系统相比，我们的系统要复杂的多，如果用Java，C之类的语言实现，应该不难，但我们挑了Uppaal，没办法，来不及换了，只能尽可能地去实现，系统该简化的就简化，直到能模拟出结果。和老板开会了，预计是无法在1月26日前完成模拟，除了模拟，还有report和ppt，这些也都还没准备。明天就给committee member发邮件，看能不能推迟一到两周。希望这周之内能把模拟的问题解决，下周写报告和ppt。

RPE最后一个Presentation就在月底，1月26日，到时我提交系统的模拟结果。最近一段时间忙着编程，看Uppaal已有些时日了，也看过一些编程的例子（都是很简单模拟），但没有在上面写过程序。Uppaal使用的语言有点像C语言，但Uppaal的功能不是很强，它的编程语言也有不少限制。对于要模拟的系统，我已经把它的伪代码写完了。根据Uppaal的情况，已经搞清如何把系统移植到Uppaal上，需要建多少自动机，自动机之间如何协调等，并且在草稿纸上根据构思好的函数和变量等构建好了这些自动机。这些天的工作，就是编程，按着脑子里的系统模型和画好的自动机在Uppaal上实现。刚开始使用Uppaal编程，免不了一些问题，但都解决了，一切还算顺利。时间有点紧，希望能提前十天完成任务（还有五天时间），这样才有足够的时间写report，准备PPT。

从暑假一直拖到上周，终于把RPE request form填完上交了，committee member也都确定下来了，Dr.Gurdip Singh，Dr. Torben Amtoft，和Dr. Daniel Andresen，他们也是我的PhD committee member，除了那个外系的老师。老板说，RPE是系里的考试，按规定不用通知外系的老师。这样也好，光是系里的三个老师，要从他们的schedule找到共同的空余时间都不容易（跑了n次，确定了n次），再加个外系的老师，估计找不到共同的free time的。以下是从PhD Guideline里截取的RPE里要做的事：
Read more…