汇报内容

1、汇报formal method一书的第三章

​ 第三章中的的一个问题，用不变量(invariants)在不同点进行检查程序的正确性，什么意思？

​ 第三章讲述了什么是程序验证，什么是谓词，表达程序正确需要引入足够的符号等

​

导师反馈内容

1、《面向智能驾驶的多粒度动态认知决策行为建模与验证方法》一个项目中，从三个方向进行保证自动驾驶，时空理论、精化理论(粒度粗细)、协同方法进行思考。

精化理论：粗细粒度、如何决策、如何预测（后面两个不一定属于精化理论）

其中对于多种粒度之间划分，其中粗粒度是对于决策不紧急且决策快，细粒度是需要紧急处理且时间长，但细粒度得包含在粗粒度中，这里有一个问题，即如何对于多种粒度之间的一致性如何保证(精化理论)。

接着example车辆行驶：

粗粒度：后面车的去向进行划分区域，且区域距离我方左转还远或者我方车并不会左转(即划定不能去的范围)

细粒度：决策出后方车所有的决策路线，且出现我方车左转，且对方车也会出现这条路上

更细粒度：预测对方轨道的权重分配，作出最有可能的决策

2、什么是不变式，不变式存在的情况

1、循环不变式，只出现循环体的程序代码中，在循环体一开始和循环体结束给出不变式条件

2、EVENT-B：事先给出了全局性质，没做一次保持的状态性质。

3、如何做AI可信验证

将AI系统进行拆分，分为传统的系统以及具有AI性质的系统，原本大的AI系统满足的需求就是我们要完成的任务，传统的系统进行抽象描述，将具有AI性质的系统的上界(全部正确)和下界(全部错误)，然后在具有AI系统的上下界之间进行取值(进行AI的调参数)，然后反例引导精化。