No description available.

This dissertation investigates the role of specification, refinement and implementation in the software development cycle. Both the structured and object-oriented paradigms are looked at. Particular emphasis is placed on the role of the refinement process. The requirements for the product (system) are determined, the specifications are drawn up, the product is designed, specified, implemented and tested. The stage between the (formal) specification of the system and the implementation of the system is the refinement stage. The refinement process consists out of data refinement, operation refinement, and operation decomposition. In this dissertation, Z, Object-Z and UML (Unified Modelling Language) are used as specification languages and C, C++, Cobol and Object-Oriented Cobol are used as implementation languages. As an illustration a small system, The ITEM System, is specified in Z and UML and implemented in Object-Oriented Cobol. / Computing / M. Sc. (Information Systems)

No description available.

No description available.

En el proceso de diseño se toman decisiones que pueden afectar a la fabricabilidad del producto. Cuando el diseñador es experto, considera las limitaciones, las propiedades y el coste de fabricación en la fase de materialización o de detalle. El problema surge cuando el diseñador no es experto o cuando no hay suficiente información y conocimiento de fabricación disponible. Tomando como referencia la teoría de Diseño Axiomático y las técnicas de DFM, se propone una metodología para identificar, definir y formalizar la información de fabricación que debería estar disponible en el diseño para diseñar para fabricar (DFM). También se propone un prototipo de modelo de información para desarrollar una futura herramienta informática que facilitaría la aplicación de esta metodología y que permitiría guiar al diseñador durante el diseño. La metodología ha sido aplicada a una biela de un motor de combustión interna alternativo (MCIA), y a los procesos que se están usando actualmente para fabricarla: forja en matriz cerrada y forja de polvo de metal. / Experience and knowledge of the designer are key elements during the design process. In the embodiment and detailed design phases is when the expert designers take into account the manufacturing process constraints, capabilities and costs. A problem arises when the designer is inexpert or when not enough manufacturing information and knowledge is available. This work presents a methodology, based on the Axiomatic Design Theory and on DFM techniques, to determine the explicit manufacturing process knowledge that the designer should have to design for manufacturing. This methodology has been the basis to develop the model information approach. This model is the first step to develop software to assist in the methodology application and to guide the designer during the design process. The methodology has been applied to a particular component (connecting rod). The manufacturing processes considered are forging and powder metallurgy, which are the main processes currently used in the manufacturing of connecting rods.

This dissertation investigates the role of specification, refinement and implementation in the software development cycle. Both the structured and object-oriented paradigms are looked at. Particular emphasis is placed on the role of the refinement process. The requirements for the product (system) are determined, the specifications are drawn up, the product is designed, specified, implemented and tested. The stage between the (formal) specification of the system and the implementation of the system is the refinement stage. The refinement process consists out of data refinement, operation refinement, and operation decomposition. In this dissertation, Z, Object-Z and UML (Unified Modelling Language) are used as specification languages and C, C++, Cobol and Object-Oriented Cobol are used as implementation languages. As an illustration a small system, The ITEM System, is specified in Z and UML and implemented in Object-Oriented Cobol. / Computing / M. Sc. (Information Systems)

