• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Industrial Informatics, IEEE Transactions on >Toward Correctness in the Specification and Handling of Non-Functional Attributes of High-Integrity Real-Time Embedded Systems
【24h】

Toward Correctness in the Specification and Handling of Non-Functional Attributes of High-Integrity Real-Time Embedded Systems

机译：高完整性实时嵌入式系统非功能属性的规范和处理中的正确性

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

摘要

In high-integrity systems, the focus of the development process is geared to assuring that the assertions made on the system are both correct (i.e., semantically sustainable) and feasible (i.e., true at run time). Some of those assertions take effect in the non-functional domain, that is, in how the system is realized and behaves in time, space and communication during execution; others in the functional domain, and thus concern what outputs the system produces for its inputs. In this paper, we address the problem of achieving correct specification and handling of non-functional attributes, with particular regard to the concurrent structure of the system, the safeness of the interaction protocols engaged in it, and the guarantee that its timing feasibility can be statically verified. Our approach is based on a Model-Driven Engineering methodology, in which correctness can be ensured by construction or verified at a high level of abstraction, while the runtime implementation structure and code are automatically generated. We employ the Ravenscar Computation Model (RCM) and focus, in particular, on aerospace applications, which impose stringent requirements on correctness properties. We discuss an algebraic formalization of our model based on graph theory which we use to prove safe termination in systems compliant with RCM, and show how to use the MAST+ static analyzer to verify the timing aspects. We finally illustrate the results of a prototype tool that was developed for evaluation by major industrial players in the European space industry.
机译：在高完整性系统中，开发过程的重点是确保在系统上作出的断言既正确（即语义上可持续）又可行（即在运行时为真）。其中一些断言在非功能性域中生效，即在系统如何实现以及在执行过程中的时间，空间和通信行为方面起作用。功能领域中的其他产品，因此涉及系统为其输入产生的输出。在本文中，我们解决了实现正确规范和处理非功能属性的问题，尤其是系统的并发结构，所参与交互协议的安全性以及保证其时序可行性的问题。静态验证。我们的方法基于模型驱动工程方法，该方法可以通过构造来确保正确性，也可以在高度抽象的情况下进行验证，同时自动生成运行时实现结构和代码。我们采用Ravenscar计算模型（RCM），并特别关注航空航天应用，这对准确性属性提出了严格要求。我们讨论了基于图论的模型代数形式化，用于证明符合RCM的系统中的安全端接，并展示了如何使用MAST +静态分析器来验证时序方面。我们最后说明了原型工具的结果，该工具是由欧洲航天工业的主要工业参与者开发用于评估的。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号