Submitted to ISEC 2024.
Verification tools for cyber-physical systems (CPS) often have their own input specification language based on formal models of CPS. This requires tool users to have acquaintance to formal models and thus poses a barrier for new users to get introduced to the verification technology. To address this concern, Verse is a recent Python library that aims to make modeling and verification of CPS more accessible. This library does not require the users to have prior knowledge of formal models of CPS. In this paper, we study the Verse library and its capabilities through two case studies: one in vehicle control and the other in robotics, demonstrating the differences from conventional CPS modeling.
Our source code for ACC can be found here. We see that our control strategy is unsafe. Additionally, we provide some plots.
- For the initial condition:
-
$x = 5$ ,$y = 0$ ,$vx = 28$ ,$ax = 0$ for the ego; -
$x = 15$ ,$y = 0$ ,$vx = 28$ ,$ax = 0$ for the lead;
we plot y vs. x:
and x vs. t:
- For the initial condition range:
-
$x \in [0,5]$ ,$y = 0$ ,$vx \in [0,15]$ ,$ax = 0$ for the ego; -
$x \in [7.5,20]$ ,$y = 0$ ,$vx = 28$ ,$ax = 0$ for the lead;
we plot y vs. x:
and x vs. t:
