Name
Abstract | ||
|---|---|---|
This paper describes ongoing work on a new technique for reducing the cost of assurance of large software systems by building on a verified component platform. From a component architecture description, we automatically derive a formal model of the system and a semantics for the runtime behaviour of generated inter-component communication code. We can prove wellformedness properties of the architecture automatically and provide a framework in which users can reason about their component code and its behaviour. By leveraging the isolation properties and communication guarantees of a formally verified platform, correctness arguments for critical components will be able to be derived independently and composed together to reason about system-level correctness. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1145/2525528.2525535 | PLOS@SOSP |
Field | DocType | Citations |
Architecture,Computer science,Software architecture description,Correctness,Software system,Real-time computing,Semantics | Conference | 1 |
PageRank | References | Authors |
0.35 | 19 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Matthew Fernandez | 1 | 15 | 2.39 |
| I. Kuz | 2 | 48 | 41.18 |
| Gerwin Klein | 3 | 1450 | 87.47 |
| June Andronick | 4 | 903 | 42.66 |