Virtual Integration of Cyber-Physical Systems by Verification
Panagiotis Manolios and Vasilis Papavasileiou.
In this position paper, we advocate the use of
verification technology to tackle the virtual integration problem
for cyber-physical systems. In particular, we advocate the
use of high-level modeling languages that allow designers to
declaratively specify what properties their architectural models
should have, not how to achieve them. We further advocate
the use of verification technology to analyze such models,
in particular to synthesize concrete architectural models that
certifiably satisfy all properties. We discuss our work in this
direction and outline some of the challenges. Specifically, we
show that virtual integration in the presence of real-time
scheduling constraints leads to problems that cannot be dealt
with in a compositional manner. They can, however, be handled
in a semi-compositional fashion, as we outline in this paper.