Developing Embedded Systems from Formal Specifications Written in Temporal Logic

Developing Embedded Systems from Formal Specifications Written in Temporal Logic
复制标题

根据时态逻辑编写的形式规范开发嵌入式系统

DOI：
10.1007/978-1-4614-3363-7_13
复制
发表时间：
2013
期刊：
Proceedings of the Third International Conference on Trends in Information, Telecommunication and Computing, Lecture Notes in Electrical Engineering
影响因子：
--
通讯作者：
Naoki Yonezaki
Naoki Yonezaki
中科院分区：
--
文献类型：
--
作者：
Shigeki Hagihara;Takahiro Arai;Masaya Shimakawa;Naoki Yonezaki

文献摘要

相似文献

我们提出了一个半自动的方法，用于开发嵌入式系统，使用程序代码提取的形式规格书中的时序逻辑。该方法包括以下四个步骤。(1)为一个系统写一个正式的规范。(2)细化规格以适应硬件的结构和功能。(3)从细化的规范中获得表示程序的转换系统。(4)将程序代码分配给规范中使用的原子命题，并将转换系统转换为程序。作为一个案例研究，以证明所提出的方法是实用的，我们生成一个程序，控制机器人作为一个线跟踪器。
We propose a semi-automatic method for developing embedded systems using program code extraction from formal specifications written in temporal logic. This method consists of the following four steps. (1) Write a formal specification for a system. (2) Refine the specification to adapt to the structure and function of the hardware. (3) Obtain a transition system representing a program from the refined specification. (4) Assign program codes to atomic propositions used in the specification, and convert the transition system to the program. As a case study to demonstrate that the proposed method is practical, we generate a program which controls a robot as a line tracer.