Extended abstract: formal verification of architectural patterns in support of dependable distributed systems

摘要

Building robust, secure distributed systems in the presence of transient faults, node failures, and changes in network topology poses a multitude of challenges. To meet current engineering challenges such as pervasive and ubiquitous computing, one must adopt model-driven approaches to build distributed applications. We propose the synchronous paradigm for component integration and coordination: developers use an abstraction that respects the synchrony hypothesis, i.e., each external event is processed by the system completely before the arrival of the next event. Based on the synchronous model, the Secure Operations Language (SOL) is designed as a verifiable language for the integration of high assurance systems.