Towards the formation of a sustainable South Florida: An analysis of conflict resolution and consensus building in the South Florida Everglades Ecosystem Restoration Initiative

This dissertation examines the sociological process of conflict resolution and consensus building in South Florida Everglades Ecosystem Restoration through what I define as a Network Management Coordinative Interstitial Group (NetMIG). The process of conflict resolution can be summarized as the participation of interested and affected parties (stakeholders) in a forum of negotiation. I study the case of the Governor's Commission for a Sustainable South Florida (GCSSF) that was established to reduce social conflict. Such conflict originated from environmental disputes about the Everglades and was manifested in the form of gridlock among regulatory (government) agencies, Indian tribes, as well as agricultural, environmental conservationist and urban development interests. The purpose of the participatory forum is to reduce conflicts of interest and to achieve consensus, with the ultimate goal of restoration of the original Everglades ecosystem, while cultivating the economic and cultural bases of the communities in the area. Further, the forum aim to formulate consensus through envisioning a common sustainable community by providing means to achieve a balance between human and natural systems. ^ Data were gathered using participant observation and document analysis techniques to conduct a theoretically based analysis of the role of the Network Management Coordinative Interstitial Group (NetMIG). I use conflict resolution theory, environmental conflict theory, stakeholder analysis, systems theory, differentiation and social change theory, and strategic management and planning theory. ^ The purpose of this study is to substantiate the role of the Governor's Commission for a Sustainable South Florida (GCSSF) as a consortium of organizations in an effort to resolve conflict rather than an ethnographic study of this organization. Environmental restoration of the Everglades is a vehicle for recognizing the significance of a Network Management Coordinative Interstitial Group (NetMIG), namely the Governor's Commission for a Sustainable South Florida (GCSSF), as a structural mechanism for stakeholder participation in the process of social conflict resolution through the creation of new cultural paradigms for a sustainable community. ^

A framework for specification and analysis of software architectures

Software architecture is the abstract design of a software system. It plays a key role as a bridge between requirements and implementation, and is a blueprint for development. The architecture represents a set of early design decisions that are crucial to a system. Mistakes in those decisions are very costly if they remain undetected until the system is implemented and deployed. This is where formal specification and analysis fits in. Formal specification makes sure that an architecture design is represented in a rigorous and unambiguous way. Furthermore, a formally specified model allows the use of different analysis techniques for verifying the correctness of those crucial design decisions. ^ This dissertation presented a framework, called SAM, for formal specification and analysis of software architectures. In terms of specification, formalisms and mechanisms were identified and chosen to specify software architecture based on different analysis needs. Formalisms for specifying properties were also explored, especially in the case of non-functional properties. In terms of analysis, the dissertation explored both the verification of functional properties and the evaluation of non-functional properties of software architecture. For the verification of functional property, methodologies were presented on how to apply existing model checking techniques on a SAM model. For the evaluation of non-functional properties, the dissertation first showed how to incorporate stochastic information into a SAM model, and then explained how to translate the model to existing tools and conducts the analysis using those tools. ^ To alleviate the analysis work, we also provided a tool to automatically translate a SAM model for model checking. All the techniques and methods described in the dissertation were illustrated by examples or case studies, which also served a purpose of advocating the use of formal methods in practice. ^

An approach for design and analysis of User-centric Communication Middleware

Today, the development of domain-specific communication applications is both time-consuming and error-prone because the low-level communication services provided by the existing systems and networks are primitive and often heterogeneous. Multimedia communication applications are typically built on top of low-level network abstractions such as TCP/UDP socket, SIP (Session Initiation Protocol) and RTP (Real-time Transport Protocol) APIs. The User-centric Communication Middleware (UCM) is proposed to encapsulate the networking complexity and heterogeneity of basic multimedia and multi-party communication for upper-layer communication applications. And UCM provides a unified user-centric communication service to diverse communication applications ranging from a simple phone call and video conferencing to specialized communication applications like disaster management and telemedicine. It makes it easier to the development of domain-specific communication applications. The UCM abstraction and API is proposed to achieve these goals. The dissertation also tries to integrate the formal method into UCM development process. The formal model is created for UCM using SAM methodology. Some design errors are found during model creation because the formal method forces to give the precise description of UCM. By using the SAM tool, formal UCM model is translated to Promela formula model. In the dissertation, some system properties are defined as temporal logic formulas. These temporal logic formulas are manually translated to promela formulas which are individually integrated with promela formula model of UCM and verified using SPIN tool. Formal analysis used here helps verify the system properties (for example multiparty multimedia protocol) and dig out the bugs of systems.

