SCIENCE CHINA Information Sciences, Volume 61, Issue 5: 052102(2018) https://doi.org/10.1007/s11432-016-9039-4

## autoC: an efficient translator for model checking deterministic scheduler based OSEK/VDX applications

• AcceptedFeb 20, 2017
• PublishedAug 11, 2017
Share
Rating

### Abstract

The OSEK/VDX automotive OS standard has been widely adopted by many automobile manufacturers, such as BMW and TOYOTA, as the basis for designing and implementing a vehicle-mounted OS.With the increasing functionalities in vehicles, more and more multi-task applications are developed based on the OSEK/VDX OS.Currently, ensuring the reliability of the developed applications is becoming a challenge for developers.As to ensure the reliability of OSEK/VDX applications, model checking as a potential solution has attracted great attention in the automotive industry.However, existing model checkers are often unable to verify a large-scale OSEK/VDX application that consists of many tasks, since the corresponding application model too complex.To make existing model checkers more scalable in verifying large-scale OSEK/VDX applications, we describe a software tool named autoC to tackle this problem by automatically translating a multi-task OSEK/VDX application into an equivalent sequential model.We conducted a series of experiments to evaluate the efficiency of autoC.The experimental results show that autoC is not only capable of efficiently sequentializing OSEK/VDX applications, but also of improving the scalability and efficiency of existing model checkers in verifying large-scale OSEK/VDX applications.

### Acknowledgment

This work was supported by National Natural Science Foundation of China (Grant Nos. 61602224, 61472240) and Fundamental Research Funds for the Central Universities (Grant Nos. lzujbky-2016-142, lzujbky-2016-k07).

### References

[1] Lemieux J. Programming in the OSEK/VDX Environment. New York: CMP Media, Inc., 2011. Google Scholar

[2] Clarke E M, Emerson E A, Sifakis J. Model checking: algorithmic verification and debugging. Commun ACM, 2009, 152: 74--84. Google Scholar

[3] Clarke E M, Grumberg O, Long D E. Model checking and abstraction. ACM Trans Program Lang Syst, 1994, 16: 1512-1542 CrossRef Google Scholar

[4] Pu F, Zhang W H. Combining search space partition and abstraction for LTL model checking. Sci China Ser F-Inf Sci, 2007, 50: 793-810 CrossRef Google Scholar

[5] Holzmann G J. The Spin Model Checker: Primer and Reference Manual. Boston: Lucent Technologies Inc., 2003. Google Scholar

[6] Morse J, Ramalho M, Cordeiro L, et al. ESBMC 1.22. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2014. 405--407. Google Scholar

[7] Cohen E, Dahlweid M, Hillebrand M, et al. VCC: a practical system for verifying concurrent C. In: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics. Berlin: Springer, 2009. 23--42. Google Scholar

[8] Cordeiro L, Fischer B. Verifying multi-threaded software using SMT-based context-bounded model checking. In: Proceedings of the 33rd International Conference on Software Engineering, Waikiki, 2011. 331--340. Google Scholar

[9] Cimatti A, Micheli A, Narasamdya I, et al. Verifying SystemC: a software model checking approach. In: Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, Lugano, 2010. 51--60. Google Scholar

[10] Zhang H T, Aoki T, Chiba Y. A spin-based approach for checking OSEK/VDX applications. In: Proceedings of the 3rd International Workshop Formal Techniques for Safety-Critical Systems (FTSCS), Paris, 2014. 239--255. Google Scholar

[11] Waszniowski L, Hanzálek Z. Formal verification of multitasking applications based on timed automata model. Real-Time Syst, 2008, 38: 39-65 CrossRef Google Scholar

[12] Clarke E M, Klieber W, Novacek M, et al. Model checking and the state explosion problem. In: Tools for Practical Software Verification. Berlin: Springer, 2012. 1--30. Google Scholar

[13] Zhang H T, Aoki T, Chiba Y. Yes You can use your model checker to verify OSEK/VDX applications. In: Proceedings of the 8th International Conference on Software Testing, Verification and Validation, Graz, 2015. 1--10. Google Scholar

[14] Campana D, Cimatti A, Narasamdya I, et al. An analytic evaluation of SystemC encodings in Promela. In: Proceedings of the 18th International SPIN Conference on Model Checking Software, Snowbird, 2011. 90--107. Google Scholar

[15] Inverso O, Tomasco E, Fischer B, et al. Lazy-CSeq: a lazy sequentialization tool for C. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Grenoble, 2014. 398--401. Google Scholar

[16] IEEE Standard for Information Technology. Portable operating system interface (POSIX) base specifications. Issue 7. http://standards.ieee.org/reading/ieee/interp/1003.1-2008.html. Google Scholar

[17] Burns A, Wellings A. Real-Time Systems and Programming Languages. 4th ed. New York: Addison Wesley Longmain, 2009. Google Scholar

[18] George C N, Scott M, Shree P, et al. CIL: intermediate language and tools for analysis and transformation of C programs. In: Proceedings of the 11th International Conference on Compiler Construction. London: Springer, 2002. 213--228. Google Scholar

