TitleExtended Abstract: Formal Verification of Architectural Patterns in Support of Dependable Distributed Systems
Publication TypeConference Paper
Year of Publication2005
AuthorsJeffords, R., and R. Bharadwaj
Conference NameThird ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'05)
Conference LocationVerona, Italy
Abstract

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.

Full Text

JeffordsBharadwaj2005.pdf

NRL Publication Release Number

05-1226-2336