A comparative analysis of corporate finance in the United States and Japan from 1880 to 1930

This study explained the diversity of corporate financial practices in two nations. Existing studies have emphasized the reliance on equity finance in U.S. firms and bank loans in Japanese firms. In fact, patterns of corporate finance were much more complex. Financial institutions, which were created by national economic policy and regulation, affected corporate financial practices, but corporate financial practices often differed from what policymakers expected. Differences in corporate financial practices between nations also reflected differences in the mixture of industries in each nation. Many factors such as the amount of fixed capital, the process of production, the level of risk, the degree of innovation, and the importance of the industry in the national economy affected corporate financial practices. In addition, corporate financial practices within each nation differed from firm to firm due to managers’ considerations about stock ownership, which would affect their control power; corporate finance was closely related to control over management through ownership. To explain these complexities of corporate financial practices, the study linked corporate finance with the development of financial institutions in the United States and in Japan. While financial institutions affected corporate financial practices, the response of the firms to financial institutions and opportunities were diverse. The study also attempted to grasp variations in corporate financial practices by dealing with companies in three sectors: railroads, public utilities, and manufacturing. Finally, the study examined the structure of firm ownership. Contradictory to the widely held belief that U.S. firms distributed securities more widely to the public than did Japanese firms, many large American firms remained closely held, while some Japanese counterparts built publicly-held corporations.

Formal verification and testing of software architectural models

Ensuring the correctness of software has been the major motivation in software research, constituting a Grand Challenge. Due to its impact in the final implementation, one critical aspect of software is its architectural design. By guaranteeing a correct architectural design, major and costly flaws can be caught early on in the development cycle. Software architecture design has received a lot of attention in the past years, with several methods, techniques and tools developed. However, there is still more to be done, such as providing adequate formal analysis of software architectures. On these regards, a framework to ensure system dependability from design to implementation has been developed at FIU (Florida International University). This framework is based on SAM (Software Architecture Model), an ADL (Architecture Description Language), that allows hierarchical compositions of components and connectors, defines an architectural modeling language for the behavior of components and connectors, and provides a specification language for the behavioral properties. The behavioral model of a SAM model is expressed in the form of Petri nets and the properties in first order linear temporal logic.^ This dissertation presents a formal verification and testing approach to guarantee the correctness of Software Architectures. The Software Architectures studied are expressed in SAM. For the formal verification approach, the technique applied was model checking and the model checker of choice was Spin. As part of the approach, a SAM model is formally translated to a model in the input language of Spin and verified for its correctness with respect to temporal properties. In terms of testing, a testing approach for SAM architectures was defined which includes the evaluation of test cases based on Petri net testing theory to be used in the testing process at the design level. Additionally, the information at the design level is used to derive test cases for the implementation level. Finally, a modeling and analysis tool (SAM tool) was implemented to help support the design and analysis of SAM models. The results show the applicability of the approach to testing and verification of SAM models with the aid of the SAM tool.^

Analysis of Housing Partnerships using the Balanced Scorecard framework

Housing Partnerships (HPs) are collaborative arrangements that assist communities in the delivery of affordable housing by combining the strengths of the public and private sectors. They emerged in several states, counties, and cities in the eighties as innovative solutions to the challenges in affordable housing resulting from changing dynamics of delivery and production. ^ My study examines HPs with particular emphasis upon the identification of those factors associated with the successful performance of their mission of affordable housing. I will use the Balanced Scorecard (BSC) framework in this study. The identification of performance factors facilitates a better understanding of how HPs can be successful in achieving their mission. The identification of performance factors is significant in the context of the current economic environment because HPs can be viewed as innovative institutional mechanisms in the provision of affordable housing. ^ The present study uses a mixed methods research approach, drawing on data from the IRS Form 990 tax returns, a survey of the chief executives of HPs, and other secondary sources. The data analysis is framed according to the four perspectives of BSC: the financial, customer, internal business, and learning and growth. Financially, revenue diversification affects the financial health of HPs and overall performance. Although HPs depend on private and government funding, they also depend on service fees to carry out their mission. From a customer perspective, the HPs mainly serve low and moderate income households, although some serve specific groups such as seniors, homeless, veterans, and victims of domestic violence. From an internal business perspective, HPs’ programs are oriented toward affordable housing needs, undertaking not only traditional activities such as construction, loan provision, etc., but also advocacy and educational programs. From an employee and learning growth perspective, the HPs are small in staff size, but undertake a range of activities with the help of volunteers. Every part of the HP is developed to maximize resources, knowledge, and skills in order to assist communities in the delivery of affordable housing and related needs. Overall, housing partnerships have played a key role in affordable housing despite the housing market downturn since 2006. Their expenses on affordable housing activities increased despite the decrease in their revenues.^

