Made available in DSpace on 2015-04-11T14:03:15Z (GMT). No. of bitstreams: 1 DISSERTACAO MARCELO.pdf: 1313111 bytes, checksum: ddf9a22433355413e807d3bd27951a01 (MD5) Previous issue date: 2008-12-15 / Fundação de Amparo à Pesquisa do Estado do Amazonas / Embedded systems have undeniable relevance in modern society. They have temporal constraints (as long as they are real time ones), power consumption management, size, weight, etc which make their design more complex than the design of their desktop peers. Given the huge number of requirements of all kinds, the high complexity of embedded software as well as the big possibilities of critical damages in case of flaws and, at last, the even bigger pressure of market for new products faster, it make necessary methods which can assure correct, fast but intuitive specification and conception of designs. Considering this, this work aims to provide a method which contribute to the state of art. The goal of the proposed method is to provide an approach which gather an specification of an embedded software in a semi-formal, object-oriented and Industry-accepted notation, which is Unified Modeling (UML), specifically their Sequence Diagram notation which is able to capture dynamic aspects of a system and a mecanism of translation of this notation into a formal one, called SMV, apropriate for being used by the SMV model checker. The goal of the method is also provide an translation scheme of the sequence diagrams into another formal notation, the so called Petri Nets notations. Petri Net notation is well suited to formal verification. Finally, the goal of the method is to provide a mechanism of translation of high level properties queries into formal notation CTL. Property queries are only qualitative. All these functionalities are implemented in a tool called Ambiente de Verificação Formal de Software Embarcado. / Os sistemas embarcados possuem inegável importância na sociedade atual. Eles possuem restrições temporais (quando são de tempo real), de gerência de consumo de energia, tamanho, peso etc que tornam o seu projeto e concepção mais complexos do que os sistemas convencionais. Dado o grande número de requisitos de todos os tipos, a alta complexidade dos softwares embarcados desenvolvidos bem como a grande possibilidade de catástrofes significativas em caso de falha e por fim a grande pressão de mercado por produtos cada vez mais rápido, fazem-se necessários métodos que possam assegurar uma correta, rápida porém intuitiva especificação e concepção dos projetos. Diante disso, o presente trabalho visa prover um método que acrescente ao atual estado da arte. O objetivo do método então é prover uma abordagem que colete uma especificação de software embarcado em uma notação semi-formal, orientada a objetos e amplamente aceita pela Indústria, que é a Unified Modeling Language (UML), especificamente com seu Diagrama de Sequência, o qual é apto para capturar os aspectos dinâmicos de um sistema e um mecanismo de tradução dessa notação para a notação formal SMV, apta a ser utilizada pelo model checker de mesmo nome. O objetivo do método é prover também um esquema de tradução dos diagramas de sequência em UML para uma notação formal, no caso a notação de Redes de Petri, o qual é adequada para verificação formal, gerando saídas de arquivos nos formatos APNN e PNML. O formato APNN é adequado para ser usado no Model Checking Kit (MCK). Por fim, prover um esquema de tradução consultas de propriedade em alto nível para o formato de CTL puro adequado para ser usado no MCK e um programa em SMV e sua especificação 7 em CTL, formatos aptos a serem usados no model checker SMV. A verificação de propriedades é apenas qualitativa, isto é, que verificará apenas propriedades de execução do software embarcado, em oposição às propriedades quantitativas de tempo por exemplo, comuns em softwares de tempo-real. Todas essas funcionalidades são realizadas por uma ferramenta, chamada Ambiente de Verificação Formal de Software Embarcado.

