Compositional verification of embedded software systems
US11977478B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Jul 19, 2022 |
| Grant date | May 7, 2024 |
| Priority date | — |
| Expiry date | Nov 29, 2042 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F11/3696
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A computer-implemented method for static testing a software system that is decomposed into software units connected by interfaces. The method comprises receiving context information for an interface, which includes at least one postcondition for the at least one output variable of a respective first software unit and/or a precondition for the input variable of a respective second software unit; receiving a selection of a third software unit in so that a substitute decomposition appertaining thereto of the software system into the third software unit and a complement of the third software unit is produced, the third software unit and the complement forming the software system and being connected via a substitute interface; selecting, based on the item of context information a postcondition per output variable of the complement; and testing whether the selected postcondition can be forward-propagated by the third software unit with regard to a formal verification.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.