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

  • HTML
    288.8427734375Kb
  • PDF
    3.5471954345703125MB
  • XML
    213.111328125Kb
Loading full text...

Full text loading...

/deliver/fulltext/iet-cps/3/1/IET-CPS.2017.0001.html;jsessionid=79rtt4d8frurm.x-iet-live-01?itemId=%2fcontent%2fjournals%2f10.1049%2fiet-cps.2017.0001&mimeType=html&fmt=ahah

References

    1. 1)
      • 1. Ecker, W., Mueller, W., Domer, R.: ‘Hardware-depended software: principles and practice’ (2009).
    2. 2)
      • 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.
    3. 3)
      • 3. Renzelmann, M.J., Kadav, A., Swift, M.M.: ‘Sym-Drive: testing drivers without devices’. Osdi'12, 2012, pp. 279292.
    4. 4)
      • 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.
    5. 5)
      • 5. ‘International technology roadmap for semiconductors ITRS’, 2007. Available at http://www.itrs.net/.
    6. 6)
      • 6. Lettnin, D.: ‘Verification of temporal properties in embedded software’. PhD dissertation, Universität Tübingen, 2009.
    7. 7)
      • 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.
    8. 8)
      • 8. Gajski, D.D., Abdi, S., Gerstlauer, A., et al: ‘Embedded system design: modeling, synthesis and verification’ (Springer Publishing Company, Incorporated, 2009, 1st edn.).
    9. 9)
      • 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.
    10. 10)
      • 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.
    11. 11)
      • 11. Baier, C., Katoen, J.-P.: ‘Principles of model checking (representation and mind series)’ (The MIT Press, 2008).
    12. 12)
      • 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.
    13. 13)
      • 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.
    14. 14)
      • 14. Balasubramanian, D., Lowry, M., Corina, P.: ‘Rapid property specification and checking for model-based formalisms’, 2011, pp. 121127.
    15. 15)
      • 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.
    16. 16)
      • 16. Zhi-bing, W., Chang-yun, L.I., Sheng-long, H.U., et al: ‘A framework on runtime verification for software behavior’, 2012.
    17. 17)
      • 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.
    18. 18)
      • 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.
    19. 19)
      • 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).
    20. 20)
      • 20. Amani, S., Chubb, P., Donaldson, A., et al: ‘Automatic verification of active device drivers’, ACM Oper. Syst. Rev., 2014, 48, (1).
    21. 21)
      • 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.
    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)
      • 23. Conway, C.L., Edwards, S.A.: ‘NDL: a domain-specific language for device drivers’, 2004, pp. 3036.
    24. 24)
      • 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.
    25. 25)
      • 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.
    26. 26)
      • 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.
    27. 27)
      • 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.
    28. 28)
      • 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.
    29. 29)
      • 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.
    30. 30)
      • 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.
    31. 31)
      • 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.
    32. 32)
      • 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.
    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)
      • 35. Davicom: ‘Dm9000a 16/8 bit ethernet controller with general processor interface – application notes v1.20’. Technical Report DM9000A-AN-V120, Davicom Semiconductor, 2005.
    36. 36)
      • 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.
    37. 37)
      • 37. ‘The tdevc project’, 2017. Available at http://www.cin.ufpe.br/~rmm2/tdevc.
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