Home   Research Publications Members Related Software
IndexBrowse   BibliographiesMy selection
 Search: in   (word length ≥ 3)
      Login
Publication no #564   Download bibtex file Type :   Html | Bib | Both
Add to my selection
IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems

Ivan Ruchkin, Joshua Sunshine, Grant Iraci, Bradley Schmerl and David Garlan.


In 22nd International Symposium on Formal Methods (FM2018), Oxford, UK, 15-17 July 2018. Appendices.

Online links: PDF

Abstract
Design and verification of modern systems requires diverse models, which often come from a variety of disciplines, and it is challenging to manage their heterogeneity – especially in the case of cyber-physical systems. To check consistency between models, recent approaches map these models to flexible static abstractions, such as architectural views. This model integration approach, however, comes at a cost of reduced expressiveness because complex behaviors of the models are abstracted away. As a result, it may be impossible to automatically verify important behavioral properties across multiple models, leaving systems vulnerable to subtle bugs. This paper introduces the Integration Property Language (IPL) that improves integration expressiveness using modular verification of properties that depend on detailed behavioral semantics while retaining the ability for static system-wide reasoning. We prove that the verification algorithm is sound and analyze its termination conditions. Furthermore, we perform a case study on a mobile robot to demonstrate IPL is practically useful and evaluate its performance.

Keywords: Cyberphysical Systems, Formal Methods, Model Checking.  
@InProceedings{Ruchkin/2018/IPL,
      AUTHOR = {Ruchkin, Ivan and Sunshine, Joshua and Iraci, Grant and Schmerl, Bradley and Garlan, David},
      TITLE = {IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems},
      YEAR = {2018},
      MONTH = {15-17 July},
      BOOKTITLE = {22nd International Symposium on Formal Methods (FM2018)},
      ADDRESS = {Oxford, UK},
      PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/fm2018-paper-camera-ready-1.pdf},
      ABSTRACT = {Design and verification of modern systems requires diverse models, which often come from a variety of disciplines, and it is challenging to manage their heterogeneity – especially in the case of cyber-physical systems. To check consistency between models, recent approaches map these models to flexible static abstractions, such as architectural views. This model integration approach, however, comes at a cost of reduced expressiveness because complex behaviors of the models are abstracted away. As a result, it may be impossible to automatically verify important behavioral properties across multiple models, leaving systems vulnerable to subtle bugs. This paper introduces the Integration Property Language (IPL) that improves integration expressiveness using modular verification of properties that depend on detailed behavioral semantics while retaining the ability for static system-wide reasoning. We prove that the verification algorithm is sound and analyze its termination conditions. Furthermore, we perform a case study on a mobile robot to demonstrate IPL is practically useful and evaluate its performance.},
      NOTE = {Appendices},
      KEYWORDS = {Cyberphysical Systems, Formal Methods, Model Checking}
}
    Created: 2018-01-23 09:19:45     Modified: 2018-07-05 17:46:12
Feedback: ABLE Webmaster
Last modified: Sat October 12 2019 16:15:32
        BibAdmin