| Autor: |
Griffin, Jeremiah, Lesani, Mohsen, Shadab, Narges, Yin, Xizhe |
| Rok vydání: |
2020 |
| Předmět: |
|
| Druh dokumentu: |
Working Paper |
| Popis: |
Distributed systems are critical to reliable and scalable computing; however, they are complicated in nature and prone to bugs. To modularly manage this complexity, network middleware has been traditionally built in layered stacks of components. We present a novel approach to compositional verification of distributed stacks to verify each component based on only the specification of lower components. We present TLC (Temporal Logic of Components), a novel temporal program logic that offers intuitive inference rules for verification of both safety and liveness properties of functional implementations of distributed components. To support compositional reasoning, we define a novel transformation on the assertion language that lowers the specification of a component to be used as a subcomponent. We prove the soundness of TLC and the lowering transformation with respect to the operational semantics for stacks of distributed components. We successfully apply TLC to compose and verify a stack of fundamental distributed components. |
| Databáze: |
arXiv |
| Externí odkaz: |
|
