- 更新了我的认识，形式化技术是一门在有限状态某些场景下有力的工具。
必须将状态很好的抽离，状态之间的转变也可以表述的情况，模型检测才能最大化发挥作用。 - 然后uppaal作为一种模型检测工具，最大的优势在于可以对实时系统进行建模。
uppaal上给的例子，分这么几类：1.实时系统 2. 协议验证 3. 控制器 4.硬件电路逻辑
在软件上，我在uppaal官网给出的例子中还没有看到。 - 如果做软件模型检测，首先我们要实现对程序的建模和验证。经过我的思考，可以放在以下几点上：
- 我们自己开发一种程序的建模技术
- 我们自己开发一种程序的验证技术，即遍历技术（老师之前跟我说的，我认为是这个技术）
- 利用别人的已有技术，应用在新的方向
- 在别人已有技术上做一些改进，举一个例子说明改进的优势
- 我们可以选择做控制器方向，也是安全性验证手段，例如书上186页的飞行控制器。也可以在软件的上一层进行建模。软件流程图级别。
其实我们现阶段做的所有形式化工作，都是属于这一类。其中包括大师兄的两个例子，防冰的，614所的，赵玉坤的毕业论文
网友评论