Especificação de requisitos é reconhecida como como uma atividade critica nos processos de desenvolvimento de software por causa de seu impacto nos riscos do projeto quando mal executada. Um grande conjunto de estudos discute aspectos teóricos, proposições de técnicas e práticas recomendadas para a Engenharia de Requisitos (ER). Para ter sucesso, ER tem que assegurar que requisitos especificados são completos e corretos, o que significa que todas as intenções dos stakeholders são cobertas pelos requisitos e que não existem requisitos desnecessários. Entretanto, a captura precisa das intenções stakeholders continua sendo um desafio e é o maior fator para falhas em projetos de software. Esta dissertação apresenta um novo método denominado “Problem-Based SRS” que tem como objetivo melhorar a qualidade da especificação de requisitos de software (SRS – Software Requirements Specification) no sentido de que os requisitos especificados forneçam uma resposta adequada para os problemas dos clientes reais. Neste método, o conhecimento sobre os requisitos de software é construído a partir do conhecimento sobre os problemas do cliente. O Problem-Based SRS consiste de uma organização de atividades e resultados através de um processo que contem cinco etapas. O método fornece suporte ao time de engenharia de requisitos para analisar sistematicamente o contexto de negócio e especificar os requisitos de software, considerando o vislumbre e a visão do software. Os aspectos de qualidade das especificações são avaliados utilizando técnicas de rastreabilidade e princípios do axiomatic design. Os casos de estudo realizados e apresentados nesta dissertação apontam que o método proposto pode contribuir de forma significativa para uma melhor especificação de requisitos de software. / Requirements specification has long been recognized as critical activity in software development processes because of its impact on project risks when poorly performed. A large amount of studies addresses theoretical aspects, propositions of techniques, and recommended practices for Requirements Engineering (RE). To be successful, RE have to ensure that the specified requirements are complete and correct what means that all intents of the stakeholders in a given business context are covered by the requirements and that no unnecessary requirement was introduced. However, the accurate capture the business intents of the stakeholders remains a challenge and it is a major factor of software project failures. This master’s dissertation presents a novel method referred to as “Problem-Based SRS” aiming at improving the quality of the Software Requirements Specification (SRS) in the sense that the stated requirements provide suitable answers to real customer ́s businesses issues. In this approach, the knowledge about the software requirements is constructed from the knowledge about the customer ́s problems. Problem-Based SRS consists in an organization of activities and outcome objects through a process that contains five main steps. It aims at supporting the software requirements engineering team to systematically analyze the business context and specify the software requirements, taking also into account a first glance and vision of the software. The quality aspects of the specifications are evaluated using traceability techniques and axiomatic design principles. The cases studies conducted and presented in this document point out that the proposed method can contribute significantly to improve the software requirements specification.

Especificação de requisitos é reconhecida como como uma atividade critica nos processos de desenvolvimento de software por causa de seu impacto nos riscos do projeto quando mal executada. Um grande conjunto de estudos discute aspectos teóricos, proposições de técnicas e práticas recomendadas para a Engenharia de Requisitos (ER). Para ter sucesso, ER tem que assegurar que requisitos especificados são completos e corretos, o que significa que todas as intenções dos stakeholders são cobertas pelos requisitos e que não existem requisitos desnecessários. Entretanto, a captura precisa das intenções stakeholders continua sendo um desafio e é o maior fator para falhas em projetos de software. Esta dissertação apresenta um novo método denominado “Problem-Based SRS” que tem como objetivo melhorar a qualidade da especificação de requisitos de software (SRS – Software Requirements Specification) no sentido de que os requisitos especificados forneçam uma resposta adequada para os problemas dos clientes reais. Neste método, o conhecimento sobre os requisitos de software é construído a partir do conhecimento sobre os problemas do cliente. O Problem-Based SRS consiste de uma organização de atividades e resultados através de um processo que contem cinco etapas. O método fornece suporte ao time de engenharia de requisitos para analisar sistematicamente o contexto de negócio e especificar os requisitos de software, considerando o vislumbre e a visão do software. Os aspectos de qualidade das especificações são avaliados utilizando técnicas de rastreabilidade e princípios do axiomatic design. Os casos de estudo realizados e apresentados nesta dissertação apontam que o método proposto pode contribuir de forma significativa para uma melhor especificação de requisitos de software. / Requirements specification has long been recognized as critical activity in software development processes because of its impact on project risks when poorly performed. A large amount of studies addresses theoretical aspects, propositions of techniques, and recommended practices for Requirements Engineering (RE). To be successful, RE have to ensure that the specified requirements are complete and correct what means that all intents of the stakeholders in a given business context are covered by the requirements and that no unnecessary requirement was introduced. However, the accurate capture the business intents of the stakeholders remains a challenge and it is a major factor of software project failures. This master’s dissertation presents a novel method referred to as “Problem-Based SRS” aiming at improving the quality of the Software Requirements Specification (SRS) in the sense that the stated requirements provide suitable answers to real customer ́s businesses issues. In this approach, the knowledge about the software requirements is constructed from the knowledge about the customer ́s problems. Problem-Based SRS consists in an organization of activities and outcome objects through a process that contains five main steps. It aims at supporting the software requirements engineering team to systematically analyze the business context and specify the software requirements, taking also into account a first glance and vision of the software. The quality aspects of the specifications are evaluated using traceability techniques and axiomatic design principles. The cases studies conducted and presented in this document point out that the proposed method can contribute significantly to improve the software requirements specification.

