**报告一：****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闪存转换层，具体包括实时垃圾回收机制和基于需求的地址映射策略，最后对下一步的工作进行介绍和讨论。 |