Variational correctness-by-construction
| Autor: | Tobias Runge, Thomas Thüm, Ina Schaefer, Tabea Bordis, Alexander Knüppel |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Correctness
Computer science business.industry Product family 020207 software engineering 02 engineering and technology Design by contract Formal methods Domain (software engineering) Variable (computer science) Software Computer engineering 0202 electrical engineering electronic engineering information engineering Code (cryptography) 020201 artificial intelligence & image processing business |
| Zdroj: | VaMoS |
| Popis: | Nowadays, the requirements for software and therefore also the required complexity is increasing steadily. Consequently, various techniques to handle the growing demand for software variants in one specific domain are used. These techniques often rely on variable code structures to implement a whole product family more efficiently. Variational software is also increasingly used for safety-critical systems, which need to be verified to guarantee their functionality in-field. However, usual verification techniques can not directly be applied to the variable code structures of most techniques. In this paper, we propose variational correctness-by-construction as a methodology to implement variational software extending the correctness-by-construction approach. Correctness-by-construction is an incremental approach to create and verify programs using small tractable refinement steps guided by a specification following the design-by-contract paradigm. Our contribution is threefold. First, we extend the list of refinement rules to enable variability in programs developed with correctness-by-construction. Second, we motivate the need for contract composition of refined method contracts and illustrate how this can be achieved. Third, we implement variational correctness-by-construction in a tool called VarCorC. We successfully conducted two case studies showing the applicability of VarCorC and were able to assess reduced verification costs compared to post-hoc verification as well. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|