[19] Clarke E, Kroening D, Lerda F. A tool for checking ANSI-C programings. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2004. 168--176. Google Scholar

[20] Yang Z J, Wang C, Gupta A, et al. Model checking sequential software programs via mixed symbolic analysis. ACM Trans Design Autom Electron Syst, 2009, 14: 1--26. Google Scholar

[21] Armin B, Clarke E M, Zhu Y S. Bounded model checking. Adv Comput, 2003, 58: 117--148. Google Scholar

[22] Tian C, Duan Z H. Detecting spurious counterexamples efficiently in abstract model checking. In: Proceedings of the 35th International Conference on Software Engineering, San Francisco, 2013. 202--211. Google Scholar

[23] Tian C, Duan Z, Duan Z. Making CEGAR More Efficient in Software Model Checking. IIEEE Trans Software Eng, 2014, 40: 1206-1223 CrossRef Google Scholar

[24] Basili V R, Selby R W. Comparing the effectiveness of software testing strategies. IEEE Trans Softw Eng, 1987, 13: 1278--1296. Google Scholar

[25] Hoffmann J, Ussath M, Holz T, et al. Slicing droids: program slicing for smali code. In: Proceedings of the 28th Annual ACM Symposium on Applied Computing, Portugal, 2013. 1844--1851. Google Scholar

[26] Chen J, Aoki T. Conformance testing for OSEK/VDX operating system using model checking. In: Proceedings of the 18th Asia-Pacific Software Engineering Conference, Washington, 2011. 274--281. Google Scholar

[27] Choi Y J. Safety analysis of trampoline OS using model checking: an experience report. In: Proceedings of the IEEE 22nd International Symposium on Software Reliability Engineering, Washington, 2011. 200--209. Google Scholar

[28] Huang Y H, Zhao Y X, Zhu L F, et al. Modeling and verifying the code-level OSEK/VDX operating system with CSP. In: Proceedings of the 5th International Symposium on Theoretical Aspects of Software Engineering, Xi'an, 2011. 142--149. Google Scholar

[29] Zhang H T, Aoki T, Lin X H, et al. SMT-based bounded model checking for OSEK/VDX applications. In: Proceedings of the 20th Asia-Pacific Software Engineering Conference, Bangkok, 2013. 307--314. Google Scholar

[30] Liu Z, Joseph M. Specification and verification of fault-tolerance, timing, and scheduling. ACM Trans Program Lang Syst, 1999, 21: 46-89 CrossRef Google Scholar

• Figure 1

(Color online) Structure of OSEK/VDX application.

• Figure 2

(Color online) Structure of OSEK/VDX OS and provided APIs.

• Figure 3

(Color online) Running application.

• Figure 4

(Color online) Scheduling type: non-deterministic scheduler and deterministic scheduler.

• Figure 5

(Color online) Realistic task interleavings in deterministic scheduler based concurrent program.

• Figure 6

(Color online) Running application model in the Spin model checker.

• Figure 7

(Color online) Architecture of autoC.

• Figure 8

• Figure 10

(Color online) Extended directed graph for running application.

• Figure 11

(Color online) C sequential model for running application.

• Table 1   Comparison: Spin based Plain checking method vs. autoC+Spin
 autoC + Spin Spin$^{\tt~plain\,\,checking\,\,~method}$ autoC Spin Benchmark #t #API #s Time Mb Time Mb #s Time Mb Non-preemption 6 11 4652 0.21 17.7 0.18 3.19 36 0 0.02 8 14 25253 0.71 81.1 0.26 3.64 38 0.01 0.04 10 17 103835 2.67 303.2 0.30 4.11 60 0.01 0.09 18 35 – T.O. – 0.60 5.72 99 0.02 0.50 Full-preemption 4 61 20501 0.10 82.5 0.14 2.98 1008 0.11 0.93 6 101 34371 1.12 126.2 0.19 3.34 1624 0.16 1.79 9 161 46990 1.26 138.1 0.29 4.05 2607 0.27 2.78 13 241 – – M.O. 0.45 5.14 3904 0.39 0.75 Mix-preemption 5 101 13541 0.44 54.7 0.18 3.21 1308 0.13 0.75 9 161 – – M.O. 0.30 4.22 2588 0.13 1.71 13 241 – – M.O. 0.45 5.23 3868 0.26 2.56 13 313 – – M.O. 0.41 4.78 390 0.38 0.24 Synchronization 5 14 2443 0.15 11.6 0.18 3.16 134 0.04 0.11 8 23 24159 0.78 86.8 0.26 4.01 230 0.02 0.14 11 32 210841 5.37 612.4 0.42 4.53 322 0.02 0.02 12 42 382329 9.62 998.3 0.45 5.11 358 0.03 0.19 Shared resource 2 4 13907 0.46 56.5 0.21 3.41 1308 0.13 0.75 9 320 – – M.O. 0.34 4.63 2588 0.26 1.71 13 480 – – M.O. 0.61 5.84 3868 0.38 2.56 12 250 – – M.O. 0.44 4.98 389 0.03 0.24

Citations

• #### 0

Altmetric

Copyright 2020 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有