Toward Correctness in the Specification and Handling of Non-Functional Attributes of High-Integrity Real-Time Embedded Systems
Toward Correctness in the Specification and Handling of Non-Functional Attributes of High-Integrity Real-Time Embedded Systems
复制标题
DOI：
10.1109/tii.2010.2043741
复制
发表时间：
2010-03
影响因子：
12.3
通讯作者：
D. Cancila;R. Passerone;T. Vardanega;Marco Panunzio
中科院分区：
文献类型：
--
作者：
D. Cancila;R. Passerone;T. Vardanega;Marco Panunzio
在高完整性系统中，开发过程的重点是确保在系统上做出的断言都是正确的（即，语义上可持续）且可行（即，运行时为true）。其中一些断言在非功能域中生效，也就是说，在执行过程中，系统如何在时间，空间和通信中实现和行为;其他断言在功能域中，因此关注系统为其输入产生什么输出。在本文中，我们解决的问题，实现正确的规范和处理的非功能性属性，特别是关于系统的并发结构，安全的交互协议参与其中，并保证其时间的可行性可以静态验证。我们的方法是基于模型驱动的工程方法，其中的正确性可以确保建设或验证在一个高层次的抽象，而运行时的实现结构和代码自动生成。我们采用的拉文斯卡计算模型（RCM）和重点，特别是在航空航天应用，这对正确性的严格要求。我们讨论了我们的模型的代数形式化基于图论，我们用来证明安全终止系统符合RCM，并展示了如何使用MAST+静态分析器来验证的时间方面。最后，我们说明了在欧洲航天工业的主要工业参与者的评估开发的原型工具的结果。
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.