A Model-Based Development and Verification Framework for Distributed System-on-Chip Architecture

The capabilities and thus, design complexity of VLSI-based embedded systems have increased tremendously in recent years, riding the wave of Moore’s law. The time-to-market requirements are also shrinking, imposing challenges to the designers, which in turn, seek to adopt new design methods to increase their productivity. As an answer to these new pressures, modern day systems have moved towards on-chip multiprocessing technologies. New architectures have emerged in on-chip multiprocessing in order to utilize the tremendous advances of fabrication technology. Platform-based design is a possible solution in addressing these challenges. The principle behind the approach is to separate the functionality of an application from the organization and communication architecture of hardware platform at several levels of abstraction. The existing design methodologies pertaining to platform-based design approach don’t provide full automation at every level of the design processes, and sometimes, the co-design of platform-based systems lead to sub-optimal systems. In addition, the design productivity gap in multiprocessor systems remain a key challenge due to existing design methodologies. This thesis addresses the aforementioned challenges and discusses the creation of a development framework for a platform-based system design, in the context of the SegBus platform - a distributed communication architecture. This research aims to provide automated procedures for platform design and application mapping. Structural verification support is also featured thus ensuring correct-by-design platforms. The solution is based on a model-based process. Both the platform and the application are modeled using the Unified Modeling Language. This thesis develops a Domain Specific Language to support platform modeling based on a corresponding UML profile. Object Constraint Language constraints are used to support structurally correct platform construction. An emulator is thus introduced to allow as much as possible accurate performance estimation of the solution, at high abstraction levels. VHDL code is automatically generated, in the form of “snippets” to be employed in the arbiter modules of the platform, as required by the application. The resulting framework is applied in building an actual design solution for an MP3 stereo audio decoder application.

Design and validation of stateful composite RESTful web services

A web service is a software system that provides a machine-processable interface to the other machines over the network using different Internet protocols. They are being increasingly used in the industry in order to automate different tasks and offer services to a wider audience. The REST architectural style aims at producing scalable and extensible web services using technologies that play well with the existing tools and infrastructure of the web. It provides a uniform set of operation that can be used to invoke a CRUD interface (create, retrieve, update and delete) of a web service. The stateless behavior of the service interface requires that every request to a resource is independent of the previous ones facilitating scalability. Automated systems, e.g., hotel reservation systems, provide advanced scenarios for stateful services that require a certain sequence of requests that must be followed in order to fulfill the service goals. Designing and developing such services for advanced scenarios with REST constraints require rigorous approaches that are capable of creating web services that can be trusted for their behavior. Systems that can be trusted for their behavior can be termed as dependable systems. This thesis presents an integrated design, analysis and validation approach that facilitates the service developer to create dependable and stateful REST web services. The main contribution of this thesis is that we provide a novel model-driven methodology to design behavioral REST web service interfaces and their compositions. The behavioral interfaces provide information on what methods can be invoked on a service and the pre- and post-conditions of these methods. The methodology uses Unified Modeling Language (UML), as the modeling language, which has a wide user base and has mature tools that are continuously evolving. We have used UML class diagram and UML state machine diagram with additional design constraints to provide resource and behavioral models, respectively, for designing REST web service interfaces. These service design models serve as a specification document and the information presented in them have manifold applications. The service design models also contain information about the time and domain requirements of the service that can help in requirement traceability which is an important part of our approach. Requirement traceability helps in capturing faults in the design models and other elements of software development environment by tracing back and forth the unfulfilled requirements of the service. The information about service actors is also included in the design models which is required for authenticating the service requests by authorized actors since not all types of users have access to all the resources. In addition, following our design approach, the service developer can ensure that the designed web service interfaces will be REST compliant. The second contribution of this thesis is consistency analysis of the behavioral REST interfaces. To overcome the inconsistency problem and design errors in our service models, we have used semantic technologies. The REST interfaces are represented in web ontology language, OWL2, that can be part of the semantic web. These interfaces are used with OWL 2 reasoners to check unsatisfiable concepts which result in implementations that fail. This work is fully automated thanks to the implemented translation tool and the existing OWL 2 reasoners. The third contribution of this thesis is the verification and validation of REST web services. We have used model checking techniques with UPPAAL model checker for this purpose. The timed automata of UML based service design models are generated with our transformation tool that are verified for their basic characteristics like deadlock freedom, liveness, reachability and safety. The implementation of a web service is tested using a black-box testing approach. Test cases are generated from the UPPAAL timed automata and using the online testing tool, UPPAAL TRON, the service implementation is validated at runtime against its specifications. Requirement traceability is also addressed in our validation approach with which we can see what service goals are met and trace back the unfulfilled service goals to detect the faults in the design models. A final contribution of the thesis is an implementation of behavioral REST interfaces and service monitors from the service design models. The partial code generation tool creates code skeletons of REST web services with method pre and post-conditions. The preconditions of methods constrain the user to invoke the stateful REST service under the right conditions and the post condition constraint the service developer to implement the right functionality. The details of the methods can be manually inserted by the developer as required. We do not target complete automation because we focus only on the interface aspects of the web service. The applicability of the approach is demonstrated with a pedagogical example of a hotel room booking service and a relatively complex worked example of holiday booking service taken from the industrial context. The former example presents a simple explanation of the approach and the later worked example shows how stateful and timed web services offering complex scenarios and involving other web services can be constructed using our approach.

