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
- Eelco Scholte - UTC Aerospace Systems ,
- Cong Liu - UTC Aerospace Systems ,
- Orlando Ferrante - United Technologies Research Center ,
- Claudio Pinello - United Technologies Research Center ,
- Alberto Ferrari - United Technologies Research Center ,
- Leonardo Mangeruca - United Technologies Research Center ,
- Christos Sofronis - United Technologies Research Center
Journal Article
2016-01-2053
ISSN: 1946-3855, e-ISSN: 1946-3901
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
- Miller , Steven P. and Whalen , Michael W. and Cofer , Darren D. Software model checking takes off, Communications of the ACM 53 2 2010
- 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
- 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
- Dutertre B. and Stavridou V. Formal requirements analysis of an avionics control system IEEE Transactions on Software Engineering 23 267 278 1997
- 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
- Holzmann G. J. The model checker spin IEEE Transactions on Software Engineering 23 279 295 1997
- McMillan K. L. Symbolic model checking: an approach to the state explosion problem PhD thesis Pittsburgh, PA, USA 1992
- Nuzzo , Pierluigi et al. A contract-based methodology for aircraft electric power system design Access 2 2014 1 25
- Henzinger Thomas A. , Pei-Hsin Ho , HowardWong-Toi HYTECH: a model checker for hybrid systems Int J STTT 1997 1 110 122
- 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
- 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
- http://www.mathworks.com/products/simulink/
- http://www.omg.org/spec/QVT/index.htm
- 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
- 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
- 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
- Marazza M. , Ferrante O. , Ferrari A. Automatic Generation of Failure Scenarios for Sytems-on-Chip Real Time Software and Systems ERTS 2014 Tolouse
- 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
- 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
- Ferrante O. , Ferrari A. , Marazza M. An algorithm for the incremental generation of high coverage tests suites 19th IEEE European Test Symposium 2014 Paderborn
- 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
- 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
- Ferrante O. , Ferrari A. , Marazza M. Formal Specs Verifier ATG: a Tool for Model-based Generation of High Coverage Test Suites ERTS 2016 Tolouse
- 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
- 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
- http://www.mathworks.com/products/sldesignverifier/?refresh=true
- 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
- 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
- https://eclipse.org/modeling/emf/
- http://www.omg.org/spec/XMI/
- Clarke , E. M. , Grumberg O. , Peled D. A. Model Checking 1999 MIT Press
- 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