可信软件工程中的逻辑方法研讨会 LEDS2015
会 议 组 织 研 讨 会 主 席 : 周 巢 尘 院 士 ( 中 国 科 学 院 软 件 研 究 所 ) 程 序 委 员 会 主 席 : 段 振 华 教 授 ( 西 安 电 子 科 技 大 学 ) 董 云 卫 教 授 ( 西 北 工 业 大 学 ) 工 业 专 题 主 席 : 叶 宏 研 究 员 ( 中 航 工 业 集 团 631 研 究 所 ) 会 议 组 织 主 席 : 李 向 宁 副 教 授 ( 西 安 电 子 科 技 大 学 ) 会 议 程 序 委 员 : 董 云 卫 教 授 ( 西 北 工 业 大 学 ) 段 振 华 教 授 ( 西 安 电 子 科 技 大 学 ) 李 宣 东 教 授 ( 南 京 大 学 ) 刘 志 明 教 授 (Birmingham City University) 叶 宏 研 究 员 ( 中 航 工 业 集 团 631 研 究 所 ) 李 亚 辉 研 究 员 ( 中 航 工 业 集 团 631 研 究 所 ) 王 戟 教 授 ( 国 防 科 技 大 学 ) 詹 乃 军 研 究 员 ( 中 科 院 软 件 所 ) 会 议 地 点 : 西 北 工 业 大 学 国 际 会 议 中 心 第 一 会 议 室 会 议 注 册 地 点 : 西 北 工 业 大 学 正 禾 宾 馆 1
可信软件工程中的逻辑方法研讨会 LEDS2015 图一 西北工业大学友谊校区校园地图 2
LEDS2015 会 议 日 程 9 月 10 日 上 午 ( 逻 辑 方 法 ) Session 1 主 持 人 : 董 云 卫 教 授 西 北 工 业 大 学 8:50-9:00 开 幕 式 9:00-9:50 谢 飞 教 授 美 国 Portland 州 立 大 学 Automata-Theoretic Approach to Hardware/Software Co-verification 9:50-10:40 张 立 军 研 究 员 中 科 院 软 件 所 概 率 模 型 检 验 算 法 10:40-10:50 茶 歇 Session2 主 持 人 : 刘 静 教 授 华 东 师 范 大 学 10:50-11:40 赵 建 华 教 授 南 京 大 学 Scope Logic 代 码 验 证 工 具 Accumulator 到 基 本 框 架 和 开 发 进 展 11:40-12:30 薛 锦 云 教 授 江 西 师 范 大 学 基 于 PAR 平 台 的 云 计 算 建 模 语 言 研 究 午 餐 ( 正 禾 宾 馆 二 楼 ) 9 月 10 日 下 午 ( 程 序 验 证 ) Session 3 主 持 人 : 田 聪 教 授 西 安 电 子 科 技 大 学 14:00-14:50 宋 富 讲 师 华 东 师 范 大 学 On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs with Call-by- Reference 14:50-15:40 甘 庭 博 士 北 京 大 学 Decidability of the Reachability for a Family of Linear Vector Fields 15:40-15:50 茶 歇 Session 4 主 持 人 : 夏 壁 灿 教 授 北 京 大 学 15:50-16:40 张 雨 博 士 海 南 大 学 一 种 面 向 CPS 的 控 制 应 用 程 序 协 同 验 证 方 法 16:40-17:30 田 聪 教 授 西 安 电 子 科 技 大 学 基 于 MSVL 的 程 序 验 证 研 究 进 展 3
9 月 11 日 上 午 ( 系 统 设 计 与 分 析 ) Session 5 主 持 人 : 薛 锦 云 教 授 江 西 师 范 大 学 9:00-9:50 陈 仪 香 教 授 华 东 师 范 大 学 A Framework for Data-driven automata design 9:50-10:40 孙 猛 副 教 授 北 京 大 学 A Framework for Off-Line Conformance Testing of Timed Connectors 10:40-10:50 茶 歇 Session6 主 持 人 : 陈 仪 香 教 授 华 东 师 范 大 学 10:50-11:40 杨 红 丽 副 教 授 北 京 工 业 大 学 WSN 数 据 收 集 协 议 建 模 分 析 与 测 试 11:40-12:30 王 捍 贫 教 授 北 京 大 学 一 种 云 存 储 管 理 系 统 的 建 模 与 验 证 午 餐 ( 正 禾 宾 馆 二 楼 ) 9 月 11 日 下 午 ( 模 型 检 测 ) Session 7 主 持 人 : 李 晓 红 天 津 大 学 14:00-14:50 冯 新 宇 教 授 中 国 科 技 大 学 Towards a fully certified preemptive embedded OS kernel 14:50-15:40 杜 德 慧 博 士 华 东 师 范 大 学 基 于 统 计 模 型 检 测 的 定 量 评 估 方 法 及 应 用 15:40-15:50 茶 歇 Session 8 主 持 人 : 张 立 军 研 究 员 中 科 院 软 件 所 15:50-16:40 张 苗 苗 研 究 员 同 济 大 学 Verification of ELDIs with Continuous Chops 16:40-17:30 李 晓 红 教 授 天 津 大 学 面 向 多 协 议 的 无 线 传 感 网 入 侵 检 测 方 法 17:30-18:20 陈 振 邦 博 士 国 防 科 技 大 学 MPISE: Symbolic Execution of MPI Programs 4
9 月 12 日 上 午 ( 工 业 应 用 需 求 与 研 究 进 展 ) Session 9 主 持 人 : 叶 宏 副 总 师 / 研 究 员 中 航 工 业 631 所 9:00-9:50 武 方 方 研 究 员 / 主 任 中 航 工 业 618 所 分 层 架 构 下 基 于 模 型 的 软 件 一 体 化 开 发 方 法 9:50-10:40 郭 向 英 研 究 员 / 主 任 航 天 科 技 502 所 航 天 器 嵌 入 式 软 件 中 的 虚 拟 测 试 方 法 及 应 用 10:40-10:50 茶 歇 Session 10 主 持 人 : 王 军 所 长 / 研 究 员 中 航 工 业 一 飞 院 10:50-11:40 李 亚 辉 研 究 员 / 主 任 中 航 工 业 631 所 机 载 嵌 入 式 软 件 安 全 性 分 析 方 法 研 究 11:40-12:30 牟 明 高 工 / 主 任 中 航 工 业 631 所 航 空 软 件 的 现 状 与 挑 战 午 餐 ( 正 禾 宾 馆 二 楼 ) 9 月 12 日 下 午 ( 模 型 与 定 理 证 明 ) Session 11 主 持 人 : 段 振 华 教 授 西 安 电 子 科 技 大 学 14:00-14:50 詹 乃 军 研 究 员 中 科 院 软 件 所 Automatic verification of stability and safety for delay differential equations 14:50-15:40 李 杨 佳 助 理 研 究 员 中 科 院 软 件 所 15:40-15:50 茶 歇 Termination analysis and invariant generation for polynomial programs Session 12 主 持 人 : 詹 乃 军 研 究 员 中 科 院 软 件 所 15:50-16:40 赵 恒 军 博 士 中 科 院 重 庆 绿 色 智 能 研 究 院 Verification of Elementary Hybrid Systems 16:40-17:30 董 云 卫 教 授 西 北 工 业 大 学 On the Relationship between Model Coverage and Code Coverage using MATLAB s Simulink 午 餐 : 正 禾 宾 馆 二 楼, 凭 餐 票 自 助 餐 晚 餐 : 正 禾 宾 馆 二 楼, 凭 注 册 参 会 证 桌 餐 5
交 通 路 线 : 1 飞 机 : 出 机 场 出 港 大 厅 就 可 以 看 到 机 场 大 巴 机 场 大 巴 有 五 条 线 路,1) 选 到 钟 楼 的 机 场 大 巴 在 西 稍 门 站 下 车 ;2) 选 到 高 新 区 的 机 场 大 巴 在 至 诚 丽 柏 酒 店 站 下 车, 车 票 27 元 / 人, 然 后 做 出 租 车, 到 西 工 大 正 禾 宾 馆 ;3) 机 场 直 接 做 出 租 车 到 西 工 大 正 禾 宾 馆, 车 费 150 元 左 右 2 火 车 : 出 了 火 车 站 出 站 口 就 在 广 场 外 找 40 路,40 路 ( 火 车 站 西 工 大 ) 站 下 车 ; 其 他 还 有 206,10,205,201,6,16, 游 7 和 608, 不 过 40 路 是 最 短 的 路 线 另 外, 直 接 做 出 租 车, 车 费 20 元 左 右 3 高 铁 : 西 安 北 站 步 行 至 北 客 站, 乘 坐 地 铁 2 号 线, 在 省 体 育 场 下 车, 然 后 乘 坐 40 路 公 交 车, 在 西 工 大 下 车,5 元 左 右 另 外, 直 接 做 出 租 车, 车 费 45 元 左 右 图 二 西 安 市 地 图 6
可信软件工程中的逻辑方法研讨会 LEDS2015 主 办 单 位 简 介 1 西北工业大学 西北工业大学坐落于古都西安 是一所以发展航空 航天 航海工程教育和 科学研究为特色的多科性 研究型 开放式大学 是 985 工程 211 工程 重点建设学校 隶属于工业和信息化部 是 卓越大学联盟 成员高校之一 西北工业大学计算机专业创建于 1958 年 是较早在全国高校中开设的专业 之一 学院现设有计算机科学与技术 电子商务技术和物联网工程等 3 个本科专 业 并承担全校非计算机专业的计算机基础教育 学院拥有 计算机科学与技术 和 软件工程 两个博士学位授权一级学科 4 个硕士点和 4 个博士点 并建有 计算机科学与技术 博士后流动站 现有教职工 149 名 其中中国科学院院士 1 名 千人计划一名 百人计划一名 博士生导师 33 名 教授 31 名 副教授 46 名 从日本 德国 新加坡引进多名海外人才 多数骨干教师曾赴国外留学 培 训和合作研究 2 西安电子科技大学 7
西 安 电 子 科 技 大 学 是 以 信 息 与 电 子 学 科 为 主, 工 理 管 文 多 学 科 协 调 发 展 的 全 国 重 点 大 学, 直 属 教 育 部, 是 国 家 985 优 势 学 科 创 新 平 台 项 目 和 211 工 程 项 目 重 点 建 设 高 校 之 一, 是 全 国 56 所 设 有 研 究 生 院 的 高 校 之 一,37 所 示 范 性 软 件 学 院 的 高 校 之 一, 也 是 全 国 20 所 获 批 设 立 集 成 电 路 人 才 培 养 基 地 的 高 校 之 一 西 安 电 子 科 技 大 学 计 算 机 专 业 源 于 1956 年 的 导 弹 系 统 专 用 计 算 机 专 业, 是 全 国 最 早 设 立 的 计 算 机 专 业 之 一 学 院 设 有 计 算 机 科 学 与 技 术 博 士 后 科 研 流 动 站, 现 有 计 算 机 科 学 与 技 术 和 软 件 工 程 两 个 博 士 学 位 授 权 一 级 学 科, 涵 盖 计 算 机 系 统 结 构 计 算 机 软 件 与 理 论 计 算 机 应 用 技 术 和 软 件 工 程 四 个 博 士 学 位 授 权 二 级 学 科,4 个 二 级 学 科 均 为 省 部 级 重 点 学 科 现 有 专 职 教 师 122 人, 其 中 教 授 24 人, 副 教 授 60 人, 博 士 生 导 师 36 人 ( 含 兼 职 ), 硕 士 生 导 师 98 人 其 中 包 括 教 育 部 长 江 学 者 奖 励 计 划 特 聘 教 授 国 家 新 世 纪 百 千 万 人 才 工 程 人 选 者 国 家 863 计 划 首 席 专 家 优 秀 青 年 基 金 获 得 者 教 育 部 新 世 纪 优 秀 人 才 计 划 入 选 者 等 3) 机 载 弹 载 计 算 机 航 空 科 技 重 点 实 验 室 ( 中 航 工 业 集 团 631 研 究 所 ) 西 安 航 空 计 算 技 术 研 究 所 ( 中 国 航 空 工 业 第 631 研 究 所 ) 是 从 事 机 载 弹 载 计 算 机 和 航 空 软 件 研 制 的 专 业 科 研 机 构 创 建 于 1958 年, 前 身 是 中 国 科 学 院 西 北 计 算 技 术 研 究 所 经 过 四 十 多 年 的 建 设, 我 所 已 发 展 成 我 国 航 空 工 业 机 载 计 算 机 发 展 中 心 航 空 软 件 开 发 中 心 计 算 机 软 件 西 安 测 评 中 心 航 空 专 用 集 成 电 路 设 计 中 心 机 载 弹 载 计 算 机 航 空 科 技 重 点 实 验 室 依 托 中 国 航 空 工 业 集 团 公 司 第 六 三 一 所, 于 1998 年 起 投 资 建 设,2005 年 开 始 试 运 行,2008 年 通 过 预 验 收 2010 年 5 月 起 实 验 室 开 始 正 式 运 行 现 任 重 点 实 验 室 主 任 为 张 亚 棣 研 究 员, 现 任 重 点 实 验 8
室 学 术 委 员 会 主 任 为 李 明 院 士 重 点 实 验 室 设 立 四 个 研 究 方 向, 分 别 为 并 行 处 理 技 术 容 错 技 术 工 程 化 技 术 和 软 件 技 术 四 个 研 究 方 向 分 别 重 点 面 向 机 载 弹 载 计 算 机 中 的 关 键 技 术, 开 展 深 入 探 索 和 研 究 重 点 实 验 室 以 满 足 新 一 代 航 空 器 需 求 为 目 标, 以 更 多 地 将 快 速 发 展 的 计 算 机 技 术 应 用 到 机 载 弹 载 计 算 机 中 的 技 术 手 段, 探 索 研 究 机 载 弹 载 计 算 机 的 新 技 术 新 方 法, 建 立 我 国 先 进 的 机 载 弹 载 计 算 机 研 制 体 系, 形 成 强 大 的 机 载 弹 载 计 算 机 的 研 制 能 力, 促 使 我 国 机 载 弹 载 计 算 机 由 跟 随 型 研 发 向 自 主 创 新 型 研 发 转 变 9
可信软件工程中的逻辑方法研讨会 LEDS2015 10