Model-based testing of software systems : functionality and performance

Software is a key component in many of our devices and products that we use every day. Most customers demand not only that their devices should function as expected but also that the software should be of high quality, reliable, fault tolerant, efficient, etc. In short, it is not enough that a calculator gives the correct result of a calculation, we want the result instantly, in the right form, with minimal use of battery, etc. One of the key aspects for succeeding in today's industry is delivering high quality. In most software development projects, high-quality software is achieved by rigorous testing and good quality assurance practices. However, today, customers are asking for these high quality software products at an ever-increasing pace. This leaves the companies with less time for development. Software testing is an expensive activity, because it requires much manual work. Testing, debugging, and verification are estimated to consume 50 to 75 per cent of the total development cost of complex software projects. Further, the most expensive software defects are those which have to be fixed after the product is released. One of the main challenges in software development is reducing the associated cost and time of software testing without sacrificing the quality of the developed software. It is often not enough to only demonstrate that a piece of software is functioning correctly. Usually, many other aspects of the software, such as performance, security, scalability, usability, etc., need also to be verified. Testing these aspects of the software is traditionally referred to as nonfunctional testing. One of the major challenges with non-functional testing is that it is usually carried out at the end of the software development process when most of the functionality is implemented. This is due to the fact that non-functional aspects, such as performance or security, apply to the software as a whole. In this thesis, we study the use of model-based testing. We present approaches to automatically generate tests from behavioral models for solving some of these challenges. We show that model-based testing is not only applicable to functional testing but also to non-functional testing. In its simplest form, performance testing is performed by executing multiple test sequences at once while observing the software in terms of responsiveness and stability, rather than the output. The main contribution of the thesis is a coherent model-based testing approach for testing functional and performance related issues in software systems. We show how we go from system models, expressed in the Unified Modeling Language, to test cases and back to models again. The system requirements are traced throughout the entire testing process. Requirements traceability facilitates finding faults in the design and implementation of the software. In the research field of model-based testing, many new proposed approaches suffer from poor or the lack of tool support. Therefore, the second contribution of this thesis is proper tool support for the proposed approach that is integrated with leading industry tools. We o er independent tools, tools that are integrated with other industry leading tools, and complete tool-chains when necessary. Many model-based testing approaches proposed by the research community suffer from poor empirical validation in an industrial context. In order to demonstrate the applicability of our proposed approach, we apply our research to several systems, including industrial ones.

Merellisen taistelutilan mallinnus

