Catálogo de publicaciones - libros

Due to their increasing complexity, design of software systems is not becoming easier. Furthermore, modern applications ranging from enterprise to embedded systems require very high levels of correctness and dependability assurance. The most effective means to handle complexity is and , and assurance of correctness requires and . When separation of concerns splits the model into several parts, an important issue is to ensure consistency among these parts. We propose an approach supporting separation of concerns and consistent and incremental modelling of requirements.

The refinement process of component designs is one of the basic building blocks for systematic component-based development. In this process, identifying inconsistent specifications of interactions among refined and refining components can be a critical issue for system safety and/or reliability.

To efficiently identify interaction inconsistencies, we have been developing a consistency checking framework integrated into the model-driven component-based development methodology , using model checking as a debugging tool. We introduce our notion of interaction consistency, propose a general framework for integrating the consistency checking mechanism into the refinement process, and demonstrate how the efficiency of identifying inconsistencies can be improved through abstractions.

The dependability of component-based systems mainly relies on the ability to guarantee the safe collaboration of components. Many specification formalisms can then be used and we argue that such specifications should be organized through an appropriate contract model so that guarantees and possible violations can be better exploited. In this paper, we propose a versatile contract model that explicitly reifies the assumptions and guarantees of some behavioral specifications on component assemblies. We briefly illustrate the integration of executable assertions and we detail how can be integrated in the contract model.

The requirements for a system are often specified as textual use cases. Although they are written in natural language, the simple and uniform sentence structure used makes automated processing of use cases feasible. However, the numerous use case approaches vary in the permitted complexity and variations of sentence structure. Frequently, use cases are written in the form of compound sentences describing several actions. While there are methods for analyzing use cases following the very simple SVDPI (subject-verb-direct object ... indirect object) pattern, methods for more complex sentences are still needed. We propose a new method for processing textual requirements based on the scheme earlier described in [13]. The new method allows to process the commonly used complex sentence structures, obtaining more descriptive behavior specifications, which may be used to verify and validate requirements and to derive the initial design of the system.

To reduce the complexities of SQL query generation and increase the flexibilities of user interface, we propose a dialogue-based NLIDB system. The system classifies users’ intentions into domain actions (pairs of a speech act and a concept sequence) using a maximum entropy model. Based on the classification results, the system fills up predefined SQL templates and generates proper SQL queries for natural language interface. In the experiment, the system showed the success rate of 83.4% for SQL generation.

Fault-tolerance has gained renewed importance with the proliferation of high-performance clusters. However, fault-tolerant systems have not yet been widely adopted commercially because they are either hard to deploy, hard to use, hard to manage, hard to maintain, or hard to justify. We have developed , a practical and easily-deployable multiple fault-tolerant MPI system for Myrinet, to satisfy the demand for a fault-tolerant system.

In this paper, we run rigorous tests using real-world applications to validate that can be used in commercial clusters. We also describe improvements made to our system to solve various problems that arose when deploying it on a commercial cluster.

This paper models our system’s checkpoint overhead and presents the results of a series of tests using computation- and communication-intensive MPI applications used commercially in various fields of science. The experimental results show that not only does our system conform to various types of running environment well, but that it can also be practically deployed in commercial clusters.

Interaction systems are a formal model for component-based systems. Combining components via connectors to form more complex systems may give rise to deadlock situations. Deciding the existence of deadlocks is NP-hard as it involves global state analysis. We present here a parametrized polynomial-time algorithm that is able to confirm deadlock-freedom for a certain class of interaction systems. The discussion includes characteristic examples and displays the role of the parameter of the algorithm.

In the paper, we propose an approach to an automatic extraction of verification models for the C language source code. We primarily focus on the representation of pointers and arrays, which make the extraction from the C language specific. We provide an implementation of the model extractor as a part of our broader effort to develop a verifier of Windows kernel drivers based on the Zing model checker. To demonstrate the feasibility of our approach, we give examples of the extraction results on a practical synchronization problem.

Delivering and maintaining dependable component-based systems within budget is a significant practical challenge. Best practice even in large organisations is only just starting to move beyond simple testing for verification of performance and reliability.

The eCAP(-CBCS) project, a collaboration between ABB Corporate Research and Monash University, Australia, seeks to extend research in architectural modelling and analysis, and apply it to distributed, embedded control systems. Background theory developed by Monash’s Distributed Systems and Software Engineering group includes generic models for composing component interaction protocols, behaviours, types and properties such as reliability and execution time.

The project produced a prototype to detect and diagnose excessive peak load in controllers caused by high task worst-case execution time / interval time ratios. Development incorporated typical business and technical requirements, both functional and extra-functional, e.g., integration into an existing development platform, prediction strategy to cope with components without source, usability, and adequate analyser performance.

Lessons learned and observations include: applications for software metrics and profile visualisation techniques; design refinements such as component type parameterisation for accurate, context-sensitive component property analyses, and; ideas for exploiting underlying theory such as context-sensitive model-driven performance testing.

The increasing complexity of today’s embedded systems applications imposes the requirements and constraints of distributed, heterogeneous subsystem interaction to software engineers. These requirements are well met by the component based software engineering paradigm: complex software is decomposed into coherent, interacting units of execution, the so called components. Connectors are a commonly used abstraction to model the interaction between them. We consequently contribute with the application of explicit connectors for distributed embedded systems software. Explicit connectors encapsulate the logic of distributed interaction, hence they provide well defined contracts regarding properties of inter-component communication. Our approach allows model level validation of component composition and interaction incorporating communication related constraints beyond simple interface matching. In addition, by using explicit connectors, the complexity of application components is reduced without the need for any heavy weight middleware. In fact, the set of all deployed explicit connectors forms the smallest possible, custom tailored middleware.