Your browser does not support JavaScript!
http://iet.metastore.ingenta.com
1887

access icon openaccess Towards a greater reliability of driver/device communication around the system life cycle through a contract-based protocol specification

Vehicle computers, Internet of Things and cyber-physical systems are all examples of electronic devices in which embedded systems require greater flexibility to process different types of applications and communication protocols. High flexibility requires the use of general purpose processors as a solution for configuring and controlling several peripherals. However, this also increases the need for hardware-dependent software. Since this is a highly critical and error-prone component due to the nature of its coding and the surrounding environment, it is essential to support the development and runtime phases through methodologies that can detect violations and errors when accessing devices by monitoring the communication protocol. This approach proposes a technique for monitoring temporal properties in high-level communication protocols between devices and drivers using a contract-based specification mechanism for describing the interface and protocol. From this specification, a monitoring module is synthesised, which can detect violation during the simulation of virtual platforms or execution of hardware platforms. The proposed specification language is a domain-specific language that supports platform-based design and enables the iteractive refinement of communication protocol and temporal property specifications along with platform stepwise implementation. Some experiments have demonstrated the effectiveness of the proposed approach for detecting errors in device drivers and device access violation.

References

    1. 1)
      • 35. Davicom: ‘Dm9000a 16/8 bit ethernet controller with general processor interface – application notes v1.20’. Technical Report DM9000A-AN-V120, Davicom Semiconductor, 2005.
    2. 2)
      • 8. Gajski, D.D., Abdi, S., Gerstlauer, A., et al: ‘Embedded system design: modeling, synthesis and verification’ (Springer Publishing Company, Incorporated, 2009, 1st edn.).
    3. 3)
      • 6. Lettnin, D.: ‘Verification of temporal properties in embedded software’. PhD dissertation, Universität Tübingen, 2009.
    4. 4)
      • 23. Conway, C.L., Edwards, S.A.: ‘NDL: a domain-specific language for device drivers’, 2004, pp. 3036.
    5. 5)
      • 24. Bombieri, N., Fummi, F., Pravadelli, G., et al: ‘Correct-by-construction generation of device drivers based on RTL testbenches’. 2009 Design, Automation & Test in Europe Conf. & Exhibition, 2009, pp. 15001505.
    6. 6)
      • 30. Weggerle, A., Himpel, C., Schmitt, T., et al: ‘Transaction based device driver development’. MIPRO, 2011, pp. 195199. Available at http://dblp.unitrier.de/db/conf/mipro/mipro2011.htmlWeggerleHSS11.
    7. 7)
      • 15. Pike, L., Niller, S., Wegmann, N.: ‘Runtime verification for ultra-critical systems’. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2012 (LNCS, 7186), no. Rv, pp. 310324.
    8. 8)
      • 28. Ganapathy, V., Balakrishnan, A., Swift, M.M., et al: ‘Microdrivers: a new architecture for device drivers’. HotOS, 2007. Available at http://dblp.unitrier.de/db/conf/hotos/hotos2007.htmlGanapathyBSJ07.
    9. 9)
      • 29. Herder, J.N., Bos, H., Gras, B., et al: ‘Failure resilience for device drivers’. Proc. of the 37th Annual IEEE/IFIP Int. Conf. on Dependable Systems and Networks, ser. DSN ’07, Washington, DC, USA, 2007, pp. 4150. Available at http://dx.doi.org/10.1109/DSN.2007.46.
    10. 10)
      • 7. Foster, H.D.: ‘Why the design productivity gap never happened’. Proc. of the Int. Conf. on Computer-Aided Design, ser. ICCAD ’13, Piscataway, NJ, USA, 2013, pp. 581584. Available at http://dl.acm.org/citation.cfm?id=2561828.2561943.
    11. 11)
      • 9. Macieira, R., Lisboa, E., Barros, E.: ‘Device driver generation and checking approach’. Brazilian Symp. on Computing System Engineering (SBESC), 2011, November 2011, pp. 7277.
    12. 12)
      • 36. Gastin, P., Oddoux, D.: ‘Fast LTL to buchi automata translation’, in Berry, G., Comon, H., Finkel, A. (Eds.): ‘Computer aided verification’, ser. Lecture Notes in Computer Science (Springer Berlin Heidelberg, 2001), vol. 2102, pp. 5365.
    13. 13)
      • 18. Villarraga, C., Schmidt, B., Bao, B., et al: ‘Software in a hardware view: new models for hw-dependent software in soc verification and test’. IEEE Int. Test Conf. (ITC), 2014, October 2014, pp. 19.
    14. 14)
      • 11. Baier, C., Katoen, J.-P.: ‘Principles of model checking (representation and mind series)’ (The MIT Press, 2008).
    15. 15)
      • 13. Behrend, J., Lettnin, D., Heckeler, P., et al: ‘Scalable hybrid verification for embedded software’. DATE, 2011, pp. 179184. Available at http://dblp.unitrier.de/db/conf/date/date2011.htmlBehrendLHRKR11.
    16. 16)
      • 37. ‘The tdevc project’, 2017. Available at http://www.cin.ufpe.br/~rmm2/tdevc.
    17. 17)
      • 19. Reinbacher, T., Brauer, J., Horauer, M., et al: ‘Runtime verification of microcontroller binary code’, Sci. Comput. Program., 2012, 80, Part A, pp. 109129, special section on foundations of coordination languages and software architectures (selected papers from FOCLASAâ10), Special section – Brazilian Symposium on Programming Languages (SBLP 2010) and Special section on formal methods for industrial critical systems (Selected papers from FMICSâ11).
    18. 18)
      • 16. Zhi-bing, W., Chang-yun, L.I., Sheng-long, H.U., et al: ‘A framework on runtime verification for software behavior’, 2012.
    19. 19)
      • 32. Damm, W., Hungar, H., Josko, B., et al: ‘Using contract-based component specifications for virtual integration testing and architecture design’. Design, Automation & Test in Europe Conf. & Exhibition (DATE), 2011, 2011, pp. 16.
    20. 20)
      • 25. Lisboa, E., Silva, L., Chaves, I., et al: ‘A design flow based on a domain specific language to concurrent development of device drivers and device controller simulation models’. Proc. of the 12th Int. Workshop on Software and Compilers for Embedded Systems, ser. SCOPES ‘09, New York, NY, USA, 2009, pp. 5360. Available at http://dl.acm.org/citation.cfm?id=1543820.1543830.
    21. 21)
      • 4. Sangiovanni-Vincentelli, A.L., Damm, W., Passerone, R.: ‘Taming dr. frankenstein: contract-based design for cyber-physical systems’, Eur. J. Control, 2012, 18, (3), pp. 217238. Available at http://dx.doi.org/10.3166/ejc.18.217-238.
    22. 22)
      • 22. Zhang, Q., Zhu, M., Chen, S.: ‘Automatic generation of device drivers’, ACM SIGPLAN Notices, 2003, 38, (6), pp. 6069. Available at http://portal.acm.org/citation.cfm?id=885638.885649.
    23. 23)
      • 26. Ryzhyk, L., Chubb, P., Kuz, I., et al: ‘Automatic device driver synthesis with termite’. Proc. of the ACM SIGOPS 22Nd Symp. on Operating Systems Principles, ser. SOSP ‘09, New York, NY, USA, 2009, pp. 7386. Available at http://doi.acm.org/10.1145/1629575.1629583.
    24. 24)
      • 1. Ecker, W., Mueller, W., Domer, R.: ‘Hardware-depended software: principles and practice’ (2009).
    25. 25)
      • 2. Reveillere, L., Merillon, F., Consel, C., et al: ‘A DSL approach to improve productivity and safety in device drivers development’. Proc. ASE 2000. Fifteenth IEEE Int. Conf. on Automated Software Engineering, 2000, pp. 101109.
    26. 26)
      • 27. Acquaviva, A., Bombieri, N., Fummi, F., et al: ‘Semi-automatic generation of device drivers for rapid embedded platform development’, IEEE Trans. CAD of Integr. Circuits Syst., 2013, 32, (9), pp. 12931306. Available at http://dblp.unitrier.de/db/journals/tcad/tcad32.htmlAcquavivaBFV13.
    27. 27)
      • 14. Balasubramanian, D., Lowry, M., Corina, P.: ‘Rapid property specification and checking for model-based formalisms’, 2011, pp. 121127.
    28. 28)
      • 20. Amani, S., Chubb, P., Donaldson, A., et al: ‘Automatic verification of active device drivers’, ACM Oper. Syst. Rev., 2014, 48, (1).
    29. 29)
      • 10. Macieira, R., Barros, E., Ascendina, C.: ‘Towards more reliable embedded systems through a mechanism for monitoring driver devices communication’. 15th Int. Symp. on Quality Electronic Design (ISQED), 2014, March 2014, pp. 420427.
    30. 30)
      • 31. Kadav, A., Renzelmann, M.J., Swift, M.M.: ‘Tolerating hardware device failures in software’. Proc. of the ACM SIGOPS 22Nd Symp. on Operating Systems Principles, ser. SOSP ’09, New York, NY, USA, 2009, pp. 5972. Available at http://doi.acm.org/10.1145/1629575.1629582.
    31. 31)
      • 21. Katayama, T., Saisho, K., Fukuda, A.: ‘Prototype of the device driver generation system for unix-like operating systems’. Proc. Int. Symp. on Principles of Software Evolution, 2000, 2000, pp. 302310.
    32. 32)
      • 5. ‘International technology roadmap for semiconductors ITRS’, 2007. Available at http://www.itrs.net/.
    33. 33)
      • 33. Ferrante, O., Passerone, R., Ferrari, A., et al: ‘Bcl: a compositional contract language for embedded systems’. Emerging Technology and Factory Automation (ETFA), 2014 IEEE, September 2014, pp. 16.
    34. 34)
      • 34. Davicom: ‘Dm9000a ethernet controller with general processor interface – datasheet’. Technical Report DM9000A-17-DS-F01, Davicom Semiconductor, 2006.
    35. 35)
      • 3. Renzelmann, M.J., Kadav, A., Swift, M.M.: ‘Sym-Drive: testing drivers without devices’. Osdi'12, 2012, pp. 279292.
    36. 36)
      • 12. Lettnin, D., Nalla, P., Behrend, J., et al: ‘Semiformal verification of temporal properties in automotive hardware dependent software’. Design, Automation Test in Europe Conf. Exhibition, 2009, DATE ‘09, April 2009, pp. 12141217.
    37. 37)
      • 17. Behrend, J., Gruenhage, A., Schroeder, D., et al: ‘Optimized hybrid verification of embedded software’. Test Workshop – LATW, 2014 15th Latin American, March 2014, pp. 16.
http://iet.metastore.ingenta.com/content/journals/10.1049/iet-cps.2017.0001
Loading

Related content

content/journals/10.1049/iet-cps.2017.0001
pub_keyword,iet_inspecKeyword,pub_concept
6
6
Loading
This is a required field
Please enter a valid email address