Formal verification of programs can be done with the aid of an interactive theorem prover. The program to be verified is represented in an intermediate language representation inside the interactive theorem prover, after which statements and their proofs can be constructed. This is a process that can be automated to a high degree. This thesis presents a proof procedure to efficiently generate a theorem stating the weakest precondition for a program to terminate successfully in a state upon which a certain postcondition is placed. Specifically, the Poly/ML implementation of the SML metalanguage is used to generate a theorem in the HOL4 interactive theorem prover regarding the properties of a program written in BIR, an abstract intermediate representation of machine code used in the PROSPER project. / Bevis av säkerhetsegenskaper hos program genom formell verifiering kan göras med hjälp av interaktiva teorembevisare. Det program som skall verifieras representeras i en mellanliggande språkrepresentation inuti den interaktiva teorembevisaren, varefter påståenden kan konstrueras, som sedan bevisas. Detta är en process som kan automatiseras i hög grad. Här presenterar vi en metod för att effektivt skapa och bevisa ett teorem som visar sundheten hos den svagaste förutsättningen för att ett program avslutas framgångsrikt under ett givet postvillkor. Specifikt använder vi Poly/ML-implementationen av SML för att generera ett teorem i den interaktiva teorembevisaren HOL4 som beskriver egenskaper hos ett program i BIR, en abstrakt mellanrepresentation av maskinkod som används i PROSPER-projektet.

