报告一：Deriving Unbounded Proof of Linear Hybrid Automata From Bounded Verification

报告人：解定宝

简介：This talk presents a technique that can derive, in some cases, a proof of unbounded reachability argument of Linear Hybrid Automata (LHA) from a Bounded Model Checking (BMC) result. During BMC checking of LHA, typical procedures can discover sets of unsatisfiable constraint cores, a.k.a. UC or IIS, in the constraint set according to the BMC problem. Currently, such unsatisfiable constraints are only fed back to the constraint set to accelerate the BMC solving. In this talk, we propose that such unsatisfiable constraint core can be utilized to give general unbounded verification result of the model. We propose to map the unsatisfiable constraint cores back into path segments, which are not feasible, in the graph structure of the LHA model. Clearly, if all the potential paths which can reach the target location in the graph structure have to go through such infeasible path segment, the target location is not reachable in general, not only in the bound.

To solve such problem, we propose to encode the infeasible path segments as LTL formulas, and present the graph structure of an LHA as a transition system. Then, we can take advantage of mature LTL model checking technique to verify whether there exists a candidate path which can reach the target according to the LTL formulas. We implement this technique into a new version of BACH, the experiments show that the performance of our tool outperforms the-state-of-the-art competitors, significantly.

报告二：面向时间约束的嵌入式闪存存储系统研究 

报告人：张琦

简介：近年来，NAND闪存因其非易失性、高读写性能、低功耗、抗震动等特点被广泛应用于各类嵌入式系统中，然而由于存在异地更新和垃圾回收等限制，闪存存储系统无法在给定时间约束下确保读写操作的执行；同时，传统嵌入式实时系统并没有考虑存储系统的时间性质，随着嵌入式系统对功耗和数据持久存储的日益关注，时间性质在嵌入式存储系统的设计和实现中变得愈发重要，因此，报告从NAND闪存存储系统的基本框架出发，介绍影响闪存时间性质的关键因素并提出一种面向时间约束的NAND闪存转换层，具体包括实时垃圾回收机制和基于需求的地址映射策略，最后对下一步的工作进行介绍和讨论。