Name
Abstract | ||
|---|---|---|
With the growing demands for automotive auxiliary functions, more and more complex applications have been developed based on OSEK/VDX OS. However, how to check the developed applications is becoming a challenge for developers. Although some invaluable formal methods have been proposed to check actual software, these methods cannot be directly employed to check OSEK/VDX applications. In this paper, we describe and develop an approach to check OSEK/VDX applications using SMT-based bounded model checking. We also implement a prototype tool and conduct many experiments on several examples. The experiment results show that our approach can completely check the properties associated with (i) variables, (ii) mutual exclusion, (iii) service API, and (iv) tasks execution sequences of developed applications. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1109/APSEC.2013.49 | Asia-Pacific Software Engineering Conference |
Keywords | Field | DocType |
OSEK/VDX,Bounded Model Checking,SMT | Model checking,Programming language,Computer science,OSEK,Computability,Real-time computing,Software,Formal methods,Mutual exclusion,Operating system,Formal verification,Bounded function | Conference |
ISSN | Citations | PageRank |
1530-1362 | 5 | 0.45 |
References | Authors | |
10 | 6 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Haitao Zhang | 1 | 17 | 2.07 |
| Toshiaki Aoki | 2 | 57 | 16.68 |
| Hsin-Hung Lin | 3 | 50 | 9.30 |
| Min Zhang | 4 | 5 | 0.45 |
| Yuki Chiba | 5 | 35 | 7.46 |
| Kenro Yatake | 6 | 23 | 4.59 |