Analysis of GA/LS Architectures

Analysis of GA/LS Systems (Powerpoint Presentation)

Systems consisting of pockets of synchronous components connected asynchronously are often referred to as Globally Asynchronous/Locally Synchronous (GA/LS) architectures. While the tools and methods developed on the MT-FCS project work quite well on synchronous systems, it is much more difficult to verify properties that span asynchronous components. However, with the growing popularity of model-based development using tools such as Simulink and SCADE, GA/LS architectures are becoming quite common and techniques for verifying such properties are badly needed.

The MT-FCS project investigated techniques for the verification of GA/LS systems that exhibited unbounded asynchrony. While interesting, these approaches don't appear to scale well to large systems. However, real systems are always implemented with tight bounds on the asynchrony. Finding a way to exploit these bounds may help to keep the problem tractable.

Another approach would be the development of design patterns for common architectural features. Examples of such architectural patterns are already well known in the fault-tolerant computing literature. Development and verification of a handful of such patterns may be sufficient for the development of architectures known to preserve key system properties.

Publications on Analysis of GA/LS Architectures

• Steven P. Miller, Mike W. Whalen, Dan O’Brien, Mats P.E. Heimdahl, and Anjali Joshi, A Methodology for the Design and Verification of Globally Asynchronous/Locally Synchronous Architectures, NASA Contractor Report NASA/CR-2005-213912, Sept. 2005.