Using third-party executable components to build control systems poses challenges for verification. This is because the informal behavior descriptions that typically accompany the components often fall short of the needed rigor. Consequently, there is a need to formalize a component contract that is strong enough to help establish system properties and also weak enough to account for all potential component behaviors in the system's context. In this paper, we present a novel approach that allows an analyst to hypothesize a component contract, explore if the component meets the contract, and, if not, have automated support to help repair the contract. Preliminary results show that, in more than 32% of the cases, the repaired contract is logically equivalent to a developer-written one; in a further 63% of cases, it is a distinct, valid, and non-trivial property of the component.
|Original language||English (US)|
|Title of host publication||Proceedings - 2021 36th IEEE/ACM International Conference on Automated Software Engineering, ASE 2021|
|Publisher||Institute of Electrical and Electronics Engineers Inc.|
|Number of pages||3|
|State||Published - 2021|
|Event||36th IEEE/ACM International Conference on Automated Software Engineering, ASE 2021 - Virtual, Online, Australia|
Duration: Nov 15 2021 → Nov 19 2021
|Name||Proceedings - 2021 36th IEEE/ACM International Conference on Automated Software Engineering, ASE 2021|
|Conference||36th IEEE/ACM International Conference on Automated Software Engineering, ASE 2021|
|Period||11/15/21 → 11/19/21|
Bibliographical noteFunding Information:
The research described in this paper has been supported in part by the National Science Foundation under grant 1563920.
© 2021 IEEE.
- Invariant discovery
- Specification repair