A unified, declarative programming-based solution to system diagnosis
STRANDS is a declarative programming-based framework for modeling, verifying and debugging a variety of types of systems -- particularly distributed systems -- allowing for static analysis of the system specification and runtime analysis of the system implementation.
STRANDS relies on Network Datalog (NDlog) for system modeling and programming. NDlog is a declarative programming language for network protocols, extending the classical query language Datalog.Programming Logic
The user could use our Hoare-style programming logic developed for NDlog to specify and prove desirable properties about distributed systems. The proof can be performed with proof assistants (e.g., Coq)
Symbolic Execution
The user could specify and verify properties of distributed systems automatically using our static analyser, based on symbolic execution over declarative programs of network applications.
Compressed Provenance
The user could use the compressed provenance to record runtime system execution in a storage-efficient manner. This allows for future querying of the execution history during debugging.
Architecture
