logo

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

More info
  • ReceivedNov 3, 2016
  • AcceptedFeb 20, 2017
  • PublishedAug 11, 2017

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

    (Color online) CFGs for tasks contask, plustask and minustask.

  • 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

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

京ICP备18024590号-1