Specification, Analysis and Implementation of Architectural Patterns for Dependable Software Systems
Reference: Yau, S. S., Mukhopadhyay, S., Bharadwaj, R. (2005). Proc. 10th IEEE Intl. Workshop on Object-Oriented Real-Time Dependable Systems (WORDS’05). Source file: WORD2005-2.pdf. URL
Summary
The paper presents the Secure Operations Language (SOL) and the agent-based SINS middleware for specifying, analyzing, and deploying architectural patterns that realize non-functional requirements (security, fault tolerance, real-time) of distributed dependable systems. SOL is a synchronous specification language with a precise formal semantics supporting automated analysis (theorem proving, model checking); SINS runs SOL agents on virtual machines distributed over hosts, with encrypted inter-agent messaging via a Secure Agent Control Protocol.
The authors illustrate SOL by formalizing a stack safety policy (a safestack module that constrains illegal pushes/pops) and the Hot Standby and Majority Vote fault-tolerance patterns as SOL modules with observable fail events. They extend SOL with module imports, an implicit fail variable, and middleware notification of module failures — enabling compositional dependability reasoning across heterogeneous deployments.
Key Ideas
- SOL: synchronous language for agent specification with formal semantics.
- SINS middleware runs SOL agents across encrypted VMs.
- Patterns (HotStandby, MajorityVote) as reusable SOL modules.
- Safety policies enforced at the language level.
- Compositional analysis of dependability requirements.
Connections
Conceptual Contribution
- Claim: Dependability (security, fault tolerance, real-time) in distributed systems is best achieved by specifying architectural patterns as formal modules in a synchronous agent language and deploying them on a middleware that enforces the same semantics at runtime.
- Mechanism: SOL is a synchronous language with precise formal semantics amenable to theorem proving and model checking; programs are agents running on SINS virtual machines across hosts, communicating over the Secure Agent Control Protocol. The authors extend SOL with module imports, an implicit
fail variable, and middleware fault notifications, then encode stack-safety, Hot Standby and Majority Vote as reusable SOL modules whose composition preserves dependability guarantees.
- Concepts introduced/used: Secure Operations Language, SINS Middleware, Synchronous Language, Architectural Pattern, Hot Standby, Majority Vote, Safestack, Secure Agent Control Protocol, Compositional Dependability
- Stance: engineering
- Relates to: A concrete agent-middleware realisation of the security calculus in Secure Communications Processing for Distributed Languages; its formal-specification stance meets the language-workbench pragmatics of The Spoofax Language Workbench; pattern reuse echoes dependability concerns in Are Multiagent Systems Resilient to Communication Failures and Theory of Self-Reproducing Automata.
Tags