Diplomityön tarkoituksena on tuottaa tutkittua tietoa Merivoimien mallinnuspalveluiden kehittämiseksi. Tutkimuksen päämääränä oli laatia mallikuvaus Merellisen taistelutilan mallista. Merellisen taistelutilan malli on tietokoneella suoritettava mallisovellus, jota käytetään simuloimaan taistelua merellisissä olosuhteissa. Merellisen taistelutilan malli laadittiin Merivoimien operatiivisen suunnittelun tarpeisiin. Diplomityö on jatkoa Esiupseerikurssi 65:lla tehdylle Merellisen taistelutilan mallin käyttäjävaatimukset -tutkimustyölle. Tutkimus on luonteeltaan kvalitatiivinen ja perustuu empiiriseen tutkimukseen. Tutkimuksen lähestymistapa on deskriptiivinen. Tutkimusmenetelminä käytettiin kirjallisuustutkimusta, käsiteanalyysia, kyselytutkimusta, perehtymistä sekä suunnittelua. Diplomityössä tutkittiin mallintamisen ja simuloinnin teoriaa, erilaisia menetelmiä asioiden ja ilmiöiden mallintamiseksi, taistelutilaa käsitteenä sekä perehdyttiin UML-mallinnuskielen (Unified Modeling Language) käyttöön mallikuvauksen laadinnassa. Tutkimuksessa selvitettiin kyselytutkimuksella Merivoimien operatiivisen suunnittelun asiantuntijoilta, minkälaisia mallinnuskysymyksiä mallin avulla tulisi ratkaista. Kysymysten perusteella määritettiin asioita ja ilmiöitä, joita kysymysten ratkaisemiseksi on mallinnettava. Asioiden ja ilmiöiden määrittelyn jälkeen tutkittiin erilaisia menetelmiä niiden mallintamiseksi. Tutkimuksen perusteella laadittiin mallikuvaus Merellisen taistelutilan mallista, joka on samalla myös tärkein tutkimustulos.

Docencia práctica en los laboratorios de las ingenierías de informática apoyada en herramientas CASE.

Aceptado para su publicación en las actas del Segundo Taller de trabajo en Ingeniería del Software basada en componentes distribuidos ISCDISï01. En colaboración con VI Jornadas de Ingeniería de Software y Bases de Datos (Almagro, Ciudad Real - 2 de noviembre de 2001)

Modelado de procesos de enseñanza-aprendizaje reutilizables con XML, UML e IMS-LD.

El artículo está incluido en un número monográfico especial con los trabajos del I Simposio Pluridisciplinar sobre Diseño, Evaluación y Descripción de Contenidos Educativos Reutilizables (Guadalajara, Octubre 2004).Resumen tomado de la publicación

Development of a semantic graph-based scene description

Software representations of scenes, i.e. the modelling of objects in space, are used in many application domains. Current modelling and scene description standards focus on visualisation dimensions, and are intrinsically limited by their dependence upon their semantic interpretation and contextual application by humans. In this paper we propose the need for an open, extensible and semantically rich modelling language, which facilitates a machine-readable semantic structure. We critically review existing standards and techniques, and highlight a need for a semantically focussed scene description language. Based on this defined need we propose a preliminary solution, based on hypergraph theory, and reflect on application domains.

Um metamodelo da linguagem de modelagem real time UML, de suporte à criação de dicionário de dados para ferramentas de modelagem de sistema tempo real, visando a verificação de consistência dos modelos

