Formal synthesis of application and platform behaviors of embedded software systems
Formal synthesis of application and platform behaviors of embedded software systems
复制标题
DOI：
10.1007/s10270-013-0342-8
复制
发表时间：
2015-05
影响因子：
2
通讯作者：
Jinhyun Kim;Inhye Kang;Jin-Young Choi;Insup Lee;Sungwon Kang
中科院分区：
文献类型：
--
作者：
Jinhyun Kim;Inhye Kang;Jin-Young Choi;Insup Lee;Sungwon Kang
两个主要的嵌入式软件组件，应用软件和平台软件，即实时操作系统（RTOS），彼此交互以实现系统的功能。然而，它们的行为如此不同，以至于一种行为建模语言不足以对两种行为风格进行建模并不足以推理它们各自行为的特征以及它们的并行行为和交互属性。在本文中，我们提出了一种综合应用软件和 RTOS 行为模型的形式化方法。在这种方法中，每个模型都使用适当的建模语言进行建模，然后组合成系统模型进行分析。此外，本文还提出了一种在功能需求和时序需求方面分析应用软件的一致方法。为了展示该方法的有效性，我们进行了一个案例研究，其中根据时序要求对 ARINC 653 及其应用进行了建模和验证。使用我们的方法，应用软件可以被构建为独立于特定平台的行为模型，并且可以以正式的方式针对各种平台和时序约束进行验证。
Two main embedded software components, application software and platform software, i.e., the real-time operating system (RTOS), interact with each other in order to achieve the functionality of the system. However, they are so different in behaviors that one behavior modeling language is not sufficient to model both styles of behaviors and to reason about the characteristics of their individual behaviors as well as their parallel behavior and interaction properties. In this paper, we present a formal approach to the synthesis of the application software and the RTOS behavior models. In this approach, each of them is modeled with its adequate modeling language and then is composed into a system model for analysis. Moreover, this paper also presents a consistent way of analyzing the application software with respect to both functional requirements and timing requirements. To show the effectiveness of the approach, a case study is conducted, where ARINC 653 and its application are modeled and verified against timing requirements. Using our approach, application software can be constructed as a behavioral model independently from a specific platform and can be verified against various platforms and timing constraints in a formal way.