Skill-Based Verification of Cyber-Physical Systems

Cyber-physical systems are ubiquitous nowadays. However, as automation increases, modeling and verifying them becomes increasingly difficult due to the inherently complex physical environment. Skill graphs are a means to model complex cyber-physical systems (e.g., vehicle automation systems) by distributing complex behaviors among skills with interfaces between them. We identified that skill graphs have a high potential to be amenable to scalable verification approaches in the early software development process. In this work, we suggest combining skill graphs with hybrid programs. Hybrid programs constitute a program notation for hybrid systems enabling the verification of cyber-physical systems. We provide the first formalization of skill graphs including a notion of compositionality and propose Skeditor, an integrated framework for modeling and verifying them. Skeditor is coupled with the theorem prover KeYmaera X, which is specialized in the verification of hybrid programs. In an experiment exhibiting the follow mode of a vehicle, we evaluate our skill-based methodology with respect to savings in verification effort and potential to find modeling defects at design time. Compared to non-compositional verification, the initial verification effort needed is reduced by more than 53%.