888 resultados para Top-level management
Resumo:
Ciao is a public domain, next generation multi-paradigm programming environment with a unique set of features: Ciao offers a complete Prolog system, supporting ISO-Prolog, but its novel modular design allows both restricting and extending the language. As a result, it allows working with fully declarative subsets of Prolog and also to extend these subsets (or ISO-Prolog) both syntactically and semantically. Most importantly, these restrictions and extensions can be activated separately on each program module so that several extensions can coexist in the same application for different modules. Ciao also supports (through such extensions) programming with functions, higher-order (with predicate abstractions), constraints, and objects, as well as feature terms (records), persistence, several control rules (breadth-first search, iterative deepening, ...), concurrency (threads/engines), a good base for distributed execution (agents), and parallel execution. Libraries also support WWW programming, sockets, external interfaces (C, Java, TclTk, relational databases, etc.), etc. Ciao offers support for programming in the large with a robust module/object system, module-based separate/incremental compilation (automatically -no need for makefiles), an assertion language for declaring (optional) program properties (including types and modes, but also determinacy, non-failure, cost, etc.), automatic static inference and static/dynamic checking of such assertions, etc. Ciao also offers support for programming in the small producing small executables (including only those builtins used by the program) and support for writing scripts in Prolog. The Ciao programming environment includes a classical top-level and a rich emacs interface with an embeddable source-level debugger and a number of execution visualization tools. The Ciao compiler (which can be run outside the top level shell) generates several forms of architecture-independent and stand-alone executables, which run with speed, efficiency and executable size which are very competive with other commercial and academic Prolog/CLP systems. Library modules can be compiled into compact bytecode or C source files, and linked statically, dynamically, or autoloaded. The novel modular design of Ciao enables, in addition to modular program development, effective global program analysis and static debugging and optimization via source to source program transformation. These tasks are performed by the Ciao preprocessor ( ciaopp, distributed separately). The Ciao programming environment also includes lpdoc, an automatic documentation generator for LP/CLP programs. It processes Prolog files adorned with (Ciao) assertions and machine-readable comments and generates manuals in many formats including postscript, pdf, texinfo, info, HTML, man, etc. , as well as on-line help, ascii README files, entries for indices of manuals (info, WWW, ...), and maintains WWW distribution sites.
Resumo:
El principal objetivo de la presente investigación fue el conocer el perfil de rendimiento técnico de los triatletas, desde un punto de vista biomecánica, en el segmento carrera a pie durante la competición en triatlón. Asimismo, como el genero y el nivel deportivo del triatleta podrían influir en su respuesta motriz durante la competicion. Para ello, se necesitaba desarrollar y validar una técnica experimental que fuera lo suficientemente precisa (validez interna), con una alta fiabilidad y con una gran validez externa (ecologica) debido al entorno de la competicion. La muestra la formaron un total de 64 deportistas: 32 triatletas participantes en la Copa del Mundo de Triatlon de Madrid-2008 (16 hombres y 16 mujeres) y 32 triatletas participantes en el Clasificatorio del Campeonato de Espana Elite (16 hombres y 16 mujeres). El análisis de la técnica de carrera de los deportistas se realizo mediante un sistema fotogramétrico en 2d que permitió calcular las coordenadas (x,y) de los centros articulares con un error de 1.66% en el eje x y de un 2.10% en el eje y. Las imágenes fueron obtenidas por una cámara que filmaba el movimiento en un plano antero-posterior del triatleta. Algoritmos basados en la DLT (Abdel-Aziz & Karara, 1971) permitieron conocer las coordenadas reales a partir de las coordenadas digitalizadas en el plano y posteriormente las distintas variables analizadas. El análisis biomecánica de la carrera se realizo en 4 ocasiones diferentes durante la competición, correspondiendo con cada una de las vueltas de 2,5 km, que el triatleta tenía que realizar. La velocidad de carrera resulto estar íntimamente ligada al nivel deportivo del triatleta. Del mismo modo, 3 de los 4 grupos analizados presentaron valores inferiores a 3 minutos 30 segundos por kilometro recorrido, poniendo de manifiesto el altísimo nivel de los sujetos analizados. Del mismo modo parece que las chicos consiguen una mayor velocidad gracias a una mayor longitud de ciclo en relación a las chicas, ya que estas muestran valores mayores en cuanto a frecuencia de zancada. La frecuencia de zancada presento los valores más altos en la primera vuelta en todos los deportistas analizados. Asimismo, los triatletas de nivel internacional y las chicas fueron los que mostraron los mayores valores. La longitud de zancada presento distintas tendencias en función del nivel y el género del deportista. Así pues, en los deportistas internacionales y en los chicos los mayores valores se encontraron en la primera vuelta mientras que la tendencia fue al descenso, siendo probablemente la fatiga acumulada la causante de dicha tendencia. En cambio, aquellos deportistas de nivel nacional y las chicas mostraron valores mayores en la segunda vuelta que en la primera, evidenciando que además de la fatiga, el ciclismo previo tiene una incidencia directa sobre su rendimiento. Los tiempos de vuelo permanecieron constantes durante toda la carrera, encontrando cierta evolución en los tiempos de apoyo, la cual provoca una modificación en los porcentajes relativos en los tiempos de vuelo. Los tiempos de apoyo más bajos se encontraron en la primera vuelta. Del mismo modo, los deportistas de nivel internacional y los chicos mostraron valores inferiores. También, estos grupos fueron más constantes en sus valores a lo largo de las vueltas. Por el contrario, se encontraron tendencias al aumento en los triatletas de nivel nacional y en las chicas, los cuales no fueron capaces de mantener el mismo rendimiento debido seguramente a su menor nivel deportivo. La oscilación vertical de la cadera se mostro constante en los triatletas de mayor nivel, encontrándose tendencias al aumento en los de menor nivel. Del mismo modo, los valores más altos correspondieron a las chicas y a los deportistas de nivel nacional. La distancia de la cadera al apoyo permaneció constante a lo largo de las vueltas en todos los grupos, obteniéndose valores mayores en los triatletas de nivel internacional y en los chicos. El ángulo de la rodilla apoyada en el momento del despegue no mostro una tendencia clara. Los deportistas de nivel internacional y los chicos presentaron los valores más bajos. El ángulo de la rodilla libre en el momento del despegue mostro una correlación muy alta con la velocidad de carrera. Del mismo modo, los ángulos más pequeños se encontraron en los triatletas internacionales y en los chicos, debido seguramente a los mayores valores de velocidad registrados por ambos grupos. Los ángulos de los tobillos no mostraron ninguna tendencia clara durante la competición analizada. Los cuatro grupos de población presentaron valores similares, por lo que parece que no representan una variable que pueda incidir sobre el rendimiento biomecánica del triatleta. Los resultados obtenidos en el presente estudio de investigación avalan la utilización de la fotogrametría-video en 2d para el análisis de la técnica de carrera durante la competición en triatlón. Su aplicación en una competición de máximo nivel internacional ha posibilitado conocer el perfil técnico que presentan los triatletas a lo largo del segmento de carrera a pie. Del mismo modo, se ha podido demostrar como los estudios realizados en laboratorio no reflejan la realidad competitiva de un triatlón de máximo nivel. The aim of this research was to determine the running technique profile during a triathlon competition from a biomechanical perspective. Also, to analyze the triathlete gender’s and level of performance’s influence on this profile in competition. An accurate (internal validity) and reliable methodology with a high external validity (ecological) had to be developed to get those aims in competition. Sixty-four triathletes were analyzed. 32 (16 males, 16 females) took part in the Madrid 2008 Triathlon World Cup and 32 (16 males and 16 females) took part in the Spanish Triathlon National Championships. The biomechanical analyses were carried out by a photogrammetric system that allow to calculate the landmarks coordinates (x,y) with a 1.66% error in x axis, and a 2.10% error in y axis. The frames were obtained with a camera situated perpendicular to the triathletes’ trajectory, filming the saggittal plane. DLT based algorithms (Abdel-Aziz & Karara, 1971) were used to calculate the real coordinates from the digitalized ones and the final variables afterwards. The biomechanical analisys itself was performed in four different moments during the competition, according to each 2.5 km lap the triathletes had to do. Running speed was highly related to performance level. Also, 3 of the 4 analyzed groups showed speed values under the 3 minutes and 30 seconds per kilometer. It demonstrated the very high performance level of the analized triathletes. Furthermore, it seems that men get higher speeds because their longer stride length, while women shows higher stride frequency values. The highest stride frequency values were found in the first lap. Women and the international level triathletes showed the highest values. Stride length showed different tendencies according to the gender and level of performance. Men and international level triathletes showed the highest level in the first lap and a decreasing tendency after that. The accumulated fatigue was probably the reason of this tendency. On the other hand, higher values than in first lap were found in the second one in women and national level triathletes. It demonstrated the previous cycling can affect to those groups in terms of biomechanics. Flight times remained constant during the running part, while the contact times showed an increasing tendency that caused a variation in flight times percents. The lowest contact times were found in the first lap and in men and international triathletes’ values. Also, these two groups were more consistent during the whole running. On the other hand, increasing tendencies were found in women and national level triathletes, who were not able to maintain the same values probably due to their lower level of performance. Higher level triathletes showed more consistent hip vertical oscillation values than lower level triathletes, who presented increasing tendencies. The highest values were found in women and national level triathletes. The horizontal distance hip-toe cap remained constant among the laps in all the groups. Men and international level triathletes showed the highest values. The support knee angle at toe-off did not show a clear tendency. The lowest values were found in men and international level triathletes. A high correlation was found between the non-support knee angle and the running speed. Furthermore, men and international level triathletes showed the smallest values, due to the higher velocities reached by these two groups. Ankles angles did not show any tendency during the running part. Similar values were found in the four analyzed groups, so this variable does not seem to represent an important one within the triathlete’s performance. The results obtained in the present research support the use of the bidimensional photogrammetric video-system to analyze the running technique during a triathlon competition. Its application in international triathlon meetings has allowed determining the triathletes’ technique profile during the running part. Also, it has been demonstrated the laboratory-based studies does not reproduce a top-level competition.
Resumo:
This paper analyzes issues which appear when supporting pruning operators in tabled LP. A version of the once/1 control predicate tailored for tabled predicates is presented, and an implementation analyzed and evaluated. Using once/1 with answer-on-demand strategies makes it possible to avoid computing unneeded solutions for problems which can benefit from tabled LP but in which only a single solution is needed, such as model checking and planning. The proposed version of once/1 is also directly applicable to the efficient implementation of other optimizations, such as early completion, cut-fail loops (to, e.g., prune at the top level), if-then-else, and constraint-based branch-and-bound optimization. Although once/1 still presents open issues such as dependencies of tabled solutions on program history, our experimental evaluation confirms that it provides an arbitrarily large efficiency improvement in several application areas.
Resumo:
El principal objetivo del presente trabajo de investigación fue determinar las diferencias en distintas variables relacionadas con el rendimiento físico entre atletas de distinto nivel durante la prueba de los 60 metros vallas. Un total de 59 vallistas masculinos (los 31 participantes en el Campeonato del Mundo Absoluto de Pista Cubierta y los 28 participantes en el Campeonato de España Absoluto de Pista Cubierta, ambos celebrados en Valencia en el año 2008) formaron la muestra del estudio. El análisis biomecánico se realizó mediante un sistema fotogramétrico en dos dimensiones que permitió calcular, aplicando algoritmos basados en el procedimiento de la DLT (Abdel-Aziz y Karara, 1971), las coordenadas (x, y) de los sucesivos apoyos de los pies de los atletas sobre toda la superficie de competición. La filmación de las pruebas se llevó a cabo con seis cámaras de vídeo, ubicadas sobre la gradas, con una frecuencia de muestreo para el tratamiento de los datos de 50 Hz. En la fase de salida, los atletas de nivel superior mostraron una menor longitud (p<0,05) y tiempo de zancada (p<0,001), debido a un menor tiempo de vuelo (p<0,05). En la fase de vallas, los atletas de nivel más elevado presentaron mayores distancia de ataque a la valla (p<0,001), así como menores distancias de caída de la valla (p<0,001), tiempos de zancada (p<0,01-0,001) y de apoyo (p<0,01-0,001 ) en los cuatro pasos que conforman cada ciclo de vallas, así como un menor tiempo de vuelo en el paso de valla (p<0,001) y en el paso de transición (p<0,001). De manera adicional, se encontraron importantes diferencias en el reparto de los pasos entre vallas entre la primera y tercera valla y el resto de obstáculos. En la fase final, se observó una mayor longitud de zancada en los atletas de nivel superior (p<0,001), así como un menor tiempo de zancada (p<0,01) y de apoyo (p<0,01). Los resultados obtenidos en el presente estudio de investigación avalan la utilización de la fotogrametría en dos dimensiones para el análisis biomecánico de la prueba de 60 metros vallas en competición. Su aplicación en competiciones del máximo nivel internacional ha posibilitado conocer las características de los vallistas a lo largo de toda la prueba y determinar posibles implicaciones de cara al proceso de entrenamiento. ABSTRACT The aim of this research was to determine the differences in different variables related to physical performance among athletes of different levels during the race of 60 meter hurdles. A total of 59 male hurdlers (the 31 participants in the World Indoor Championship and the 28 participants in the Spanish Indoor Championship, both held in Valencia in 2008) formed the sample of the study. The biomechanical analysis of athletes was performed using a two-dimensional photogrammetric system which enabled calculation, applying algorithms based on the DLT method (Abdel -Aziz y Karara , 1971), the coordinates (x , y) of the successive supports of the feet on the entire competition surface. Filming test was conducted with six video cameras, located on the bleachers, with a sampling frequency for data processing of 50 Hz. In the approach run phase, the top-level athletes showed a smaller length step (p<0.05), and shorter step time (p<0.001), due to a shorter step flight time (p<0.05). In the hurdle unit phase, the higher level athletes had greater take-off distances (p<0.001), shorter landing distances (p<0.001), smaller step times (p<0.01-0.001), and support times (p<0.01- 0.001) in the four steps that comprised each hurdle unit, and smaller flight times in the hurdle step (p < 0.001), and the recovery step (p<0.001). Additionally, differences in the distribution of hurdle unit steps between the first and third hurdle, and other hurdles were found. In the run-in phase, a greater step length in top-level athletes (p<0.001), and a shorter step time (p<0.01) and contact time (p<0.01) was observed. The results obtained in this study support the use of photogrammetry in two dimensions for biomechanical analysis in 60 meter hurdles competition events. Its application at the highest international level competitions has allowed to know the characteristics of the hurdlers over the entire race and identify possible implications for the training process.
Resumo:
In this paper, a set of design parameters, such as the slopes of upstream and downstream faces of the dam, radius of the upper arch, width of the dam at the top level and height of the vertical upper part of the dam, are given as function of the valley characteristics when the dam is situated, such as its geometry and its geotechnical properties. These tables have been obtained using a regression of the design parameters of an arch-gravity dam with a minimum concrete volume, placed in a large number of valleys with different characteristics and properties. Elasticites for these design parameters are also discussed.
Resumo:
Kelp forests are strongly influenced by macroinvertebrate grazing on fleshy macroalgae. In the North Pacific Ocean, sea otter predation on macroinvertebrates substantially reduces the intensity of herbivory on macroalgae. Temperate Australasia, in contrast, has no known predator of comparable influence. These ecological and biogeographic patterns led us to predict that (i) the intensity of herbivory should be greater in temperate Australasia than in the North Pacific Ocean; thus (ii) Australasian seaweeds have been under stronger selection to evolve chemical defenses and (iii) Australasian herbivores have been more strongly selected to tolerate these compounds. We tested these predictions first by measuring rates of algal tissue loss to herbivory at several locations in Australasian and North Pacific kelp forests. There were significant differences in grazing rates among sea otter-dominated locations in the North Pacific (0-2% day-1), Australasia (5-7% day-1), and a North Pacific location lacking sea otters (80% day-1). The expectations that chronically high rates of herbivory in Australasia have selected for high concentrations of defensive secondary metabolites (phlorotannins) in brown algae and increased tolerance of these defenses in the herbivores also were supported. Phlorotannin concentrations in kelps and fucoids from Australasia were, on average, 5-6 times higher than those in a comparable suite of North Pacific algae, confirming earlier findings. Furthermore, feeding rates of Australasian herbivores were largely unaffected by phlorotannins, regardless of the compounds' regional source. North Pacific herbivores, in contrast, were consistently deterred by phlorotannins from both Australasia and the North Pacific. These findings suggest that top-level consumers, acting through food chains of various lengths, can strongly influence the ecology and evolution of plantherbivore interactions.
Resumo:
Women’s handball is a sport, which has seen an accelerated development over the last decade. Data on movement patterns in combination with physiological demands are nearly nonexistent in the literature. The aim of this study was twofold: first, to analyze the horizontal movement pattern, including the sprint acceleration profiles, of individual female elite handball players and the corresponding heart rates (HRs) during a match and secondly to determine underlying correlations with individual aerobic performance. Players from one German First League team (n = 11) and the Norwegian National Team (n = 14) were studied during one match using the Sagit system for movement analysis and Polar HR monitoring for analysis of physiological demands. Mean HR during the match was 86 % of maximum HR (HRmax). With the exception of the goalkeepers (GKs, 78 % of HRmax), no position-specific differences could be detected. Total distance covered during the match was 4614 m (2066 m in GKs and 5251 m in field players (FPs)). Total distance consisted of 9.2 % sprinting, 26.7 % fast running, 28.8 % slow running, and 35.5 % walking. Mean velocity varied between 1.9 km/h (0.52 m/s) (GKs) and 4.2 km/h (1.17 m/s) (FPs, no position effect). Field players with a higher level of maximum oxygen uptake (V̇O2max) executed run activities with a higher velocity but comparable percentage of HRmax as compared to players with lower aerobic performance, independent of FP position. Acceleration profile depended on aerobic performance and the field player’s position. In conclusion, a high V̇O2max appears to be important in top-level international women’s handball. Sprint and endurance training should be conducted according to the specific demands of the player’s position.
Resumo:
The coming weeks and months will be decisive for the general tenor of politics in Turkey. The country faces local elections this March, presidential elections in August and general elections next June, while top-level political scandals compound the deterioration in the state of democracy and rule of law. At the same time, stagnation in Turkey’s accession process continues to sour relations with the EU. In this new Policy Brief, Steven Blockmans puts forward a number of recommendations to help drive the EU accession process forward, namely the early opening of negotiation chapters 23 (judiciary and fundamental rights) and 24 (justice, freedom and security), in line with the EU’s so-called New Approach. In that way reform could not just be assured on paper, but a track record in implementation could be established throughout the process. To achieve this, member states, and Cyprus in particular, need to be persuaded to end their opposition to formulating benchmarks for the opening of accession negotiating chapters 23 and 24.
Resumo:
The policy of rapprochement with Russia that President Victor Yanukovych and his entourage had been actively promoting in the first months of his presidency has slowed down notably. One of the reasons for this lowered pace is that current talks between Russia and Ukraine concern the spheres in which Kyiv is not ready to make concessions to Russia. Despite numerous top-level meetings, recent months have failed to bring a breakthrough in energy issues of key importance. First of all, no compromise was reached in gas issues where the divergence of interests is particularly large and where Ukraine has adopted a tough stance to negotiate the best conditions possible. Even though some agreements were signed during the October session of the inter-governmental committee presided over by the prime ministers (the agreement on linking the two states’ aircraft production and on the joint construction of a nuclear fuel production plant), these resulted from prior agreements. Economic negotiations will continue in the coming months but the observed deadlock is not likely to be broken any time soon. The results of these talks are likely to reflect the interests of both Russia and Ukraine, as well as the competition among Ukrainian business groups, some of which opt for closer cooperation with their Eastern neighbour. Ukraine’s consent to send oil to Belarus along the Odessa-Brody pipeline shows that the government in Kyiv is ready to engage in projects they consider profitable, even those that run counter to Russian interests. Ukraine’s adoption of this stance may trigger irritation in Moscow and lead to a cooling in bilateral relations.
Resumo:
Visualization has proven to be a powerful and widely-applicable tool the analysis and interpretation of data. Most visualization algorithms aim to find a projection from the data space down to a two-dimensional visualization space. However, for complex data sets living in a high-dimensional space it is unlikely that a single two-dimensional projection can reveal all of the interesting structure. We therefore introduce a hierarchical visualization algorithm which allows the complete data set to be visualized at the top level, with clusters and sub-clusters of data points visualized at deeper levels. The algorithm is based on a hierarchical mixture of latent variable models, whose parameters are estimated using the expectation-maximization algorithm. We demonstrate the principle of the approach first on a toy data set, and then apply the algorithm to the visualization of a synthetic data set in 12 dimensions obtained from a simulation of multi-phase flows in oil pipelines and to data in 36 dimensions derived from satellite images.
Resumo:
Initially this paper asks two questions: In order to create and sustain competitive advantage through collaborative systems WHAT should be managed? and HOW should it be managed? It introduces the competitive business structure and reviews some of the global trends in manufacturing and business, which leads to focus on manage processes, value propositions and extended business processes. It then goes on to develop a model of the collaborative architecture for extended enterprises and demonstrates the validity of this architecture through a case study. It concludes that, in order to create and sustain competitive advantage, collaborative systems should facilitate the management of: the collaborative architecture of the extended enterprise; the extended business processes and the value proposition for each extended enterprise through a meta level management process. It also identifies areas for further research, such as better understanding of: the exact nature and interaction of multiple strategies within an enterprise; how to manage people/teams working along extended business processes; and the nature and prerequisites of the manage processes.
Resumo:
This thesis applies a hierarchical latent trait model system to a large quantity of data. The motivation for it was lack of viable approaches to analyse High Throughput Screening datasets which maybe include thousands of data points with high dimensions. High Throughput Screening (HTS) is an important tool in the pharmaceutical industry for discovering leads which can be optimised and further developed into candidate drugs. Since the development of new robotic technologies, the ability to test the activities of compounds has considerably increased in recent years. Traditional methods, looking at tables and graphical plots for analysing relationships between measured activities and the structure of compounds, have not been feasible when facing a large HTS dataset. Instead, data visualisation provides a method for analysing such large datasets, especially with high dimensions. So far, a few visualisation techniques for drug design have been developed, but most of them just cope with several properties of compounds at one time. We believe that a latent variable model (LTM) with a non-linear mapping from the latent space to the data space is a preferred choice for visualising a complex high-dimensional data set. As a type of latent variable model, the latent trait model can deal with either continuous data or discrete data, which makes it particularly useful in this domain. In addition, with the aid of differential geometry, we can imagine the distribution of data from magnification factor and curvature plots. Rather than obtaining the useful information just from a single plot, a hierarchical LTM arranges a set of LTMs and their corresponding plots in a tree structure. We model the whole data set with a LTM at the top level, which is broken down into clusters at deeper levels of t.he hierarchy. In this manner, the refined visualisation plots can be displayed in deeper levels and sub-clusters may be found. Hierarchy of LTMs is trained using expectation-maximisation (EM) algorithm to maximise its likelihood with respect to the data sample. Training proceeds interactively in a recursive fashion (top-down). The user subjectively identifies interesting regions on the visualisation plot that they would like to model in a greater detail. At each stage of hierarchical LTM construction, the EM algorithm alternates between the E- and M-step. Another problem that can occur when visualising a large data set is that there may be significant overlaps of data clusters. It is very difficult for the user to judge where centres of regions of interest should be put. We address this problem by employing the minimum message length technique, which can help the user to decide the optimal structure of the model. In this thesis we also demonstrate the applicability of the hierarchy of latent trait models in the field of document data mining.
Resumo:
Using a unique firm level data, this paper analyses the role of political connections in the post-entry performance of private start-up companies in China. It documents robust evidence that political affiliation enhances firms' survival and growth prospects. But interestingly politically neutral start-ups enjoy faster productivity improvements conditional on survival. In addition, the benefits of political connections are largely confined to firms associated with local or top level governments, and they are more pronounced in capital-intensive industries. We conclude that the close association between the state and a segment of the business community is leading to sub-optimal resource allocation in the economy by interfering with the process of market selection.
Resumo:
Technological capabilities in Chinese manufacturing have been transformed in the last three decades. However, the extent to which and how domestic market oriented state owned enterprises (SOEs) have developed their capabilities remain important questions. The East Asian latecomer model has been adapted to study six Chinese SOEs in the automotive, steel and machine tools sectors to assess capability levels attained and the role of external sources and internal efforts in developing them. All six enterprises demonstrate high competence in operating established technology, managing investment and making product and process improvements but differ in innovative capability. While the East Asian latecomer model in which linking, leveraging and learning explain technological capability development is relevant for the companies studied, it needs to be adapted for Chinese SOEs to take account of types of external links and leverage of enterprises, the role of government, enterprise level management motives and means of financing development.
Resumo:
Modern software systems are often large and complicated. To better understand, develop, and manage large software systems, researchers have studied software architectures that provide the top level overall structural design of software systems for the last decade. One major research focus on software architectures is formal architecture description languages, but most existing research focuses primarily on the descriptive capability and puts less emphasis on software architecture design methods and formal analysis techniques, which are necessary to develop correct software architecture design. ^ Refinement is a general approach of adding details to a software design. A formal refinement method can further ensure certain design properties. This dissertation proposes refinement methods, including a set of formal refinement patterns and complementary verification techniques, for software architecture design using Software Architecture Model (SAM), which was developed at Florida International University. First, a general guideline for software architecture design in SAM is proposed. Second, specification construction through property-preserving refinement patterns is discussed. The refinement patterns are categorized into connector refinement, component refinement and high-level Petri nets refinement. These three levels of refinement patterns are applicable to overall system interaction, architectural components, and underlying formal language, respectively. Third, verification after modeling as a complementary technique to specification refinement is discussed. Two formal verification tools, the Stanford Temporal Prover (STeP) and the Simple Promela Interpreter (SPIN), are adopted into SAM to develop the initial models. Fourth, formalization and refinement of security issues are studied. A method for security enforcement in SAM is proposed. The Role-Based Access Control model is formalized using predicate transition nets and Z notation. The patterns of enforcing access control and auditing are proposed. Finally, modeling and refining a life insurance system is used to demonstrate how to apply the refinement patterns for software architecture design using SAM and how to integrate the access control model. ^ The results of this dissertation demonstrate that a refinement method is an effective way to develop a high assurance system. The method developed in this dissertation extends existing work on modeling software architectures using SAM and makes SAM a more usable and valuable formal tool for software architecture design. ^