SHOW publication #564 - ABLE Publications

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.

@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}
}