Formal Model-Based Synthesis of Application-Specific Static RTOS
Formal Model-Based Synthesis of Application-Specific Static RTOS
复制标题
基于形式模型的特定应用静态 RTOS 的综合
DOI：
10.1145/3015777
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
O. Roux
中科院分区：
文献类型：
--
作者：
Tigori Kabland Toussaint Gautier;Jean;Sébastien Faucou;O. Roux
在嵌入式系统中，根据应用程序的要求对实时操作系统（RTOS）的代码进行专门化，允许从二进制程序中删除未使用的服务和其他死代码源。典型的专门化过程基于预编译器宏和构建脚本的混合，这两者都是已知的错误源。在这篇文章中，我们提出了一种新的基于模型的方法来设计特定于应用程序的RTOS。从描述RTOS和应用程序需求的有限状态模型开始，自动计算应用程序实际使用的RTOS代码中的块集。此集合用于构建特定于应用程序的RTOS模型。该模型被输入到代码生成器中，以生成特定于应用程序的RTOS的源代码。它也被用来进行基于模型的验证和确认，包括形式化的验证，专门化过程没有引入不需要的行为或抑制预期的。为了证明这种方法的可行性，它适用于专门的蹦床，AUTOSAR OS标准的开源实现，从汽车领域的工业案例研究。
In an embedded system, the specialization of the code of the real-time operating system (RTOS) according to the requirements of the application allows one to remove unused services and other sources of dead code from the binary program. The typical specialization process is based on a mix of precompiler macros and build scripts, both of which are known for being sources of errors. In this article, we present a new model-based approach to the design of application-specific RTOS. Starting with finite state models describing the RTOS and the application requirements, the set of blocks in the RTOS code actually used by the application is automatically computed. This set is used to build an application-specific RTOS model. This model is fed into a code generator to produce the source code of an application-specific RTOS. It is also used to carry on model-based validations and verifications, including the formal verification that the specialization process did not introduce unwanted behaviors or suppress expected ones. To demonstrate the feasibility of this approach, it is applied to specialize Trampoline, an open-source implementation of the AUTOSAR OS standard, to an industrial case study from the automotive domain.