| Autor: |
César Augusto R. dos Santos, Tom Schrijvers, Amr Hany Saleh, Mike Nicolai |
| Přispěvatelé: |
Huisman, M, Pasareanu, C, Zhan, N |
| Rok vydání: |
2021 |
| Zdroj: |
Formal Methods ISBN: 9783030908690 |
| Popis: |
Generative Engineering is a new paradigm for the development of cyber-physical systems. Rather than developing a single, increasingly more detailed model of a system, multiple architectural variants are computationally generated and evaluated, which would be prohibitively expensive to do by hand. Existing synthesis approaches are geared towards finding one solution fast, but this makes them less effective for generative engineering where we are interested in enumerating many or all solutions. The common approach in generative engineering is to compute a new verification problem per generated architecture, despite all being variants of the same verification problem. This makes the tools unable to exploit commonalities and they end up doing much of the same verification work over and over again. Our work addresses this inefficiency in the synthesis of all correct-by-construction logical architectures of a system with a simple but effective approach. We create only one parameterized verification problem per use case, and, by exploiting the assumption mechanism of SMT solvers, we can very efficiently and incrementally check each generated architecture. Our experimental evaluation demonstrates that this approach is orders of magnitude faster than the typical synthesis approach. ispartof: pages:776-787 ispartof: Springer LNCS vol:13047 pages:776-787 ispartof: Industry Day of Formal Methods 2021 location:Beijing, China date:20 Nov - 26 Nov 2021 status: accepted |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
