Refinement methods for software architecture design using the software architecture model

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. ^

An aspect-oriented approach to designing role-based access control services

Access control (AC) limits access to the resources of a system only to authorized entities. Given that information systems today are increasingly interconnected, AC is extremely important. The implementation of an AC service is a complicated task. Yet the requirements to an AC service vary a lot. Accordingly, the design of an AC service should be flexible and extensible in order to save development effort and time. Unfortunately, with conventional object-oriented techniques, when an extension has not been anticipated at the design time, the modification incurred by the extension is often invasive. Invasive changes destroy design modularity, further deteriorate design extensibility, and even worse, they reduce product reliability. ^ A concern is crosscutting if it spans multiple object-oriented classes. It was identified that invasive changes were due to the crosscutting nature of most unplanned extensions. To overcome this problem, an aspect-oriented design approach for AC services was proposed, as aspect-oriented techniques could effectively encapsulate crosscutting concerns. The proposed approach was applied to develop an AC framework that supported role-based access control model. In the framework, the core role-based access control mechanism is given in an object-oriented design, while each extension is captured as an aspect. The resulting framework is well-modularized, flexible, and most importantly, supports noninvasive adaptation. ^ In addition, a process to formalize the aspect-oriented design was described. The purpose is to provide high assurance for AC services. Object-Z was used to specify the static structure and Predicate/Transition net was used to model the dynamic behavior. Object-Z was extended to facilitate specification in an aspect-oriented style. The process of formal modeling helps designers to enhance their understanding of the design, hence to detect problems. Furthermore, the specification can be mathematically verified. This provides confidence that the design is correct. It was illustrated through an example that the model was ready for formal analysis. ^

Des activités physiques et sportives pratiquées par les femmes au Québec : Témoignages et collections (1880-1974)

Ce mémoire porte sur la pratique du sport et de l‟activité physique par les femmes au Québec entre 1880 et 1974, par l‟étude de la collection d‟objets sportifs du Musée de la civilisation, le dépouillement de catalogues commerciaux et d‟autres documents d‟archives, ainsi que l‟analyse de contenu de témoignages oraux recueillis par la chercheure et tenus dans le cadre du projet « Vivre sa ville : Québec au XXe siècle » du Laboratoire d‟ethnologie urbaine. L‟utilisation de ces trois sources de données permet de faire ressortir les modalités d‟insertion des femmes dans la pratique sportive. Les normes et les pratiques du sport féminin seront abordées notamment en ce qui a trait à l‟hygiène, à la morale chrétienne, aux installations et aux organisations sportives.

Diseño urbano arquitectónico del Parque Cultural y Recreativo Coyoctor en el cantón Cañar

El presente trabajo se desarrolla con la finalidad de resolver un problema de carácter social que acontece en la ciudad de Cañar, el cual consiste en el déficit de áreas verdes, por lo que en respuesta ante esta necesidad se propone el diseño urbano arquitectónico de un equipamiento recreativo, que mejore la calidad de vida de la población. El contexto en el cual se desarrolla esta propuesta, se caracteriza por su patrimonio material e inmaterial, mismo que incide de manera directa en las decisiones que se toman sobre el anteproyecto. Para el desarrollo del anteproyecto como fase final del presente documento de tesis, se requiere un vasto estudio que inicia con los aspectos históricos del cantón Cañar, la teoría y metodologías necesarias para abordar proyectos urbano arquitectónicos, un diagnostico que incorpora temas sociales y técnicos, además un análisis formal del espacio basado en la cultura cañari.

O cinema de Ray Harryhausen: efeitos especiais e maneirismo no cinema de Hollywood

Através de uma análise histórico-formal, este trabalho propõe uma leitura maneirista da obra de Ray Harryhausen (1920-2013), um dos maiores criadores de efeitos especiais do cinema de Hollywood, verdadeiro autor de uma série de filmes que se distinguem pelo uso virtuoso da técnica, colocada ao serviço de narrativas fantásticas, construídas numa clara referencia a grandes clássicos do cinema de Hollywood.

Alexander Scriabin: the definition of a new sound space in the crisis of tonality