AIDS workplace *policy adoption and implementation in local government: An analysis of departmental variation

This is an empirical study whose purpose was to examine the process of innovation adoption as an adaptive response by a public organization and its subunits existing under varying degrees of environmental uncertainty. Meshing organization innovation research and contingency theory to form a theoretical framework, an exploratory case study design was undertaken in a large, metropolitan government located in an area with the fourth highest prevalence rate of HIV/AIDS in the country. A number of environmental and organizational factors were examined for their influence upon decision making in the adoption/non-adoption as well as implementation of any number of AIDS-related policies, practices, and programs.^ The major findings of the study are as follows. For the county government itself (macro level), no AIDS-specific workplace policies have been adopted. AIDS activities (AIDS education, AIDS Task Force, AIDS Coordinator, etc.), adopted county-wide early in the epidemic, have all been abandoned. Worker infection rates, in the aggregate and throughout the epidemic have been small. As a result, absent co-worker conflict (isolated and negligible), no increase in employee health care costs, no litigation regarding discrimination, and no major impact on workforce productivity, AIDS has basically become a non-issue at the strategic core of the organization. At the departmental level, policy adoption decisions varied widely. Here the predominant issue is occupational risk, i.e., both objective as well as perceived. As expected, more AIDS-related activities (policies, practices, and programs) were found in departments with workers known to have significant risk for exposure to the AIDS virus (fire rescue, medical examiner, police, etc.). AIDS specific policies, in the form of OSHA's Bloodborn Pathogen Standard, took place primarily because they were legislatively mandated. Union participation varied widely, although not necessarily based upon worker risk. In several departments, the union was a primary factor bringing about adoption decisions. Additional factors were identified and included organizational presence of AIDS expertise, availability of slack resources, and the existence of a policy champion. Other variables, such as subunit size, centralization of decision making, and formalization were not consistent factors explaining adoption decisions. ^

A deontic analysis of inter -organizational control requirements

This research focuses on the design and verification of inter-organizational controls. Instead of looking at a documentary procedure, which is the flow of documents and data among the parties, the research examines the underlying deontic purpose of the procedure, the so-called deontic process, and identifies control requirements to secure this purpose. The vision of the research is a formal theory for streamlining bureaucracy in business and government procedures. ^ Underpinning most inter-organizational procedures are deontic relations, which are about rights and obligations of the parties. When all parties trust each other, they are willing to fulfill their obligations and honor the counter parties’ rights; thus controls may not be needed. The challenge is in cases where trust may not be assumed. In these cases, the parties need to rely on explicit controls to reduce their exposure to the risk of opportunism. However, at present there is no analytic approach or technique to determine which controls are needed for a given contracting or governance situation. ^ The research proposes a formal method for deriving inter-organizational control requirements based on static analysis of deontic relations and dynamic analysis of deontic changes. The formal method will take a deontic process model of an inter-organizational transaction and certain domain knowledge as inputs to automatically generate control requirements that a documentary procedure needs to satisfy in order to limit fraud potentials. The deliverables of the research include a formal representation namely Deontic Petri Nets that combine multiple modal logics and Petri nets for modeling deontic processes, a set of control principles that represent an initial formal theory on the relationships between deontic processes and documentary procedures, and a working prototype that uses model checking technique to identify fraud potentials in a deontic process and generate control requirements to limit them. Fourteen scenarios of two well-known international payment procedures—cash in advance and documentary credit—have been used to test the prototype. The results showed that all control requirements stipulated in these procedures could be derived automatically.^

A Comparative Analysis of Corporate Finance in the United States and Japan From 1880 to 1930

