Safety-critical systems are systems in which failure may lead to serious harm for humans or the environment. Due to the nature of these systems, there exist regulatory standards that recommend a set of safety mechanisms that should be included in these systems, e.g., IEC 61508. However, these standards offer little to no implementation assistance for these mechanisms. This thesis provides such development assistance, by proposing an approach for the automatic generation of safety mechanisms via Model-Driven Development (MDD). Such an automation of previously manual activities has been known to increase developer productivity and to reduce the number of bugs in the implementation. In the context of safety-critical systems, the latter also means an improvement in safety. The approach introduces a novel way to define safety requirements as structured sentences. This structure allows for the automatic parsing of these requirements in order to subsequently generate software-implemented safety mechanisms, as well as to initially configure hardware-implemented safety mechanisms. The generation approach for software-implemented safety mechanisms uses Unified Modeling Language (UML) stereotypes to represent these mechanisms in the application model. Automated model-to-model transformations parse this model representation and realize the safety mechanisms within an intermediate model. From this intermediate model, code may be generated with simple 1:1 mappings. For the generation of hardware-implemented safety mechanisms, this thesis introduces a novel Graphical User Interface (GUI) tool for representing the configuration of hardware interfaces. A template-based code snippet repository is used for generating the code responsible for the configuration of the hardware-implemented safety mechanisms. The presented approach is validated by applying it to the development of a safety-critical fire detection application example. Furthermore, the runtime overhead of the respective transformation steps of the code generation process is measured. The results indicate a linear scalability and a runtime that is no impediment to the workflow of the developer. Furthermore, the memory and runtime overhead of the generated code is evaluated. The results show that the inclusion of a single safety mechanism for a single system element has a negligible overhead. However, the relative overhead indicates that the application of safety mechanisms should be limited to those system elements that are strictly safety-critical, as their arbitrary application to all system elements would have large effects on the runtime and memory usage of the application.

Master of Science / Department of Computing and Information Sciences / John Hatcliff / Medical devices are safety-critical systems whose failure may put human life in danger. They are becoming more advanced and thus more complex. This leads to bigger and more complicated code-bases that are hard to maintain and verify. Model-driven development provides high-level and abstract description of the system in the form of models that omit details, which are not relevant during the design phase. This allows for certain types of verification and hazard analysis to be performed on the models. These models can then be translated into code. However, errors that do not exist in the models may be introduced during the implementation phase. Automated translation from verified models to code may prevent to some extent. This thesis proposes approach for model-driven development and verification of medical devices. Models are created in AADL (Architecture Analysis & Design Language), a language for software and hardware architecture modeling. AADL models are translated to SPARK Ada, contract-based programming language, which is suitable for software verification. Generated code base is further extended by developers to implement internals of specific devices. Created programs can be verified using SPARK tools. A PCA (Patient Controlled Analgesia) pump medical device is used to illustrate the primary artifacts and process steps. The foundation for this work is "Integrated Clinical Environment Patient-Controlled Analgesia Infusion Pump System Requirements" document and AADL Models created by Brian Larson. In addition to proposed model-driven development approach, a PCA pump prototype was created using the BeagleBoard-xM device as a platform. Some components of PCA pump prototype were verified by SPARK tools and Bakar Kiasan.

近年來，模型驅動的軟體開發方式已在軟體開發社群引起廣泛的討論與研究。知名的物件管理組織並提出模型驅動架構來推廣這種新的軟體開發方式。一般使用模型驅動架構觀念的開發方法多著重在模型交換、模型變更及產生程式碼的精準度，但對於應用樣板程式在產生程式的使用上卻很少有特別的規範，故本研究選擇樣板程式的應用進行探討。在模型建構方面，我們依循一般將業務性及非業務性的模型分開設計及管理的方式，以方便系統開發人員在設計模型時，可以專注於業務性的功能設計，非業務性的功能便可依系統的需求選擇特定的組合；但在程式碼產生部分，本研究則應用剖面導向程式設計中的織入方式來產生程式碼。我們以Orr, Doug所製作的原型程式為基礎，建立一個應用剖面樣板於模型驅動開發的流程，並且以一個應用實例及使用工具來闡明整體導入的過程及運用價值。經由這樣的實例，可以讓系統開發者感受應用剖面樣板於模型驅動開發所帶來的方便及效率的提昇。 / Recently, model-driven software development has attracted great attention from the software development community. The Object Management Group (OMG) has also proposed the so-called Model-Driven Architecture (MDA) to promote it. As far as we know, most system development approaches using the MDA concept emphasize on model exchange, model change and degree of preciseness on code generation and do not discuss much about the usage of templates for code generation. Therefore, this research proposes to study the code generation part of MDA using templates. Like other MDA-based approaches, our development process also design and manage functional models and non-functional models separately, allowing system developers to focus on functional models design and to easily choose existing functions for non-functional models by requirements. What makes our approach different is we add an attachment model which facilitates the code generation steps by using the weaving mechanism found in aspect-oriented programming (AOP). In this study, we elaborate the attachment model proposed by Orr, Doug and propose an example of model-driven development process using it for code generation. Moreover, we utilize the prototype of Orr, Doug’s to create a complete example which re-engineers an existing application by replacing its system platform and extending its business functions using this process.