A computação de tempo real é uma das áreas mais desafiadoras e de maior demanda tecnológica da atualidade. Está diretamente ligada a aplicações que envolvem índices críticos de confiabilidade e segurança. Estas características, inerentes a esta área da computação, vêm contribuindo para o aumento da complexidade dos sistemas tempo real e seu conseqüente desenvolvimento. Isto fez com que mecanismos para facilitar especificação, delimitação e solução de problemas passem a ser itens importantes para tais aplicações. Este trabalho propõe mecanismos para atuarem no desenvolvimento de sistemas de tempo real, com o objetivo de serem empregados como ferramenta de apoio no problema da verificação de presença de inconsistências, que podem vir a ocorrer nos vários modelos gerados partir da notação da linguagem de modelagem gráfica para sistemas de tempo real - UML-RT(Unified Modeling Language for Real Time). Estes mecanismos foram projetados através da construção de um metamodelo dos conceitos presentes nos diagramas de classe, de objetos, de seqüência, de colaboração e de estados. Para construir o metamodelo, utiliza-se a notação do diagrama de classes da UML (Unified Modeling Language). Contudo, por intermédio das representações gráficas do diagrama de classes não é possível descrever toda a semântica presente em tais diagramas. Assim, regras descritas em linguagem de modelagem OCL (Object Constraint Language) são utilizadas como um formalismo adicional ao metamodelo. Com estas descrições em OCL será possível a diminuição das possíveis ambigüidades e inconsistências, além de complementar as limitações impostas pelo caráter gráfico da UML. O metamodelo projetado é mapeado para um modelo Entidade&Relacionamento. A partir deste modelo, são gerados os scripts DDL (Data Definition Language) que serão usados na criação do dicionário de dados, no banco de dados Oracle. As descrições semânticas escritas através de regras em OCL são mapeadas para triggers, que disparam no momento em que o dicionário de dados é manipulado. O MET Editor do SiMOO-RT é a ferramenta diagramática que faz o povoamento dos dados no dicionário de dados. SiMOO-RT é uma ferramenta orientada a objetos para a modelagem, simulação e geração automática de código para sistemas de tempo real.

Agentes de software nas empresas : um estudo de caso na área de compras

Com o aumento de informações disponíveis e das possibilidades de fazer comércio por meios eletrônicos, aumenta a complexidade de algumas tarefas, como comprar. Um dos possíveis caminhos para diminuir essa complexidade é dotar programas de computadores com conhecimentos sobre a realização de tais tarefas, incluindo como tomar decisões. Esta dissertação versa sobre a utilização de agentes de software nas empresas, que são programas de computadores delegados para a realização de funções específicas. Além de uma revisão sobre o atual uso de tais tecnologias, apresenta-se uma possível aplicação na área de Compras para uma empresa real. Para modelar o sistema proposto, utilizou-se uma extensão da Unified Modeling Language (UML), a Agent UML, que objetiva a adequação da primeira para representar sistemas multiagentes. As dificuldades encontradas para modelagem são uma discussão adicional, bem como as sugestões. Outras contribuições do presente trabalho são as apresentações de mecanismos de decisão e de negociação para a Função Compras, inspirados em funções de valor e na negociação colaborativa. Encerra-se, apontando algumas futuras direções, incentivando reflexões posteriores sobre este tema pioneiro na Escola de Administração da Universidade Federal do Rio Grande do Sul.

Um Modelo de simulação de processos de software baseado em conhecimento para o ambiente PROSOFT

Construção de software com qualidade tem motivado diversas pesquisas na área de Engenharia de Software. Problemas como a grande complexidade requerida pelas aplicações atuais e a necessidade de gerenciamento de um número cada vez maior de pessoas envolvidas em projetos são obstáculos para serem transpostos. Trabalhos relacionados a tecnologia de processos de software aparecem como uma proposta para se obter maior controle das atividades realizadas com o intuito de se obter maior qualidade. A simulação de processos de software, através da representação dos passos definidos em um modelo, tem sido utilizada no auxílio a gerentes de projetos de sistemas para fornecer-lhes informações preciosas sobre o desenvolvimento de um sistema especificado. A representação de conhecimento a respeito das características relacionadas a um ambiente de desenvolvimento ajuda na obtenção de simulações mais realísticas. A partir do modelo, o simulador obtém uma descrição do ambiente em que deve atuar, baseado no conhecimento que se tem a respeito do ambiente. Esse trabalho apresenta um modelo de simulação de processos de software baseado em conhecimento para ser inserido em um ambiente de engenharia de processos de software. A função do modelo é simular um processo de software instanciado, procurando detectar inconsistências no mesmo que possam gerar problemas durante a sua execução, como aumento de custos e comprometimento da qualidade do(s) produto(s) obtido(s). Após a simulação o projetista pode constatar a necessidade de se refazer o modelo, ajustar parâmetros ou executar o processo de software. O objetivo da simulação, nesse trabalho, é auxiliar as pessoas responsáveis por um ambiente de desenvolvimento a obter modelos de processos validados. O modelo de simulação foi definido para ser utilizado no ambiente PROSOFT, que é um ambiente de desenvolvimento que permite a integração de novas ferramentas para desenvolvimento de software. O ambiente PROSOFT vem recebendo propostas de extensão que tem contribuído para o seu aprimoramento, fornecendo para seus usuários uma quantidade cada vez maior de ferramentas de auxílio a construção de artefatos de software. As propostas mais recentes foram um modelo para construção de sistemas especialistas, a definição de um ambiente cooperativo e um gerenciador de processos de software. ATOs algébricos (construções do PROSOFT) são utilizados para especificar formalmente o modelo de simulação definido neste trabalho. A validação é realizada através de um modelo em UML (Unified Method Language) que foi utilizado como base para a construção de um programa implementado usando a linguagem Java. Isso ocorre porque a ferramenta do PROSOFT (implementada em Java) que seria utilizada para validar as especificações algébricas ainda não está finalizada.

