|Title||Extended Abstract: Formal Verification of Architectural Patterns in Support of Dependable Distributed Systems|
|Publication Type||Conference Paper|
|Year of Publication||2005|
|Authors||Jeffords, R., and R. Bharadwaj|
|Conference Name||Third ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'05)|
|Conference Location||Verona, Italy|
Architectural patterns, analogous to design patterns, are a means to develop mechanisms for adding non-functional requirements, such as fault-tolerance, during the integration of hardware and software components. A synchronous language, the Secure Operations Language (SOL), was developed as a verifiable language for development of components (agents) to be ntegrated into high assurance systems. Agents written in SOL execute in a distributed nfrastructure allowing creation, deployment, migration, communication, etc. of these agents. his research addresses the generic extension f SOL to support architectural patterns. The architectural pattern, Hot Standby, which provides backup computational capability in case of failure of the primary resource, is exemplified. It is shown that formal properties, associated with such architectural patterns written in extended SOL are amenable to formal proof.
|NRL Publication Release Number|| |