This study explained the diversity of corporate financial practices in two nations. Existing studies have emphasized the reliance on equity finance in U.S. firms and bank loans in Japanese firms. In fact, patterns of corporate finance were much more complex. Financial institutions, which were created by national economic policy and regulation, affected corporate financial practices, but corporate financial practices often differed from what policymakers expected. Differences in corporate financial practices between nations also reflected differences in the mixture of industries in each nation. Many factors such as the amount of fixed capital, the process of production, the level of risk, the degree of innovation, and the importance of the industry in the national economy affected corporate financial practices. In addition, corporate financial practices within each nation differed from firm to firm due to managers’ considerations about stock ownership, which would affect their control power; corporate finance was closely related to control over management through ownership. To explain these complexities of corporate financial practices, the study linked corporate finance with the development of financial institutions in the United States and in Japan. While financial institutions affected corporate financial practices, the response of the firms to financial institutions and opportunities were diverse. The study also attempted to grasp variations in corporate financial practices by dealing with companies in three sectors: railroads, public utilities, and manufacturing. Finally, the study examined the structure of firm ownership. Contradictory to the widely held belief that U.S. firms distributed securities more widely to the public than did Japanese firms, many large American firms remained closely held, while some Japanese counterparts built publicly-held corporations.

A Deontic Analysis of Inter-Organizational Control Requirements

This research focuses on the design and verification of inter-organizational controls. Instead of looking at a documentary procedure, which is the flow of documents and data among the parties, the research examines the underlying deontic purpose of the procedure, the so-called deontic process, and identifies control requirements to secure this purpose. The vision of the research is a formal theory for streamlining bureaucracy in business and government procedures. Underpinning most inter-organizational procedures are deontic relations, which are about rights and obligations of the parties. When all parties trust each other, they are willing to fulfill their obligations and honor the counter parties’ rights; thus controls may not be needed. The challenge is in cases where trust may not be assumed. In these cases, the parties need to rely on explicit controls to reduce their exposure to the risk of opportunism. However, at present there is no analytic approach or technique to determine which controls are needed for a given contracting or governance situation. The research proposes a formal method for deriving inter-organizational control requirements based on static analysis of deontic relations and dynamic analysis of deontic changes. The formal method will take a deontic process model of an inter-organizational transaction and certain domain knowledge as inputs to automatically generate control requirements that a documentary procedure needs to satisfy in order to limit fraud potentials. The deliverables of the research include a formal representation namely Deontic Petri Nets that combine multiple modal logics and Petri nets for modeling deontic processes, a set of control principles that represent an initial formal theory on the relationships between deontic processes and documentary procedures, and a working prototype that uses model checking technique to identify fraud potentials in a deontic process and generate control requirements to limit them. Fourteen scenarios of two well-known international payment procedures -- cash in advance and documentary credit -- have been used to test the prototype. The results showed that all control requirements stipulated in these procedures could be derived automatically.

Formal verification and testing of software architectural models

Ensuring the correctness of software has been the major motivation in software research, constituting a Grand Challenge. Due to its impact in the final implementation, one critical aspect of software is its architectural design. By guaranteeing a correct architectural design, major and costly flaws can be caught early on in the development cycle. Software architecture design has received a lot of attention in the past years, with several methods, techniques and tools developed. However, there is still more to be done, such as providing adequate formal analysis of software architectures. On these regards, a framework to ensure system dependability from design to implementation has been developed at FIU (Florida International University). This framework is based on SAM (Software Architecture Model), an ADL (Architecture Description Language), that allows hierarchical compositions of components and connectors, defines an architectural modeling language for the behavior of components and connectors, and provides a specification language for the behavioral properties. The behavioral model of a SAM model is expressed in the form of Petri nets and the properties in first order linear temporal logic. This dissertation presents a formal verification and testing approach to guarantee the correctness of Software Architectures. The Software Architectures studied are expressed in SAM. For the formal verification approach, the technique applied was model checking and the model checker of choice was Spin. As part of the approach, a SAM model is formally translated to a model in the input language of Spin and verified for its correctness with respect to temporal properties. In terms of testing, a testing approach for SAM architectures was defined which includes the evaluation of test cases based on Petri net testing theory to be used in the testing process at the design level. Additionally, the information at the design level is used to derive test cases for the implementation level. Finally, a modeling and analysis tool (SAM tool) was implemented to help support the design and analysis of SAM models. The results show the applicability of the approach to testing and verification of SAM models with the aid of the SAM tool.