Com o aumento do uso das atividades de modelagem em processos de desenvolvimento de software, a participação de pessoas com deficiência visual em tais processos requer esforços dedicados para que os modelos sejam passíveis de entendimento, caso contrário essa participação fica comprometida. Os modelos são em sua maioria visuais e, portanto, seu processo de construção requer o posicionamento de elementos no espaço do documento por meio de um dispositivo de apontar, como o mouse, e sua leitura requer o uso da visão, uma vez que os diagramas são compostos não apenas por textos, mas também por elementos visuais como retângulos e arcos conectando-os. Neste contexto, o objetivo deste projeto foi desenvolver uma técnica textual para representação e interação com diagramas que possibilite que pessoas com deficiência visual sejam capazes de colaborar em projetos de software, tanto utilizando uma abordagem de desenvolvimento orientado a modelos, quanto em uma abordagem de desenvolvimento tradicional. Para atingir o objetivo proposto foi desenvolvido um protótipo de uma ferramenta Web, a AWMo (lê-se letra a letra: A-W-M-O), a partir da qual a edição de modelos pode ser realizada por meio de duas visões equivalentes: uma visão gráfica, na qual o engenheiro de software poderá inserir novos elementos no diagrama, posicioná-los e definir suas propriedades de modo visual; e uma visão textual, na qual o engenheiro de software pode inserir novos elementos, propriedades e relacioná-los utilizando uma gramática textual. Um estudo de caso foi conduzido para avaliar sua eficácia e os resultados mostraram que a linguagem textual desenvolvida não representa uma barreira para a utilização da abordagem proposta pela AWMo. Os resultados sugerem que a AWMo é uma opção viável para facilitar o acesso de deficientes visuais a modelos de software, ajudando a promover a colaboração e comunicação efetiva e de maneira independente entre usuários com e sem visão para atividades de modelagem de software / With the growth of modeling activities in software development processes, the participation of visually impaired users requires dedicated efforts so that the models are capable to be understood, otherwise this participation is compromised. The models are mostly visuals and, therefore, their construction process requires the positioning of elements in the document space with a pointing device, like the mouse, and their reading requires the use of vision, since the diagrams are composed not only by text, but also by visual elements such as rectangles and arcs connecting them. In this context, the goal of this project was to develop a textual technique to represent and interact with diagrams to allow visually disabled people to collaborate in software development projects, either using an model driven development approach or a tradicional development approach. To achieve the proposed goal, a prototype Web tool called AWMo was developed. The prototype allows the edition of models to be done in two distinct views: a graphical view, where the software engineer is able to insert new elements and define their position in a visual and traditional way; and a textual view, where the software engineer is able to insert new elements, their properties and relationships using a textual grammar. A case study was conducted to evaluate the efficacy of the approach and the results show that the textual language developed did not posed itself as a barrier to the use of the AWMo. The results suggest that AWMo is a viable option to allow the access of the visually impaired to software models, promoting collaboration and effective communication between sighted and blind users in software modeling activities, but most importantly, in an independent way

Since Web applications are very complex, compared to traditional client/server applications, Web application design with the UML can be obtrusively hard for a modeller. The grounds are that the UML does not define the correct semantics to be able to visualize a web application correctly. This is a qualitative reduction study where we have used interviews and our own experience during the redesign of a UML-modelled e-commerce application with WAE-UML. Using the flow of a case study we have tried to see if we can improve three quality attributes of a complete design. Stakeholder communication reflects the need of unambiguous design artefacts that are easy to understand and that mediate the real message of the use-case. The condition of the design artefacts should provide artefacts that resemble reality and that not are misleading and provide for verification and validation of the requirements. The last attribute maintainability should provide means for easy maintenance and updates. We found that WAE-UML can improve these quality attributes in a design but the impact it has on them is dependent on two major aspects. The first aspect concerns the designers’ judgment of detail in a design. A detailed design can be good considering requirements and use-case traceability and verification, but prohibit communication. Maintainability can also be improved in a detailed design because the diagrams are less abstract and a truer picture of the application. The second aspect is that it depends on the knowledge possessed of the semantics by the people in contact with the design documents. Due to the time aspect the people working in the industry that we interviewed were reluctant to modelling a Web application at all. They thought it would take a long time to learn WAE-UML but also for executing a design phase. / Contact e-mail: miga02@student.bth.se, hean01@student.bth.se

This diploma thesis is focused on a topic selection for bachelor and diploma theses, student’s registration for the topics, a registration for state exams and bachelor and diploma theses defense. This thesis includes an analysis of this area and a proposal of an electronic solution. The main goal of this thesis is to build a solution which eliminates a physical appearance of students at school during the registration for the topic of bachelor and diploma theses as well as a registration for state exams and bachelor and diploma theses defense. In connection with this is also valuable to spare the work of the department clerk and secretary connected with the registration agenda. The analysis was realized mostly by UML methodology, the solution includes detailed ERD model and the proposed application screen layouts. The final result of this work is a complete solution proposal that is ready to be used for the application implementation.