This dissertation describes the new compositional system introduced by Scriabin in 1909– 1910, focusing on Feuillet d’Album op. 58, Poème op. 59, nº1, Prélude op. 59, nº2 and Promethée op. 60. Based upon exhaustive pitch and formal analysis the present study (a) claims the inexistence of non-functional pitches in all analysed works, (b) shows that transpositional procedures have structural consequences on the “basic chord”, and (c) for the first time advances an explanation on the intrinsic relation between the sonata form and the slow Luce line in Promethée op. 60; RESUMO: Sob o título de “Alexander Scriabin: a definição dum novo espaço sonoro na crise da Tonalidade”, a presente tese descreve o novo sistema compositivo introduzido por Scriabin em 1909– 1910, tomando como ponto de partida o estudo de Feuillet d’Album op. 58, Poème op. 59, nº1, Prélude op. 59, nº2 e Promethée op. 60. Baseando-se numa análise exaustiva das alturas e da forma, este estudo (a) conclui pela inexistência de alturas não funcionais em qualquer das obras analisadas, (b) mostra que os procedimentos transpositivos têm consequências estruturais no “acorde básico”, e (c) pela primeira vez explica a estrutura formal de Promethée op. 60 a partir da relação intrínseca entre a sua forma sonata e a linha lenta de Luce.

Formal security analysis of Australian e-passport implementation

This paper provides a detailed description of the current Australian e-passport implementation and makes a formal verification using model checking tools CASPER/CSP/FDR. We highlight security issues present in the current e-passport implementation and identify new threats when an e-passport system is integrated with an automated processing systems like SmartGate. Because the current e-passport specification does not provide adequate security goals, to perform a rational security analysis we identify and describe a set of security goals for evaluation of e-passport protocols. Our analysis confirms existing security issues that were previously informally identified and presents weaknesses that exists in the current e-passport implementation.

Formal modelling and analysis of DNP3 secure authentication

Supervisory Control and Data Acquisition (SCADA) systems are one of the key foundations of smart grids. The Distributed Network Protocol version 3 (DNP3) is a standard SCADA protocol designed to facilitate communications in substations and smart grid nodes. The protocol is embedded with a security mechanism called Secure Authentication (DNP3-SA). This mechanism ensures that end-to-end communication security is provided in substations. This paper presents a formal model for the behavioural analysis of DNP3-SA using Coloured Petri Nets (CPN). Our DNP3-SA CPN model is capable of testing and verifying various attack scenarios: modification, replay and spoofing, combined complex attack and mitigation strategies. Using the model has revealed a previously unidentified flaw in the DNP3-SA protocol that can be exploited by an attacker that has access to the network interconnecting DNP3 devices. An attacker can launch a successful attack on an outstation without possessing the pre-shared keys by replaying a previously authenticated command with arbitrary parameters. We propose an update to the DNP3-SA protocol that removes the flaw and prevents such attacks. The update is validated and verified using our CPN model proving the effectiveness of the model and importance of the formal protocol analysis.

Formal network behaviour analysis using model checking

In this research we modelled computer network devices to ensure their communication behaviours meet various network standards. By modelling devices as finite-state machines and examining their properties in a range of configurations, we discovered a flaw in a common network protocol and produced a technique to improve organisations' network security against data theft.

Formal security analysis of the DNP3-secure authentication protocol

This thesis evaluates the security of Supervisory Control and Data Acquisition (SCADA) systems, which are one of the key foundations of many critical infrastructures. Specifically, it examines one of the standardised SCADA protocols called the Distributed Network Protocol Version 3, which attempts to provide a security mechanism to ensure that messages transmitted between devices, are adequately secured from rogue applications. To achieve this, the thesis applies formal methods from theoretical computer science to formally analyse the correctness of the protocol.

Identification and doing without it, V: A formal mathematical analysis for a case of mix-up of individuals, and of recovery from failure to attain identification

Identification, when sought, is not necessarily obtained. Operational guidance that is normatively acceptable may be necessary for such cases. We proceed to formalize and illustrate modes of exchanges of individual identity, and provide procedures of recovery strategies in specific prescriptions from an ancient body of law for such situations when, for given types of purposes, individuals of some relevant kind had become intermixed and were undistinguishable. Rules were devised, in a variety of domains, for coping with situations that occur if and when the goal of identification was frustrated. We propose or discuss mathematical representations of such recovery procedures.

Production Linkages Between Informal and Formal Activities Considering Domestic and Imported Inputs: an Application of the Minimal-Flow-Analysis Method to Senegal.

We apply to the Senegalese input-output matrix of 1990, disagregated into formal and informal activities, a recently designed structural analytical method (Minimal-Flow-Analysis) which permits to depict the direct and indirect production likanges existing between activities.