• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>RSTI >Compilation modulaire d'un langage synchrone
【24h】

Compilation modulaire d'un langage synchrone

机译：同步语言的模块化编译

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Dans cet article, nous étudions la compilation modulaire de programmes synchrones impératifs. Nous nous appuyons sur des méthodes formelles pour compiler et valider les applications spécifiées. Nous avons défini et implémenté un langage dédié (LE) et sa sémantique équationnelle qui permet la compilation modulaire des programmes vers différentes cibles logicielles et matérielles (code C, code Vhdl, synthétiseurs fpga, format d'entrée d'outils de vérification...). Nous montrons que cette sémantique est correcte et nous introduisons un algorithme pour vérifier la causalité qui respecte notre approche modulaire. En nous appuyant sur cette approche formelle, nous avons réalisé une boîte à outils pour compiler et vérifier des applications réactives synchrones.%abstract. In this paper, we study the modular compilation of imperative synchronous programs. We rely on a formal framework well suited to perform compilation and formal validation of systems. In practice, we design and implement a special purpose language (LE) and its execution equational semantics that allows the modular compilation of programs into software and hardware targets (C code, Vhdl code, FPGA synthesis, Verification tools). We show the correctness of this semantics, and we introduce a new algorithm to check program causality with respect to our modular approach. Relying in this formal approach, we defined a toolkit dedicated to the compilation and the verification of reactive applications.
机译：在本文中，我们研究命令式同步程序的模块化编译。我们依靠正式方法来编译和验证指定的应用程序。我们已经定义并实现了一种专用语言（LE）及其等式语义，它允许将程序模块化编译为不同的软件和硬件目标（C代码，Vhdl代码，fpga合成器，验证工具的输入格式... ）。我们证明了这种语义是正确的，并且我们引入了一种算法来验证因果关系，该因果关系遵循我们的模块化方法。使用这种正式方法，我们创建了一个工具箱来编译和验证同步反应式应用程序。在本文中，我们研究命令式同步程序的模块化编译。我们依赖于非常适合执行系统的编译和形式验证的正式框架。在实践中，我们设计和实现一种特殊目的的语言（LE）及其执行方程式语义，该语义允许将程序模块化编译为软件和硬件目标（C代码，Vhdl代码，FPGA综合，验证工具）。我们展示了这种语义的正确性，并针对我们的模块化方法引入了一种新的算法来检查程序的因果关系。依靠这种形式化方法，我们定义了一个专用于反应性应用程序的编译和验证的工具包。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号