Le langage UML est devenu un standard de fait, y compris pour le développement de systèmes critiques. Néanmoins, les outils actuels apportent peu d'aide pour exploiter et vérifier les modèles proposés, surtout en cours de développement. Cette thèse se concentre sur l'aide à la construction d'architectures en UML durant les phases d'analyse et de conception de systèmes réactifs. Elle vise à développer un cadre théorique et pragmatique pour mettre en œuvre une approche incrémentale. Ce cadre fournit un outil permettant de vérifier les architectures durant leur modélisation. Les architectures sont modélisées par des diagrammes UML de structures composites alors que les composants primitifs sont présentés par une combinaison de diagrammes de machines d'états et de diagramme d'activités. Ce travail offre les moyens de vérifier d'une part si une nouvelle architecture est un raffinement, une extension ou un incrément de celle définie durant les étapes précédentes, et d'autre part si un composant est compatible avec un environnement ou s'il est substituable par un autre. L'analyse des architectures impose de leur donner une sémantique formelle. Concernant les composants primitifs, nous leur associons une sémantique en LTS (Labelled Transition Systems) ce qui nous a conduit à définir une procédure de transformation automatique de machines d'états et diagrammes d'activités en LTS. Concernant les composants composites, nous leur associons un LTS en transformant un diagramme de structure composite en une spécification Exp.Open, puis en générant la fusion des LTS grâce à la boîte à outils CADP. Dans un second temps, nous avons mis en œuvre des techniques de vérifications de relations de conformité de LTS que sont les préordres de raffinement, d'extension, et d'incrément. Nous avons également défini et implanté une relation de compatibilité et de substituabilité. L'ensemble de ces techniques de construction incrémentale se positionne selon deux axes. L'axe vertical représente le niveau d'abstraction. L'évolution d'une architecture peut se faire sur cet axe dans deux sens : i) par des techniques de raffinement dans le sens descendant et ii) par des techniques d'abstraction dans le sens ascendant. L'axe horizontal représente le niveau de couverture des exigences. L'évolution d'une architecture peut se faire sur cet axe selon deux sens : i) par des techniques d'extension et ii) par des techniques de restriction. Ces travaux ont été réalisés de façon théorique et pratique : ils ont donné lieu au développement d'un outil dédié à la construction incrémentale de modèles UML, appelé IDCM (Incremental Development of Conforming Models), regroupant la transformation de modèles et la mise en œuvre de l'ensemble des relations incrémentales. Ceci a été validé sur diverses études de cas. / UML is becoming a de facto standard, including for development of dependable systems. However, current tools offer little help to take benefit of proposed models and to verify them, especially during development phases. This thesis focuses on supporting construction of UML architectures of reactive systems. It aims at developing a theoretic and pragmatic framework to implement the incremental approach. The framework provides tools to verify the coherenceof architectures during the modelling phase. Architectures are modelled by UML diagram of composite structures while primitive components are represented by a combination of state machine diagram and activity diagram. This work provides a means to verify in one hand if a new architecture is a refinement, an extension or an increment of those defined in the previous steps, and in another hand, if a component is compatible with an environment or if it is substitutableby another.In order to analyse UML architectures, we must give them a formal semantics. We associated primitive components with LTS (Labelled Transition Systems) which led us to define a procedure for automatic transformation of state machines and activities diagrams into LTS. We associated composite components with LTS by transforming a diagram of composite structure into Exp.Open specification, then by generating LTS fusion with the toolbox CADP. We have implemented verification techniques of conformance relations on LTS such as the preorders: refinement, extension, and increment. We also defined and implemented compatibility relation and substitutability relation. All these incremental construction techniques are positioned along two axes. The vertical axis represents the level of bstraction.The development of an architecture following this axis in two directions: i) refinement techniques in the downward direction and ii) abstraction techniques in the upward direction. The horizontal axis represents the coverage level of requirements. The development of architectures can be realized following this axis in two directions : i) extension direction and ii) restrictiondirection.This work has been carried out in theory and practice : it has led to the development of a dedicated tool for incremental construction of UML models, called IDCM (Incremental Development of Conforming Models), grouping the transformation of models and the implementation of a set of incremental relations. This has been validated on various case studies.

