On Formal Modeling of TOPPERS Embedded Software

Author

Kawabe, Yoshinobu ; Ito, Nobuhiro ; Ishii, Naohiro

Author_Institution

Aichi Inst. of Technol., Toyota, Japan

fYear

2010

fDate

24-26 May 2010

Firstpage

93

Lastpage

100

Abstract

Today embedded software is widely used. As the complexity of embedded systems grows, the number of tasks performed by embedded software is increasing. These tasks must communicate with each other to achieve synchronization. And therefore, the growing complexity of communications is making it increasingly difficult to program and debug these tasks. To confirm the correctness of embedded software, this paper introduces a formal specification language for embedded systems that can deal with their concurrent nature. After formalizing the APIs of an embedded real-time operating system, we demonstrate how to describe and verify embedded software formally.

Keywords

Concurrent computing; Control systems; Embedded software; Embedded system; Formal languages; Formal specifications; Multitasking; Operating systems; Real time systems; Software engineering; TOPPERS real-time operating system; distributed systems; embedded software; formal methods; verification;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering Research, Management and Applications (SERA), 2010 Eighth ACIS International Conference on

Conference_Location

Montreal, QC, Canada

Print_ISBN

978-0-7695-4075-7

Electronic_ISBN

978-1-4244-7337-3

Type

conf

DOI

10.1109/SERA.2010.22

Filename

5489100