Implementations of high-level modeling languages that integrate high-performance verifiers

集成高性能验证器的高级建模语言的实现

• 批准号: 23300011
• 负责人: UEDA Kazunori
• 金额: $ 12.9万
• 依托单位: Waseda University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2011
• 资助国家: 日本
• 起止时间: 2011-04-01 至 2014-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-23300011/
• 关键词: 高水準モデリング言語; 言語処理系; モデル検査; ハイブリッドシステム; 並列処理; ハイプリッドシステム

Modeling and verification technologies of natural, symbolic and cyber-physical systems are becoming increasingly important. The aim of this research was to demonstrate the viability of high-level modeling languages based on mathematical notions such as graphs, sets, equations and inequations whose generality goes far beyond Computer Science. To achieve this goal, we constructed two publicly available language implementations that integrate runtime systems and verifiers. One of them is an implementation of the graph rewriting language LMNtal, which has now evolved into a parallel model checker with hypergraph rewriting capabilities; the other is an implementation of the hybrid constraint language HydLa, which has evolved into a non-deterministic symbolic execution system for hybrid systems with uncertainties.

自然、符号和网络物理系统的建模和验证技术变得越来越重要。 这项研究的目的是证明基于图形、集合、方程和不等式等数学概念的高级建模语言的可行性，其通用性远远超出了计算机科学的范围。 为了实现这一目标，我们构建了两种集成运行时系统和验证器的公开可用的语言实现。 其中之一是图重写语言 LMNtal 的实现，该语言现已发展成为具有超图重写功能的并行模型检查器；另一个是混合约束语言HydLa的实现，它已经发展成为一种针对具有不确定性的混合系统的非确定性符号执行系统。

项目成果

Interval-Based Projection Method for Under-Constrained Numerical Systems

欠约束数值系统的基于区间的投影方法

• DOI: 10.1007/s10601-012-9126-y
• 发表时间: 2012
• 期刊: Constraints Journal
• 作者: 石井大輔;Alexandre Goldsztejn;Christophe Jermann
• 通讯作者: Christophe Jermann

An Execution Algorithm for the Hybrid System Modeling Language HydLa

混合系统建模语言HydLa的执行算法

• DOI: 10.11309/jssst.28.3_167
• 发表时间: 2011
• 期刊: Computer Software
• 作者: 渋谷俊;高田賢士郎;細部博史;上田和紀
• 通讯作者: 上田和紀

ハイブリッド制約言語プログラムのハイブリッドオートマトンへの変換アルゴリズム

将混合约束语言程序转换为混合自动机的算法

• 发表时间: 2012
• 作者: 竹口輝;和田亮;松本翔太;細部博史;上田和紀
• 通讯作者: 上田和紀

LMNtal実行時処理系SLIMにおけるグラフ構造探索の計算量改善

提高LMNtal运行时处理系统SLIM中图结构搜索的计算复杂度

• 作者: 高野 芳彰;鈴木 隼人;千葉 諒太郎;佐野 健太郎;山本 悟;菱木 知郎;正木 仁;青山 龍一，上田 和紀
• 通讯作者: 青山 龍一，上田 和紀

Concurrent Objects and Beyond (COB 2012), G. Agha et al. (eds.) （査読有）

并发对象及超越 (COB 2012)，G. Agha 等人（编辑）（同行评审）

• 发表时间: 2013
• 作者: 信夫 裕貴;上田 和紀;Kazunori Ueda et al.;Kazunori Ueda;Kazunori Ueda
• 通讯作者: Kazunori Ueda