This work deals with the problematics of conversion of UML diagrams to code. Initially, existing solutions in this field are analyzed. Based on the gained findings, a new tool is designed and implemened. It accepts UML class diagrams and database models from the free diagramming environment Dia and for each of these offers three target languages. The key feature of this tool is its modular design allowing new target languages to be added easily.

Der Große Beleg dokumentiert die Entwicklung eines Java Code-Generators für Dresden OCL2 for Eclipse. Schwerpunkt der Arbeit liegt dabei auf der Abbildung der Object Constraint Language auf die Programmiersprache Java mit Hilfe von AspectJ.

Displaying the architecture of a software system is not a simple task. Showing all of the available information will unnecessarily complicate the view, while showing too little might render the view unhelpful. Furthermore, showing the dynamics of the operation of such a system is even more challenging. This thesis project describes the development of a graphical tool that can both display the configuration of an advanced authentication, authorization, and accounting (AAA) system and the messages passed between nodes in the system.  The solution described uses force-based graph layouts coupled with adaptive filters as well as vector-based rendering to deliver a view of the status of the system. Force-based layout spreads out the nodes in an adaptive fashion. The adaptive filters starts by showing what is most often the most relevant information, but can be configured by the user. Finally, the vector based rendering offers unlimited zoom into the individual nodes in the graph in order to display additional detailed information. Unified Modeling Language (UML) sequence charts are used to display the message flow inside the system (both between nodes and inside individual nodes). To validate the results of this thesis project each iteration of the design was evaluated through meetings with the staff at Aptilo Networks. These meetings provided feedback on the direction the project was taking as well as provided input (such as ideas for features to implement). The result of this thesis project shows a way to display the status of an AAA system with multiple properties displayed at the same time. It combines this with a view of the flow of messages and application of policies in the network via a dynamically generated UML sequence diagram. As a result human operators are able to see both the system’s architecture and the dynamics of its operation using the same user interface. This integrated view should enable more effective management of the AAA system and facilitate responding to problems and attacks. / Att visualisera arkitekturen av ett mjukvarusystem är inte lätt. Visas all tillgänglig information så blir vyn för komplicerad medan ifall för lite visas så blir vyn onödig. Att samtidigt visa dynamiken som uppstår när systemet arbetar är ytterligare en utmaning. Detta examensprojektet beskriver hur utvecklingen av ett grafiskt verktyg, som både kan visa konfigurationen av ett avancerat autentisering-, tillåtelse- och bokförings-system (AAA) och meddelanden som skickas mellan noder i systemet.<p> Lösningen använder en kraftriktad graflayout tillsammans med adaptiva filter och vektorbaserad rendering för att visa en vy av systemets status. De adaptiva filtren börjar med att visa den information som oftast är mest relevant men kan ställas in av användaren. Nyttjandet av vektorbaserad grafik tillhandahåller obegränsade möjligheter för användaren att zooma in på delar av grafen för att visa mer detaljerad information. UML sekvensdiagram används för att visa medelandeflödet inuti systemet (både mellan noder och inuti noder). För att utvärdera resultatet av examensprojektet blev varje iteration av designen utvärderad vid möten med personalen på Aptilo Networks. Dessa möten gav återkoppling på vilken rikting projektet tog samt input med t. ex. id´eer på nya egenskaper att lägga till. Resultatet av detta examensarbete visar ett sätt att visa statusen för ett AAA system med många av systemets egenskaper visade samtidigt. Det kombinerar detta med en vy av flödet av meddelanden och applikationpolicies i nätverket via ett dynamiskt genererat UML sekvensdiagram. Resultatet av detta är att mänskliga operatörer kan se både systemets arkitektur och dynamiken i hur det fungerar i samma gränssnitt. Detta gränssnitt bör möjliggöra mer effektiv hantering av AAA systemet och underlätta lösningar på både problem i systemet och attacker mot systemet.