Goals Software Construction Process

Generalized hyper competitiveness in the world markets has determined the need to offer better products to potential and actual clients in order to mark an advantagefrom other competitors. To ensure the production of an adequate product, enterprises need to work on the efficiency and efficacy of their business processes (BPs) by means of the construction of Interactive Information Systems (IISs, including Interactive Multimedia Documents) so that they are processed more fluidly and correctly.The construction of the correct IIS is a major task that can only be successful if the needs from every intervenient are taken into account. Their requirements must bedefined with precision, extensively analyzed and consequently the system must be accurately designed in order to minimize implementation problems so that the IIS isproduced on schedule and with the fewer mistakes as possible. The main contribution of this thesis is the proposal of Goals, a software (engineering) construction process which aims at defining the tasks to be carried out in order to develop software. This process defines the stakeholders, the artifacts, and the techniques that should be applied to achieve correctness of the IIS. Complementarily, this process suggests two methodologies to be applied in the initial phases of the lifecycle of the Software Engineering process: Process Use Cases for the phase of requirements, and; MultiGoals for the phases of analysis and design. Process Use Cases is a UML-based (Unified Modeling Language), goal-driven and use case oriented methodology for the definition of functional requirements. It uses an information oriented strategy in order to identify BPs while constructing the enterprise’s information structure, and finalizes with the identification of use cases within the design of these BPs. This approach provides a useful tool for both activities of Business Process Management and Software Engineering. MultiGoals is a UML-based, use case-driven and architectural centric methodology for the analysis and design of IISs with support for Multimedia. It proposes the analysis of user tasks as the basis of the design of the: (i) user interface; (ii) the system behaviour that is modeled by means of patterns which can combine Multimedia and standard information, and; (iii) the database and media contents. This thesis makes the theoretic presentation of these approaches accompanied with examples from a real project which provide the necessary support for the understanding of the used techniques.

Geração automática de interfaces com o utilizador: uma abordagem baseada em MDA para a plataforma PHP

