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