Målet med detta examensarbete har varit att modellera och implementera ett system för att generera medlemskort för idrottsföreningar på uppdrag av Express-Bild AB. Genom deras webbsida vill företaget att man för en förening ska kunna skapa ett medlemskort. En medlem i föreningen ska sedan kunna ladda ner och visa sitt kort i Androidenheten. När kortet visas i mobilen ska det gå att tilta bilden då Androidenhetens position ändras från ett vertikalt läge till ett horisontellt. I samband med att kortet visas i ett vertikalt läge vill företaget att erbjudanden om rabatter och liknande ska visas i samma vy. Skapade kort ska även kunna administreras på sidan. För att åstadkomma detta har tre subsystem identifierats: Ett system för att skapa en mall för korten, ett för att ladda upp viktiga komponenter för korten och ett för att skapa, ladda ner och visa de individuella korten till enheten. Modeller för systemen upprättades i UML för att öka förståelsen av, och insikten i systemens uppbyggnad och funktion. Utifrån modellerna gjordes senare implementationen av systemen. Resultatet av arbetet blev ett system som uppfyllde de flesta av de krav som Express-Bild önskade se uppfyllda. Det enda kravet som inte uppfylldes var att kunna visa erbjudanden om rabatter i medlemskortets vy. / The goal with this bachelor thesis has been to model and implement a system for generating membership cards for sports associations on behalf of Express-Bild AB. By using their webpage, the company wants a privileged user of an association to be able to create a membership card for the association. A member of the association should then be able to download and view the card in his android device. When the card is displayed in the device, it should be posible to rotate the card when the device is being tilted. When the card is displayed in a vertical position, should also offers about discounts be displayed in the same view. The possiblity to administrate these cards should exists on the webpage. To accomplish this, three subsystems has been indentified: One system for the creation of a card template, one for uploading important resourdces for the card, and one for creating, downloading and displaying the individual membership card to the device. Models for these systems were established in UML to increase the understanding, and the insight of the systems structure and functionality. These models were later used when implementing the systems. The result of the thesis was a system that fulfilled most of the requirements that Express-Bild had. The only requirement that was not implemented was the one about displaying offers in the membership card view.

Model Driven Development (MDD) and Model Based Testing (MBT) are gaining inroads individually for their application in embedded software engineering projects. However, their full-edged and integrated usage in real-life embedded software engineering projects (e.g. industrially relevant examples) and executing MBT in resource constrained embedded systems (e.g. 16 bit system/64 KiByte memory) are emerging fields. Addressing the aforementioned gaps, this thesis proposes an integrated model-based approach and test framework for executing the model-based test cases, with minimal overhead, in embedded systems. Given a chosen System Under Test (SUT) and the system design model, a test framework generation algorithm generates the necessary artifacts (i.e., the test framework) for executing the model-based test cases. The main goal of the test framework is to enable test automation and test case execution at the host computer (which executes the test harness), thereby only the test input data is executed at the target. Significant overhead involved in interpreting the test data at the target is eliminated, as the test framework makes use of a target debugger (communication and decoding agent) on the host and a target monitor (software-based runtime monitoring routine) in the embedded system. In the prototype implementation of the proposed approach, corresponding (standardized) languages such as the Unified Modeling Language (UML) and the UML Testing Profile (UTP) are used for the MDD and MBT phases respectively. The applicability of the proposed approach is demonstrated using an experimental evaluation (of the prototype) in real-life examples. The empirical results indicate that the total time spent for executing the test cases in the target (runtime-time complexity), comprises of only the time spent to decode the test input data by the target monitor and execute it in the embedded system. Similarly, the only memory requirement in the target for executing the model-based test cases in the target is that of the software-based target monitor. A quantitative comparison on the percentage change in the memory overhead (runtime-memory complexity) for the existing approach and the proposed approach indicates that the existing approach (e.g. in a MDD/MBT tool-Rhapsody), introduces approximately 150% to 350% increase in memory overhead for executing the test cases. On the other hand, in the proposed approach, the target monitor is independent of the number of test cases to be executed and their complexity. Hence, the percentage change in the memory overhead for the proposed approach shows a declining trend w.r.t the increasing code-size for equivalent application scenarios (approximately 17% to 2%). Thus, the proposed test automation approach provides the essential benefit of executing model- based tests, without downloading the test harness in the target. It is demonstrated that it is feasible to execute the test cases specified at higher abstraction levels (e.g. using UML sequence diagrams) in resource constrained embedded systems and how this may be realized using the proposed approach. Further, as the proposed runtime monitoring mechanism is time and memory-aware, the overhead parameters can be accommodated in the earlier phases of the embedded software development cycle (if necessary) and the target monitor can be included in the final production code. The aforementioned advantages highlight the scalability, applicability, reliability and superiority of the proposed approach over the existing methodologies for executing the model-based test cases in embedded systems.