Given the broad scale of distribution and complexity of today's system, an exhaustive model-checking algorithm is computationally costly and testing is not exhaustive enough. Runtime Verification on the other hand analyzes a developing execution, be it online or offline, of the system in order to check for the health of the system with respect to some specification. Runtime verification of distributed systems with respect to temporal specification is both critical as well as a challenging task. It is critical because it ensures the reliability of the system by detecting violations of system requirements. To guarantee the lack of violations one has to analyze every possible ordering of system events which makes it computationally expensive and hence challenging. In this dissertation, we focus on a partially synchronous distributed system, where the various components of the distributed system do not share a common global clock and a clock synchronization algorithm limits the maximum clock skew among processes to a constant. Following listed are the main contributions of this dissertation,• We introduce two monitoring techniques where the specification in the linear temporal logic (LTL) is either represented by a deterministic finite automaton, or, we use a progression-based formula re-witting technique to reduce the distributed runtime verification problem to an SMT problem.• We introduce a progression-based formula rewriting scheme for monitoring metric temporal logic (MTL) specifications which employ SMT-solving techniques with probabilistic guarantees. • We introduce an (offline) SMT-based monitor synthesis algorithm, which results in minimizing the size of monitoring messages for an automata-based synchronous monitoring algorithm that copes with up to t crash monitor failures. • We extend the stream-based specification language LOLA for monitoring partially-synchronous systems and develop an (online) SMT-based decentralized monitoring technique for the same. • All of our techniques have been tested by both extensive synthetic experiments and real-life case studies, such as a distributed database, Cassandra; an Internet-of-Things dataset of an house, Orange4Home; an Ethereum-based smart contracts; Industrial Control Systems (ICS), Secure Water Treatment (SWaT), etc.
Read
