Search tips
 This content is not included in your SAE MOBILUS subscription, or you are not logged in.

A Methodology for Increasing the Efficiency and Coverage of Model Checking and its Application to Aerospace Systems

Journal Article
2016-01-2053
ISSN: 1946-3855, e-ISSN: 1946-3901
DOI: https://doi.org/10.4271/2016-01-2053
Published September 20, 2016 by SAE International in United States
A Methodology for Increasing the Efficiency and Coverage of Model Checking and its Application to Aerospace Systems
Sector:
Citation: Ferrante, O., Scholte, E., Pinello, C., Ferrari, A. et al., "A Methodology for Increasing the Efficiency and Coverage of Model Checking and its Application to Aerospace Systems," SAE Int. J. Aerosp. 9(1):140-150, 2016, https://doi.org/10.4271/2016-01-2053.
Language: English

References

  1. Miller , Steven P. and Whalen , Michael W. and Cofer , Darren D. Software model checking takes off, Communications of the ACM 53 2 2010
  2. Clarke E. Model checking Ramesh S. and Sivakumar G. Foundations of Software Technology and Theoretical Computer Science, volume 1346 of Lecture Notes in Computer Science 54 56 Springer Berlin Heidelberg 1997 10.1007/BFb0058022
  3. Clarke E. M. , Emerson E. A. , and Sistla A. P. Automatic verification of finite-state concurrent systems using temporal logic specifications ACM Trans. Program. Lang. Syst. 8 244 263 April 1986
  4. Dutertre B. and Stavridou V. Formal requirements analysis of an avionics control system IEEE Transactions on Software Engineering 23 267 278 1997
  5. Hamilton D. , Covington R. , Kelly J. , Kirkwood C. , Thomas M. , Flora-Holmquist A. R. , Staskauskas M. G. , Miller S. P. , Srivas M. , Cleland G. , and MacKenzie D. Experiences in applying formal methods to the analysis of software and system requirements Proceedings of the 1st Workshop on Industrial-Strength Formal Specification Techniques 30 Washington, DC, USA 1995
  6. Holzmann G. J. The model checker spin IEEE Transactions on Software Engineering 23 279 295 1997
  7. McMillan K. L. Symbolic model checking: an approach to the state explosion problem PhD thesis Pittsburgh, PA, USA 1992
  8. Nuzzo , Pierluigi et al. A contract-based methodology for aircraft electric power system design Access 2 2014 1 25
  9. Henzinger Thomas A. , Pei-Hsin Ho , HowardWong-Toi HYTECH: a model checker for hybrid systems Int J STTT 1997 1 110 122
  10. Kwiatkowska , M. ; Norman , G. ; Parker , D. 2011 PRISM 4.0: Verification of Probabilistic Real-time Systems In Proc. 23rd International Conference on Computer Aided Verification (CAV’11) 6806 585 591 Springer
  11. Owre S . , Rushby J. M. , and Shankar N. PVS: A prototype verification system Kapur D. 11th International Conference on Automated Deduction (CADE) 607 748 752 Saratoga, NY jun 1992 Springer-Verlag
  12. http://www.mathworks.com/products/simulink/
  13. http://www.omg.org/spec/QVT/index.htm
  14. Cavada R. , Cimatti A. , Dorigatti M. , Griggio A. , Mariotti A. , Micheli A. , Mover S. , Roveri M. , Tonetta S. The nuXmv Symbolic Model Checker Computer Aided Verification Lecture Notes in Computer Science 8559 334 342
  15. Ferrante O. , Benvenuti L. , Mangeruca L. , Sofronis C. and Ferrari A. Parallel NuSMV: a NuSMV extension for the verification of complex embedded systems Computer Safety, Reliability, and Security, Lecture Notes in Computer Science 7613 2012 409 416
  16. Mangeruca L. , Ferrante O. , Ferrari A. Formalization and completeness of evolving requirements using Contracts 8th IEEE International Symposium on Industrial Embedded Systems (SIES 2013) 19-21 June 2013 Porto, Portugal
  17. Marazza M. , Ferrante O. , Ferrari A. Automatic Generation of Failure Scenarios for Sytems-on-Chip Real Time Software and Systems ERTS 2014 Tolouse
  18. Ferrante O. , Ferrari A. , Mangeruca L. , Passerone R. , Sofronis C. , D'Angelo M. Monitor-Based Run-Time Contract Verification of Distributed Systems 2014 9th IEEE Symposium on Industrial Embedded Systems Pisa 2014
  19. Ferrante O. , Ferrari A. , Mangeruca L. , Passerone R. , Sofronis C. BCL: a compositional contract language for embedded systems 19th IEEE International Conference on Emerging Technologies and Factory Automation Barcelona 2014
  20. Ferrante O. , Ferrari A. , Marazza M. An algorithm for the incremental generation of high coverage tests suites 19th IEEE European Test Symposium 2014 Paderborn
  21. Carloni M. , Ferrante O. , Ferrari A. , Massaroli G. , Orazzo A. , Petrone I. , Velardi L. Contract-Based Analysis for Verification of Communication-Based Train Control (CBTC) System SAFECOMP 2014 Firenze
  22. Carloni M. , Ferrante O. , Ferrari A. , Massaroli G. , Orazzo A. , Petrone I. , Velardi L. Contract Modeling and Verification with Formal Specs Verifier Tool-Suite - Application to Ansaldo STS Rapid Transit Metro System Use Case SAFECOMP 2015
  23. Ferrante O. , Ferrari A. , Marazza M. Formal Specs Verifier ATG: a Tool for Model-based Generation of High Coverage Test Suites ERTS 2016 Tolouse
  24. Cimatti A. , Clarke M. E. , Giunchiglia E. , Giunchiglia F. , Pistore M. , Roveri M. , Sebastiani R. , and Tacchella A NuSMV 2: An OpenSource Tool for Symbolic Model Checking Proceedings of the 14th International Conference on Computer Aided Verification (CAV '02) Brinksma Ed and Larsen Kim Guldstrand Springer-Verlag London, UK, UK 359 364
  25. Balasubramanian , M. and Bhatnagar , A. and Roy , S. Automatic translation of simulink models into the input language of a model checker US Patent App. 11/545,134 2008 https://www.google.com/patents/US20080086705
  26. http://www.mathworks.com/products/sldesignverifier/?refresh=true
  27. Whalen , M. , Cofer , D. , Miller S. , Krogh , Bruce H. , Storm , W. Integration of Formal Analysis into a Model-based Software Development Process Proceedings of the 12th International Conference on Formal Methods for Industrial Critical Systems 2008 Berlin, Germany
  28. Brayton R. , Mishchenko A. ABC: an academic industrial-strength verification tool Proceedings of the 22nd international conference on Computer Aided Verification (CAV'10) Tayssir Touili , Byron Cook , and Paul Jackson Springer-Verlag Berlin, Heidelberg 24 40 http://dx.doi.org/10.1007/978-3-642-14295-6_5
  29. https://eclipse.org/modeling/emf/
  30. http://www.omg.org/spec/XMI/
  31. Clarke , E. M. , Grumberg O. , Peled D. A. Model Checking 1999 MIT Press
  32. Benveniste A. , Caillaud B. , Ferrari A. , Mangeruca L. , Passerone R. , and Sofronis C. Multiple Viewpoint Contract-Based Specification and Design Formal Methods for Components and Objects Boer Frank S. , Bonsangue Marcello M. , Graf Susanne , and Roever Willem-Paul 5382 Springer-Verlag Berlin

Cited By