The research presented in this thesis is aimed at developing reliable information systems through the application of model-driven and formal techniques. These are techniques in which a precise, formal model of system behaviour is exploited as source code. As such a model may be more abstract, and more concise, than source code written in a conventional programming language, it should be easier and more economical to create, to analyse, and to change. The quality of the model of the system can be ensured through certain kinds of formal analysis and fixed accordingly if necessary. Most valuably, the model serves as the basis for the automated generation or configuration of a working system. This thesis provides four research contributions. The first involves the analysis of a proposed modelling language targeted at the model-driven development of information systems. Logical properties of the language are derived, as are properties of its compiled form---a guarded substitution notation. The second involves the extension of this language, and its semantics, to permit the description of workflows on information systems. Workflows described in this way may be analysed to determine, in advance of execution, the extent to which their concurrent execution may introduce the possibility of deadlock or blocking: a condition that, in this context, is synonymous with a failure to achieve the specified outcome. The third contribution concerns the validation of models written in this language by adapting existing techniques of software testing to the analysis of design models. A methodology is presented for checking model consistency, on the basis of a generated test suite, against the intended requirements. The fourth and final contribution is the presentation of an implementation strategy for the language, targeted at standard, relational databases, and an argument for its correctness, based on a simple, set-theoretic semantics for structure and operations.

Automatically generating a program from its specification eliminates a large source of errors that is often unavoidable in a manual approach. While a general purpose code generator is impossible to build, it is possible to build a practical code generator for a specific domain. This thesis investigates the theory behind Booster — a domain specific, object based specification language and automatic code generator. The domain of Booster is information systems — systems that consist of a rich object model in which the objects refer to each other to form a complicated network of associations. The operations of such systems are conceptually simple (changing the attributes of objects, adding or removing new objects and creating or destroying associations) but they are tricky to implement correctly. The thesis focuses on the theoretical foundation of the Booster approach, in particular on three contributions: semantics, model completion, and code generation. The semantics of a Booster model is a single abstract data type (ADT) where the invariants and the methods of all the classes in the model are promoted to the level of the ADT. This is different from the traditional view that considers each class as a separate ADT. The thesis argues that the Booster semantics is a better model of object oriented systems. The second important contribution is the idea of model completion — a process that augments the postconditions of methods with additional predicates that follow from the system’s invariant and the method’s original intention. The third contribution describes a simple but effective code generation technique that is based on interpreting postconditions as executable statements and uses weakest preconditions to ensure that the generated code refines its specification.

[pt] Hoje em dia é incontável o volume aplicações desenvolvidas para a World Wide Web. Essas aplicações possuem interfaces com o usuário que devem ser capazes de se adaptar a diversas situações de uso, mudanças de contexto e conteúdo e ainda ser compatíveis com vários navegadores e dispositivos. Além disso, o projeto e a manutenção de interfaces que necessitam de adaptações em função das regras de negócio da aplicação demandam boa parte do esforço exigido durante do ciclo de vida do desenvolvimento de uma aplicação. Para auxiliar no projeto dessas interfaces, algumas UIDL s (User Interfaces Description Languages) foram propostas com o intuito de oferecer um nível de abstração para que o projetista não precise focar a atenção em aspectos mais concretos durante o desenvolvimento de uma interface. Esse trabalho apresenta uma proposta para modelagem e geração de interfaces de aplicações web baseadas em regras de produção. Essas regras definem critérios para as situações de: acionamento de uma interface, seleção dos elementos que participam da composição abstrata e do mapeamento dos widgets concretos que serão utilizados na etapa de renderização. Essa proposta contempla um método para modelagem das interfaces, uma arquitetura de implementação e um ambiente de autoria e execução dos modelos de interface. Também será apresentada uma arquitetura para construção de widgets concretos, uma máquina de interpretação e renderização de interfaces. O objetivo geral da proposta é conseguir projetar interfaces mais sensíveis aos dados e aos contextos de uso, cobrir certas situações de adaptação e gerar interfaces mais flexíveis e reutilizáveis. / [en] Today there is a countless number of applications developed for the World Wide Web. These applications have user interfaces that should be able to adapt to several usage scenarios, content and context changes and also to be compatible with multiple browsers and devices. Furthermore, the design and maintenance of interfaces that need adjustments depending on the business rules of the application require much effort during the development life cycle of an application. In order to assist in the design of these interfaces, some UIDL s (User Interface Description Languages) have been proposed aiming at providing a level of abstraction so that the designer does not need to immediately focus attention on concrete aspects during the development of an interface. This work presents a proposal for modeling and generating interfaces of web applications based on production rules. These rules define criteria for situations determining the activation of an interface; for the selection the elements that participate in the abstract composition and also for the mapping of specific widgets that will be used in the rendering stage. The proposal contemplates a method for modeling interfaces, an implementation architecture and a framework for authoring and execution of the proposed interface models. An architecture is also presented for building widgets as well as a concrete interface interpretation and rendering machine from a hierarchy specification. The overall goal of the proposal is to design interfaces more responsive to data and contexts of use, including situations of adaptation, generating more flexible and reusable interfaces.

