A methodology for formally modeling and analyzing software architecture of mobile agent systems

A methodology for formally modeling and analyzing software architecture of mobile agent systems provides a solid basis to develop high quality mobile agent systems, and the methodology is helpful to study other distributed and concurrent systems as well. However, it is a challenge to provide the methodology because of the agent mobility in mobile agent systems.^ The methodology was defined from two essential parts of software architecture: a formalism to define the architectural models and an analysis method to formally verify system properties. The formalism is two-layer Predicate/Transition (PrT) nets extended with dynamic channels, and the analysis method is a hierarchical approach to verify models on different levels. The two-layer modeling formalism smoothly transforms physical models of mobile agent systems into their architectural models. Dynamic channels facilitate the synchronous communication between nets, and they naturally capture the dynamic architecture configuration and agent mobility of mobile agent systems. Component properties are verified based on transformed individual components, system properties are checked in a simplified system model, and interaction properties are analyzed on models composing from involved nets. Based on the formalism and the analysis method, this researcher formally modeled and analyzed a software architecture of mobile agent systems, and designed an architectural model of a medical information processing system based on mobile agents. The model checking tool SPIN was used to verify system properties such as reachability, concurrency and safety of the medical information processing system. ^ From successful modeling and analyzing the software architecture of mobile agent systems, the conclusion is that PrT nets extended with channels are a powerful tool to model mobile agent systems, and the hierarchical analysis method provides a rigorous foundation for the modeling tool. The hierarchical analysis method not only reduces the complexity of the analysis, but also expands the application scope of model checking techniques. The results of formally modeling and analyzing the software architecture of the medical information processing system show that model checking is an effective and an efficient way to verify software architecture. Moreover, this system shows a high level of flexibility, efficiency and low cost of mobile agent technologies. ^

New trends in health architecture for children and the effects of the built environment on young patients

The objective of this thesis was to investigate the effects of the built environment on the outcome of young patients. This investigation included recent innovations in children's hospitals that integrated both medical and architectural case studies as part of their design issues. In addition, the intervention responded to man-made conditions and natural elements of the site. The thesis project, a Children's Rehabilitation Hospital, is located at 1500 N.W. River Drive in Miami, Florida. The thesis intervention emerged from a site analysis that focused on the shifting of the urban grid, the variation in scale of the immediate context and the visual-physical connection to the river's edge. Furthermore, it addressed the issues of overnight accommodation for patient's families, as well as sound control through the use of specific materials in space enclosures and open courtyards. The key to the success of this intervention lies in the special attention given to the integration between nature and the built environment. Issues such as the incorporation of nature within a building through the use of vistas and the exploitation of natural light through windows and skylights, were pivotal in the creation of a pleasant environment for visitors, employees and young patients.

Mobile architecture : offering new perceptions of the city

The purpose of this thesis is to explore the design of mobile architecture that challenges traditional ideas of site through the design of a museum to commemorate immigration to the United States. This thesis develops a floating, moveable, inhabitable structure that moves on the inter-coastal waterways of South Florida, within the public areas of Miami. The floating museum offers new perceptions of the city and new means of occupying its various settings. Its architectural elements do not change but are read differently in each location. The museum brings its exhibitions to the city as an event. One moment it is there and the next it is gone. In its design, the Museum of Immigration explores the experience of leaving one place to settle in another. As a prototype, it might be the first in a series of such buildings around the country that offers a new relationship between building and site.