这几天我重新审视了几篇论文。 目的是再次扫描这个领域，不断地以单方面的形象追求全面的形象，甚至是深刻的形象。 基本动机是对现有的这个工具有更多的了解。
static testing，或static analysis，static verification的重要性得到理论界和工业界的充分广泛支持，工具的种类、功能超出了我事先的想象，Matlab本身就有这方面的扩展： polyspacacation 另外，成熟的工具和制造商也达到了一定的规模，如Coverity、QAC、Purify、PCLint等，SPIN、NuSMV以及基于这些的更接近实践的Modex/FeaVer/SPIN工具切
实用性是这次收获的关键词。
practicability意味着scalability、soundness、extendability这三个要求。 可伸缩性是提升实验室、稿纸理论成果投入到现实中大项目的必要条件，否则，这些技术永远只是theorist’stoy。 由于可靠性是对实现技术的正确性的要求，是一种实现技术，其准确性不仅限于理论上一些假设下的一些情况，而是取决于现实所有可能条件下的外在表现。 可扩展性是确保一个工具拥有一定的使用寿命的根本所在，也是根本价值。 其功能不是固定的，必须具备应对一定范围内需求变化的能力。 适应能力越高，工具的寿命越长。
目前，2008 ACM Turing Award获奖者的工作大大改善了模型检查相关算法的性能，Cousot为程序解释提供了坚实的理论基础，硬件计算能力将这些理论方法应用于实践但是，从测试的初衷来看，无法保证找出任一程序中存在的所有错误，因此，这种工具的适用语言、领域范围必然有限，另外，其错误检测的有效性(coverage、falage ) 降低FPR需要反馈筛选更多信息； 要提高coverage，就必须放松假设，网罗更多的可能性。 假说和信息本来就是一体的，信息一多，假说就变强； 假设放松的话，信息会变少。 这也是entropy的死律。 最后剩下一个，好像还没有死律。 仔细考虑需求，讨论测试所需的东西和工具提供的功能之间会填补什么空白，以及如何搭建桥梁以确保这一差距是灵活可调的。
具体来说，就像需求分析，不是实现问题。 测试人员想自动化什么样的任务？ 工具的哪些工作在实践中没什么用？ 在这些可能实现的功能、想要实现的功能之间可以挖掘出什么样的模式呢？ 模型出来了，问题才能解决根本问题，进入实现阶段。
目前的思路是，第一步通过parser将分析的触角渗透到程序结构中，然后将程序中的信息吸附到AST树中，建立分析所需信息的流水线系统，根据需要，采用翻译方式建立异步并行模型，通过多次扫描集合
研究中的一些错误想法：
1 .要全面调查领域内现有的所有方法、工具，博采众长——这是一项力所能及而无法完成的任务。 多出现在文献中，尽量掌握典型的方法、工具，一般3-4即可，超过5可能难以掌握。 另外，软件分析验证领域门槛较高，贪婪求全只是囫囵吞枣无法消化，对最终目标没有多少好处。 最终目标还是开发有自己特色的方法、工具，如果别人的想法接近自己的，使用方便的话，“拿来”也可以。 否则，如果对方很复杂，想法不同，即使很强大，也不需要学习掌握。 因为这样无益于提高自己方案的创新性，只会削弱，只会强化自己方案的功能，没有多少学术价值； 实践上来说，即便是学习掌握了，最终整合后也往往需要根据需要进行修改，此时以前的硬拼接工具很难调整，工程意义也不大。 优选的研究方法是在了解3-4的典型方法、工具后，暂时总结这些特征，而不是其他方法、工具，修改最初的需求。 这是第一阶段。 第二阶段是开始回归，根据修改后的需求，重新独立考虑实现方案，确认每个实现方案有什么好处是重要的一步，要在这一步确定自己方案的核心特色。 此时还不能说是创新。 因为以前的调查不够。 因此，这一核心特色必须具有十分坚实的现实意义，同时难度适中，存在创新空间。 这是所谓的“选择点”，是重要的一步。
2.
例如，在嵌入式软件分析验证技术中，目前的现实需要是实用化，希望自动化测试工作，并扩展狭窄的原型工具应用于实际复杂的项目。 但是，这很难。 现实太复杂了，不完整。 另外，创新空间不大，有很多直接支持C程序的并发模型检测工具Modex、C代码典型的运行时错误检测工具Lint，以及C代码静态分析支持工具Frame-C。 那么，需要进一步挖掘和细化现实需求，探讨这些工具的可改进之处。 首先，它们都是针对ANSI-C的，实际上它们只是用于ANSI-C的子集，似乎不支持扩展。 这是在嵌入式领域运用的最大障碍。 伯克利大学的CIL是对c程序分析和转换的专门支持，它具有正确定义的API，采用Ocaml实施，封装良好，应该可以轻松集成并作为预处理程序。 其次，这些工具是自动化的，可以拉直
接给出测试人员需要的关键信息。但是，需要测试人员输入大量信息以指导工具内部的建模操作。这本来就是一种权衡。将一些输入也自动化会降低工具的适用范围，但是可以强化工具的使用效率。再次，这些工具竟然没有一个是从“测试”的角度提出来的，从而可以发现：它们都忽略了测试领域的一个重要考虑因素：缺陷模型，而是抽象的看待程序中可能存在的问题，这样就出现了一个很大的应用创新空白。就嵌入式软件测试而言，也大致可以划分为几类，缺陷也有一些典型的特征，这些信息都可以用来指导工具内部的建模操作，总结一下，就可以作为工具的一种配置接口。同时，工具的输出也可以利用这些信息做出更加有背景意义的描述，作为一种输出接口。相当于增强了工具的功能，同时，也是特定类型缺陷的新的测试方法。——这里，创新的模式是“背景挖掘”。还是没见到创新的主要模式：“持续改进”。比如改进一个算法的效率。一般具有深厚理论基础的技术，算法都是建立在大量的模型、符号上，门槛高；而如果只是一种操作方法如随机测试用例生成方法，则不需要专门的精神数学模型，采取一种具体数学的思维来改进。我当然希望遇到的问题都是这种低门槛的、技巧性的问题，从而不需要做太多前期功课就可以产生所谓的“创新”。但是，技巧是需要的，然而，刻画才是永恒的。（对于上面这句话过敏的人，我们可以就具体数学这本书的一则书评讨论一下。）这里而言的刻画，就是所谓的中间层表示——一个用于程序分析、静态分析、模型检验等等诸多后期工作的公用操作对象——这个暂时还不存在，我觉得也不存在。一种可行的机制仍然是，就不同的分析目标，建立相应的分析模型，然后分别从源代码开始做转换。如果需要什么统一的地方，那就是类似CIL这样的东西——将一些源代码中不合理的地方澄清一下——然后还是各干各的translator。
脚注：为什么需要CIL呢？直接用AST不就行了？——直接解析出来的AST是包含全部复杂C语法的，有很多的dark corner。CIL相当于化简了C，便于接下来的分析处理——正如它名称所说，for program analysis and translation。