Verteilte Kommunikationssysteme haben in den letzten Jahren enorm an Bedeutung gewonnen, insbesondere durch die Vielzahl von Anwendungen in unserem Alltag. Die Heterogenität der Anwendungen und Anwendungsdomänen spricht für die Komplexität solcher Systeme und verdeutlicht die Herausforderungen, mit denen ihre Entwickler konfrontiert sind. Der Schwerpunkt dieser Arbeit liegt auf der Unterstützung des Entwicklungsprozesses von Anwendungen für verteilte Kommunikationssysteme. Es gibt zwei Aspekte, die dabei berücksichtigt werden müssen. Der erste und offensichtlichste ist die Unterstützung der Entwicklung der Anwendung selbst, die letztendlich auf der vorhandenen verteilten Kommunikationsinfrastruktur bereitgestellt werden soll. Der zweite weniger offensichtliche, aber genauso wichtige Aspekt besteht in der Analyse der Anwendung vor ihrer eigentlichen Installation. Anwendungsentwicklung und analyse sind also "zwei Seiten der gleichen Medaille". Durch die Berücksichtigung beider Aspekt erhöht sich jedoch andererseits der Aufwand bei der Entwicklung. Die Arbeit kombiniert und erweitert vorhandene Technologien entsprechend dem modellgetriebenen Entwicklungsparadigma zu einer einheitlichen Entwicklungsmethode. Die Eigenschaften der Anwendung werden in einer vereinheitlichten Beschreibung erfasst, welche sowohl die automatische Überführung in Installationen auf echten Infrastrukturen erlaubt, als auch die Analyse auf der Basis von Modellen. Darüber hinaus wird der Entwicklungsprozess mit zusätzlicher Unterstützung bei der Visualisierung der Analyse ergänzt. Die Praktikabilität des Ansatzes wird anschließend anhand der Entwicklung und Analyse einer Anwendung zur Erdbebenfrühwarnung unter Beweis gestellt. / Distributed communication systems have gained a substantial importance over the past years with a large set of examples of systems that are present in our everyday life. The heterogeneity of applications and application domains speaks for the complexity of such systems and the challenges that developers are faced with. The focus of this dissertation is on the development of applications for distributed communication systems. There are two aspects that need to be considered during application development. The first and most obvious is the development of the application itself that will be deployed on the existing distributed communication infrastructure. The second and less obvious, but equally important, is the analysis of the deployed application. Application development and analysis are like "two sides of the the same coin". However, the separation between the two increases the cost and effort required during the development process. Existing technologies are combined and extended following the model-driven development paradigm to obtain a unified development method. The properties of the application are captured in a unified description which drives automatic transformation for deployment on real infrastructures and/or analysis. Furthermore, the development process is complemented with additional support for visualization to aid analysis. The defined approach is then used in the development of an alarming application for earthquake early warning.

Especificações formais são úteis para descrever o que um sistema deve fazer sem definir como, e, em virtude da sua natureza formal e da possibilidade de abstração, é possível analisá-las sistematicamente. No entanto, o uso de especificações formais como parte do desenvolvimento de software não constitui prática comum. Isso se dá, em parte, pelo fato de existirem apenas um pequeno número de metodologias e ferramentas adequadas que dêem suporte a esse desenvolvimento. O primeiro objetivo deste trabalho é propor uma metodologia de desenvolvimento que possibilite, a partir de uma especificação formal em notação Z, produzir uma implementação dessa especificação em Java. Essa metodologia centra-se na geração do esqueleto da aplicação Java e na instrumentação desse esqueleto com mecanismos de verificação de condições (invariantes, pré e pós-condições) e rastreamento de violações dessas condições. Através desses mecanismos, possibilita-se intercalar desenvolvimento formal e informal no processo global de desenvolvimento de software. O segundo objetivo é desenvolver uma ferramenta que implemente parte dessa metodologia, produzindo uma implementação parcial que deverá ser complementada pelo usuário. / Formal specifications are useful for describing what a system should do, without defining how, and, owing to its formal nature, it is possible to analyse them systematically. However useful formal specifications are, their usage as part of the software development process is rather rare. This is, in part, due to the scarcity of both methodologies and tools that support this development. The first goal of this work is to define a software development methodology that enables the developer to produce a Java application from a formal specification written in Z. This methodology will rely strongly on the generation of Java application skeletons and instrumentation of the generated code with means of verifying conditions (invariants, pre and post-conditions) e tracing violations of these conditions. Through this mechanisms, it is possible to mix formal and informal development in the global software development process. The second goal of this work is to develop a tool that will implement part of this methodology, producing a partial implementation that must be complemented by the developer.