Os modelos e as técnicas de modelação são, hoje em dia, fundamentais na engenharia de software, devido à complexidade e sofisticação dos sistemas de informação actuais.A linguagem Unified Modeling Language (UML) [OMG, 2005a] [OMG, 2005b] tornou-se uma norma para modelação, na engenharia de software e em outras áreas e domínios, mas é reconhecida a sua falta de suporte para a modelação da interactividade e da interface com o utilizador [Nunes and Falcão e Cunha, 2000].Neste trabalho, é explorada a ligação entre as áreas de engenharia de software e de interacção humano-computador, tendo, para isso, sido escolhido o processo de desenvolvimento Wisdom [Nunes and Falcão e Cunha, 2000] [Nunes, 2001]. O método Wisdom é conduzido por casos de utilização essenciais e pelo princípio da prototipificação evolutiva, focando-se no desenho das interfaces com o utilizador através da estrutura da apresentação, com a notação Protótipos Abstractos Canónicos (PAC) [Constantine and Lockwood, 1999] [Constantine, 2003], e do comportamento da interacção com a notação ConcurTaskTrees (CTT) [Paternò, 1999] [Mori, Paternò, et al., 2004] em UML.É proposto, também, neste trabalho um novo passo no processo Wisdom, sendo definido um modelo específico, construído segundo os requisitos da recomendação Model Driven Architecture (MDA) [Soley and OMG, 2000] [OMG, 2003] elaborada pela organização Object Managent Group (OMG). Este modelo específico será o intermediário entre o modelo de desenho e a implementação da interface final com o utilizador. Esta proposta alinha o método Wisdom com a recomendação MDA, tornando possível que sejam gerados, de forma automática, protótipos funcionais de interfaces com o utilizador a partir dos modelos conceptuais de análise e desenho.Foi utilizada a ferramenta de modelação e de metamodelação MetaSketch [Nóbrega, Nunes, et al., 2006] para a definição e manipulação dos modelos e elementos propostos. Foram criadas as aplicações Model2Model e Model2Code para suportar as transformações entre modelos e a geração de código a partir destes. Para a plataforma de implementação foi escolhida a framework Hydra, desenvolvida na linguagem PHP [PHP, 2006], que foi adaptada com alguns conceitos de modo a suportar a abordagem defendida neste trabalho.

JML- Based formal development of a Java card application for managing medical appointments

Although formal methods can dramatically increase the quality of software systems, they have not widely been adopted in software industry. Many software companies have the perception that formal methods are not cost-effective cause they are plenty of mathematical symbols that are difficult for non-experts to assimilate. The Java Modelling Language (short for JML) Section 3.3 is an academic initiative towards the development of a common formal specification language for Java programs, and the implementation of tools to check program correctness. This master thesis work shows how JML based formal methods can be used to formally develop a privacy sensitive Java application. This is a smart card application for managing medical appointments. The application is named HealthCard. We follow the software development strategy introduced by João Pestana, presented in Section 3.4. Our work influenced the development of this strategy by providing hands-on insight on challenges related to development of a privacy sensitive application in Java. Pestana’s strategy is based on a three-step evolution strategy of software specifications, from informal ones, through semiformal ones, to JML formal specifications. We further prove that this strategy can be automated by implementing a tool that generates JML formal specifications from a welldefined subset of informal software specifications. Hence, our work proves that JML-based formal methods techniques are cost-effective, and that they can be made popular in software industry. Although formal methods are not popular in many software development companies, we endeavour to integrate formal methods to general software practices. We hope our work can contribute to a better acceptance of mathematical based formalisms and tools used by software engineers. The structure of this document is as follows. In Section 2, we describe the preliminaries of this thesis work. We make an introduction to the application for managing medical applications we have implemented. We also describe the technologies used in the development of the application. This section further illustrates the Java Card Remote Method Invocation communication model used in the medical application for the client and server applications. Section 3 introduces software correctness, including the design by contract and the concept of contract in JML. Section 4 presents the design structure of the application. Section 5 shows the implementation of the HealthCard. Section 6 describes how the HealthCard is verified and validated using JML formal methods tools. Section 7 includes some metrics of the HealthCard implementation and specification. Section 8 presents a short example of how a client-side of a smart card application can be implemented while respecting formal specifications. Section 9 describes a prototype tools to generate JML formal specifications from informal specifications automatically. Section 10 describes some challenges and main ideas came acrorss during the development of the HealthCard. The full formal specification and implementation of the HealthCard smart card application presented in this document can be reached at https://sourceforge.net/projects/healthcard/.

A JML-Based strategy for incorporating formal specifications into the software development process

This thesis presents a JML-based strategy that incorporates formal specifications into the software development process of object-oriented programs. The strategy evolves functional requirements into a “semi-formal” requirements form, and then expressing them as JML formal specifications. The strategy is implemented as a formal-specification pseudo-phase that runs in parallel with the other phase of software development. What makes our strategy different from other software development strategies used in literature is the particular use of JML specifications we make all along the way from requirements to validation-and-verification.