Assertion-based verification of RTOS properties

Author

Oliveira, Marcio F S ; Zabel, Henning ; Mueller, Wolfgang

Author_Institution

C-Lab., Univ. of Paderborn, Paderborn, Germany

fYear

2010

fDate

8-12 March 2010

Firstpage

630

Lastpage

633

Abstract

Today, mobile and embedded real time systems have to cope with the migration and allocation of multiple software tasks running on top of a real time operating system (RTOS) residing on one or several processors. For scaling of each task set and processor configuration, instruction set simulation and worst case timing analysis are typically applied. This paper presents a complementary approach for the verification of RTOS properties based on an abstract RTOS-Model in SystemC. We apply IEEE P1850 PSL for which we present an approach and first experiences for the assertion-based verification of RTOS properties.

Keywords

embedded systems; instruction sets; operating systems (computers); program verification; specification languages; task analysis; IEEE P1850 PSL; RTOS property; SystemC; abstract RTOS model; assertion-based verification; embedded real time systems; instruction set simulation; multiple software task allocation; property specification language; real time operating system; worst case timing analysis; Analytical models; Embedded software; Hardware; Operating systems; Performance analysis; Processor scheduling; Real time systems; Software performance; Software systems; Timing; PSL; real-time operating systems; verification;

fLanguage

English

Publisher

ieee

Conference_Titel

Design, Automation & Test in Europe Conference & Exhibition (DATE), 2010

Conference_Location

Dresden

ISSN

1530-1591

Print_ISBN

978-1-4244-7054-9

Type

conf

DOI

10.1109/DATE.2010.5457130

Filename

5457130