Modeliais grįstas programų kūrimas yra vienas naujausių abstrakcijos pakėlimo būdų programų kūrimo procese. Jis kai kuriais atvejais leidžia pagreitinti programų kūrimo procesą net iki 10 kartų. Šiame darbe analizuojamas dviejų modeliais grįstų metodų taikymas dokumentų valdymo sistemų kūrime – tai apibendrinta modeliais grįsta architektūra (MDA) ir dalykinei sričiai specifinis modeliavimas (DSM). Darbe rasite tiek teorinius šios temos aspektus, tiek ir praktinius bandymus. Teorinėje dalyje apibrėžta dokumentų valdymo sistema – jos pagrindinės funkcijos bei savybės. Taip pat išskirti pagrindiniai modeliais grįstų metodų privalumai ir trūkumai. Praktinių bandymų metu atsiskleidžia tikroji metodams skirtų palaikyti įrankių vertė. MDA įrankių atveju realiai pamatysite, kokios pagalbos galima laukti iš jų spartinant programų kūrimą. Tuo tarpu analizuojant DSM galimybes buvo sukurtas pilnai funkcionuojantis įrankis skirtas dokumentų valdymo sistemoms kurti, kuris leidžia sumodeliuoti dokumentų valdymo sistemų duomenų sluoksnį, sugeneruoti jo kodą bei duomenų bazių schemą. DSL kalbos kūrimo žingsnių aprašymas gali būti naudojamas kaip pagrindas kitų dalykinių sričių kalbų kūrimui, o sukurta kalba gali būti praplėsta iki tokio lygio, kokio reikia, ir naudojama dokumentų valdymo sistemų kūrime. / Model Driven Development is one of the newest ways to increase level of abstraction in software development process. In some cases it allows to increase productivity up to 10 times. This work analyzes usage of two model driven methods in the creation of document management systems. They are, unified Model Driven Architecture (MDA) and Domain Specific Modeling (DSM). You will find both, theoretical and practical aspects of this topic. Theoretical part consists of a definition of document management system, its functions and characteristics. It also contains main advantages and drawbacks of model driven methods. During practical experiments the real value of method supporting tools is revealed. In case of MDA tools, you will see what help can you expect while increasing productivity. Whereas while analyzing DSM possibilities the fully functional tool for modeling document systems was created. It allows creating a model of a data layer, generating its source code and database scheme. The description of DSL creation steps can be used as a base for other domains, and created language can be extended as much as needed and used to create document management systems.

Statische Codemetriken sind wichtige Indikatoren für die Qualität eines Softwaresystems. Sie beleuchten dabei unterschiedliche Aspekte eines Softwaresystems. Deshalb ist es notwendig, mehrere Codemetriken zu nutzen, um die Qualität eines Softwaresystems in seiner Gesamtheit bewerten zu können. Wünschenswert wäre zudem eine Darstellung, die die Struktur des Gesamtsystems und die Bewertung einzelner Elemente eines Softwaresystems in einer Darstellung kombiniert. Die Arbeit untersucht deshalb, welche Metaphern geeignet sind, um eine solche Darstellung zu ermöglichen. Ein zweites Ziel der Arbeit war es, eine solche Visualisierung automatisch erzeugen zu können. Dafür wurde ein Generator entwickelt, der diese Anforderung erfüllt. Zur Konzeption dieses Generators kamen Techniken aus der generativen Softwareentwicklung zum Einsatz. Bei der Umsetzung des Generators wurde auf Techniken aus der modellgetriebenen Softwareentwicklung zurückgegriffen, vor allem auf Techniken aus dem openArchitectureWare-Framework. Der Generator kann in Eclipse eingebunden werden und ist in der Lage, aus einem Java-Projekt die Struktur und die Metrikwerte automatisch zu extrahieren. Diese Werte werden daraufhin in ein dreidimensionales Modell überführt, das auf dem offenen Extensible 3D Standard basiert. Der Generator ermöglichte zudem die Evaluierung zweier unterschiedlicher Metaphern, die im Rahmen der Arbeit durchgeführt wurde.