Es ist eine weit verbreitete Wahrnehmung, dass der Übergang zwischen der Mathematik der gymnasialen Oberstufe und der Mathematik an der Universität für Studierende problematisch sein kann. Besondere Verständnisschwierigkeiten in Bereich der lineare Algebra (lA) bereiten den Studierenden die verschiedenen Herangehensweisen auf diesen beiden Ebenen. Dies lässt sich auf die strukturell-axiomatischer Herangehensweisen an die lA an der Universität, im Gegensatz zu ihrer arithmetisch-geometrischen Darstellung in der Schule, zurückführen. Dies bedingt ebenfalls Unterschiede im prozeduralen und konzeptuellen Verständnis. Ziel dieser Arbeit ist es, zu untersuchen, wie Schüler konzeptuelles Verständnis, Bezug nehmend auf die Theorien von concept definition/image in Verbindung mit multiplen Modi der Beschreibung und des Denkens von Konzepten wie Bilinearität z.B. Skalarprodukt und Multilinearität z.B. Determinanten gewinnen können. Um dies zu erreichen wurde eine substanzielle Lehr-Lernumgebung unter Verwendung einer dynamischen Geometriesoftware (DGS) entwickelt. Die Lerneinheit wurde an einem Berliner Gymnasium eingesetzt und dabei ein vollständiger design-based research Zyklus durchlaufen und eine multiple-level Datenanalyse durchgeführt. Die Ergebnisse der Untersuchung zeigen nicht nur, dass eine Erweiterung der Vorstellungen der Schüler, eine Entwicklung multipler Denkmodi und ein Gewinn tieferen konzeptuellen Verständnisses in der lA erfolgreich vermittelt werden können, sondern geben auch Einblicke in ein mögliches theoretisches Modell, mit dessen Hilfe sich diese Prozesse weiter untersuchen lassen. Weiterhin werden die interaktiven Lehr-Lernmaterialien für die weitere Verwendung im Rahmen von Lehre und Forschung zur Verfügung gestellt. Es öffnen sich neue Forschungsfragen hinsichtlich lokalen Axiomatisierens in der lA der gymnasialen Oberstufe, welches auf einer Integration geometrischer, algebraischer und axiomatischer Denkmodi, unterstützt durch DGS, basieren könnte. / A common perception among researchers in mathematics education is that the transition between secondary- and tertiary level of mathematics may be problematic for the students. In particular, the exact and abstract nature of the theory of Linear algebra versus its arithmetic-geometric presentation in school appears to be difficult for the novice students. The application of properties for defining concepts at university in contrast to their usage for describing concepts in school points out a possible occurrence of obstacles for learning and discrepancies in procedural and conceptual understanding. The aim of this study is to examine how could upper-high school students develop a conceptual understanding based on concept definition and concept image in connection to multiple modes of description and thinking about concepts such as bi-linearity exemplified by the dot product of vectors and multi-linearity exemplified by determinants. In order to achieve this, I have created a specific teaching/ learning sequence in a dynamic geometry environment (DGE), then implemented it and evaluated it in a high school in Berlin, following a complete cycle of design-based research and conducting a multiple-level data analysis. The findings of the study show not only that widening students' concept images, developing multiple modes of thinking and gaining deeper conceptual understanding can successfully be mediated by dynamic geometries, but also give insights into an eventual theoretical model of how can they be further examined. Moreover, the study promotes authorized open-source interactive teaching/ learning materials for further sustainable practice and research. It opens new research questions about revisiting axiomatic approaches on local levels in upper high-school Linear algebra which may base on the integration of all three modes of description and thinking geometric, algebraic and abstract possibly facilitated by DGE. / Честа перцепција кај многумина истражувачи во областа на математичкото образование е дека транзицијата помеѓу средното и високото образование по математика може да биде проблематична за студентите. Егзакноста и апстрактноста на теоријата по Линеарна алгебра наспроти нејзината аритметичко-геометриска презентација во средното гимназиско образование се покажува како особено тешка за студентите. Примена на својствата на математичките поими за нивно дефинирање на универзитетско ниво наспроти нивното употреба за опишување на претходно дефинирани поими на училишно ниво, укажува на можна појава на тешкотии при нивното изучување и несовпаѓање на процедуралното и концептуалното разбирање на истите. Целта на оваа студија е да истражи како средношколците би можеле да развијат концептуално разбирање на поимите врз основа на концепт дефиниција и концепт слика во врска со мулти-моди на мислење, конкретно за поими како билинеарност, пр. скаларен производ на вектори, и мултилинеарност, пр. детерминанти. За да ја постигнам оваа цел, креирав наставна содржина поддржана од еден динамичен геометриски систем (ДГС) и следејќи целосен циклус на т.н. design-based research и спрoведувајќи мулти-анализа на податоци, истата ја имплементирав и евалуирав во едно средно училиште во Берлин. Резултатите од студијата укажуваат не само на фактот дека проширувањето на концепт сликите на учениците, развојот на мулти-моди на мислење и стекнувањето на длабоко концептуално разбирање на поимите можат да бидат успешно посредувани од ДГС туку овозможија и увид во еден теоретски модел за тоа коко тие можат понатаму да се истражуваат. Уште повеќе, студијата промовира авторизирани open-source интерактивни материјали за предавање и учење на содржините кои може да служат за понатамошни одржливи истражувања и развој. Студијата отвора нови истражувачки прашања за средношколската Линеарна алгебра која може да се базира на интеграција на сите три моди на мислење, геометриски, алгебарски и апстрактен, поддржан од ДГС.