| Autor: |
Metzger, Niklas, Schmitt, Sanny, Schwenger, Maximilian |
| Rok vydání: |
2021 |
| Předmět: |
|
| Druh dokumentu: |
Working Paper |
| Popis: |
The verification of cyber-physical systems operating in a safety-critical environment requires formal system models. The validity of the verification hinges on the precision of the model: possible behavior not captured in the model can result in formally verified, but unsafe systems. Yet, manual construction is delicate and error-prone while automatic construction does not scale for large and complex systems. As a remedy, this paper devises an automatic construction algorithm that utilizes information contained in artifacts of the development process: a runtime monitoring specification and recorded test traces. These artifacts incur no additional cost and provide sufficient information so that the construction process scales well for large systems. The algorithm uses a hybrid approach between a top-down and a bottom-up construction which allows for proving the result conservative, while limiting the level of over-approximation. |
| Databáze: |
arXiv |
| Externí odkaz: |
|
