Search

The performance of software running on parallel or distributed architectures can be severely affected by the location of data. In shared memory multicore architectures, data movement between caches and main memory is driven by data accesses from tasks executing in parallel on different cores and by a protocol to ensure cache coherence. This paper integrates cache coherence in a formal model of data access, to capture such data movement from an application perspective. We develop an executable model which captures cache coherent data movement between different cache levels and main memory, for software described by task-level data access patterns. The proposed model is generic in the number of cache levels and cores, and abstracts from the concrete communication medium. We show that the model guarantees expected correctness properties for cache coherence, in particular data consistency. This paper further presents a proof-of-concept implementation of the proposed model in rewriting logic, which allows different choices for the underlying hardware architecture of dynamically created parallel data access patterns to be specified and compared at the modelling level. • A formal, operational model of data access in multicore architectures with multilevel caches. • Correctness properties of the formal model, expressed as invariants over an arbitrary number of cores and caches. • A proof-of-concept implementation of the model to compare executions based on penalties, an abstract performance indicator. [ABSTRACT FROM AUTHOR]

Abstract: This paper describes the jcolibri2 framework for building Case-based reasoning (CBR) systems. CBR is a mature subfield of artificial intelligence based on the reuse of previous problem solutions–cases–to solve new ones. However, up until now, it lacked a reference toolkit for developing such systems. jcolibri2 aims to become that toolkit and to foster the collaboration among research groups. This software is the result of the experience collected over several years of framework development and evolution. This experience is explained in the paper, together with a description of the specialized CBR tools that can be implemented with jcolibri: CBR with textual cases, recommenders, knowledge/data intensive applications or distributed architectures. [Copyright &y& Elsevier]

Abstract: A layered software architecture helps in understanding the role of software entities (e.g. packages or classes) in a system and, hence, the impact of changes on these entities. However, the computation of an optimal layered organization in the presence of cyclic dependencies is difficult. In this paper, we present an approach that (i) provides a strategy supporting the automated detection of cyclic dependencies, (ii) proposes heuristics to break cyclic dependencies, and (iii) computes an organization of software entities in multiple layers even in the presence of cyclic dependencies. Our approach performs better than the other existing approaches in terms of accuracy and interactivity, and it supports human inputs and constraints. In this paper, we present this approach and compare it to existing solutions. We applied our approach on two large software systems to identify package layers and the results are manually validated by software engineers of the two systems. [Copyright &y& Elsevier]

Abstract Computer science marches towards energy-aware practices. This trend impacts not only the design of computer architectures, but also the design of programs. However, developers still lack affordable and accurate technology to measure energy consumption in computing systems. The goal of this paper is to mitigate such problem. To this end, we introduce JetsonLEAP, a framework that supports the implementation of energy-aware programs. JetsonLEAP consists of an embedded hardware, in our case, the NVIDIA Jetson TK1 development board, a circuit to control the flow of energy, of our own design, plus a library to instrument program parts. We discuss two different circuit setups. The most precise setup lets us reliably measure the energy spent by 225,000 instructions, the least precise, although more affordable setup, gives us a window of 975,000 instructions. To probe the precision of our system, we use it in tandem with a high-precision, high-cost acquisition system, and show that results do not differ in any significant way from those that we get using our simpler apparatus. Our entire infrastructure – board, power meter and both circuits – can be reproduced with about $500.00. To demonstrate the efficacy of our framework, we have used it to measure the energy consumed by programs running on ARM cores, on the GPU, and on a remote server. Furthermore, we have studied the impact of OpenACC directives on the energy efficiency of high-performance applications. Highlights • Revised version of early submission. • New infra-structure to measure energy in embedded devices. • Apparatus interfaces with compiler to measure energy consumption of small events. • Several new experiments have been performed. [ABSTRACT FROM AUTHOR]

Highlights • An architectural assumption management process with guidelines is developed. • Two case studies were conducted to validate the process. • The process can help to make architectural assumptions explicit. • The process can help to identify and reduce invalid architectural assumptions. Abstract Context Architectural assumption management is critical to the success of software development projects. In this paper, we propose an Architectural Assumption Management (AAM) process, comprised of four AAM activities: Architectural Assumption Making, Description, Evaluation, and Maintenance. Objective Evaluating the AAM process in architectural assumption management, regarding the ease of understanding and the effort of conducting the AAM process, as well as the effectiveness of using the AAM process to make architectural assumptions explicit and to identify and reduce invalid architectural assumptions. Method An explanatory study with 88 first-year master students in software engineering, and an exploratory study with five practitioners from five companies. Results (1) the ease of understanding the AAM process is moderate for first-year master students but easy for practitioners; (2) the effort of conducting the AAM process is moderate for first-year master students; (3) Making and Evaluation took the students more time than Description and Maintenance; (4) the practitioners considered Evaluation as the most time consuming activity; (5) the AAM process can help to make architectural assumptions explicit and to identify and reduce invalid architectural assumptions in projects. The majority of the students and practitioners agreed that Architectural Assumption Evaluation is the most helpful activity for all these three aspects. For other activities, there are different opinions about their helpfulness; and (6) there are various factors identified that can impact the aforementioned results. Being aware of and properly adjusting these factors can facilitate the application of the AAM process in projects. Conclusions The AAM process aims at systematically managing architectural assumptions in software development. The results of the case studies provide preliminary empirical evidence for the evaluation of the AAM process. [ABSTRACT FROM AUTHOR]

The practical application of the object constraint language (OCL), which is part of the UML specification since version 1.1, depends crucially on the existence of adequate tool support. This paper discusses general design issues for OCL tools. It is argued that the nature of OCL will lead to a large variety of tools, applied in combination with a variety of different UML tools. Therefore, a flexible modular architecture for a UML/OCL toolset is proposed. The paper reports on the first results of an ongoing project which aims at the provision of such an OCL toolset that is available as free software. [Copyright &y& Elsevier]

To manage the complexity of C programs, architecture models are used as high-level descriptions, allowing developers to understand, assess, and manage the C programs without having to understand the intricate complexity of the code implementations. However, for the architecture models to serve their purpose, they must be accurate representations of the C programs. In order to support creating accurate architecture models, the present paper presents a mapping from the domain of sequential non-recursive C programs to a domain of formal architecture models, each being a hierarchy of components with well-defined interfaces . The hierarchically organized components and their interfaces, which capture both data and function call dependencies, are shown to both enable high-level assessment and analysis of the C program and provide a foundation for organizing and expressing specifications for compositional verification . [ABSTRACT FROM AUTHOR]

Classical compiler architecture is centred around producing object code in a batch-oriented fashion. Integrated development environments (IDEs) present new challenges to the language implementer: information should be (almost) instantly available, and should be dynamically updated and presented even for incorrect code, as the user is editing. To increase responsiveness, it may be necessary to compute information incrementally, and to make use of multicore processors. An existing compiler cannot easily be adapted to provide IDE services without impacting the user experience; typically, IDE developers have to develop their own language frontends particularly targeted at IDE use. In this paper, we discuss the design of a library, Pica, for managing resources and information and easing IDE integration, and show how it is applied in the Eclipse IDE for the experimental Magnolia programming language. [ABSTRACT FROM AUTHOR]

Today's complex systems require software architects to address a large number of quality attributes. These quality attributes can be in contradiction with each other. In practice, software architects manually try to come up with a set of different architectural designs and then try to identify the most suitable one. This is a time-consuming and error-prone process. Also, this process may lead the architect to suboptimal designs. To tackle this problem, metaheuristic approaches for automating architecture design have been proposed by researchers. Metaheuristic approaches, such as genetic algorithms (GA), use degrees of freedom to automatically generate new alternative solutions. In this paper, we present two novel degrees of freedom for the optimization of system architectures. These two degrees of freedom: (i) the topology of the hardware platform, and (ii) load balancing of software components, can improve the results of the optimization algorithm. Our approach is implemented as part of the AQOSA (Automated Quality-driven Optimization of Software Architectures) framework. The AQOSA framework aids architects by automatically synthesizing optimal solutions by using multi-objective evolutionary algorithms and it reports the trade-offs between multiple quality properties as output. We analyze the effectiveness of our proposed degrees of freedom, by running a computationally-intensive optimization experiment using an industrial case study from automotive domain. The results show that two new degrees of freedom, (i) architecture topology and (ii) load balancing, help the evolutionary algorithm to find better solutions by enlarging the search space. [ABSTRACT FROM AUTHOR]

Event-driven programming in large scale environments is becoming a common requirement of modern distributed applications. It introduces some beneficial effects such as real-time state updates and replications, which enable new kinds of applications and efficient architectural solutions. However, these benefits could be compromised if the adopted infrastructure were not designed to ensure efficient delivery of events and related data. This paper presents an architectural model, a middleware (WS-Link) and annotation-based mechanisms to ensure high performance in delivering events carrying large attachments. We transparently decouple event notification from related data to avoid useless data-transfers. This way, while event notifications are routed in a conventional manner through an event service, data are directly and transparently transferred from publishers to subscribers. The theoretical analysis shows that we can reduce the average event delivery time by half, compared to a conventional approach requiring the full mediation of the event service. The experimental analysis confirms that the proposed approach outperforms the conventional one (both for throughput and delivery time) even though the middleware overhead, introduced by the specific adopted model, slightly reduces the expected benefits. [ABSTRACT FROM AUTHOR]

In a well designed software system, units of related functionality are organized into modules and classes, which are in turn arranged into inheritance trees, package hierarchies, components, libraries, frameworks, and services. The trade-offs between simplicity versus flexibility and power are carefully considered, and interfaces are designed that expose the key functional properties of a component while hiding much of the complexity of the implementation details. However, over time the design integrity of a well-engineered system tends to decay as new features are added, as new quality attributes are emphasized, and as old architectural knowledge is lost when experienced development personnel shift to new jobs. Consequently, as developers and as users we often find ourselves looking at a piece of functionality or other design artifact and wondering, “Why is this here?” That is, we would like to examine the provenance of an artifact to understand its history and why it is where it is within the current design of the system. In this brief paper, we sketch some of the dimensions of the broad problem of extracting and reasoning about the provenance of software development artifacts. As a motivating example, we also describe some recent related work that uses hashing to quickly and accurately identify version information of embedded Java libraries. [ABSTRACT FROM AUTHOR]

Abstract: The OpenDSA Project seeks to provide complete instructional materials for data structures and algorithms (DSA) courses. Our vision for a highly interactive eTextbook involves the use of many algorithm visualizations (AVs) and a wide range of interactive exercises with automated assessment. To realize this vision we require a mix of third-party and custom software components that make up a client/server-based web application. The massive amount content development required compels us to adopt an appropriate mix of open-source practices that will encourage broad contribution to the project. In this paper we describe the OpenDSA system architecture and the design goals that led to the present version of the system. [Copyright &y& Elsevier]

Abstract: We report on the actual industrial use of formal methods during the development of a software bus. During an internship at Neopost Inc., of 14 weeks, we developed the server component of a software bus, called the XBus, using formal methods during the design, validation and testing phase: we modeled our design of the XBus in the process algebra mCRL2, validated the design using the mCRL2-simulator, and fully automatically tested our implementation with the model-based test tool JTorX. This resulted in a well-tested software bus with a maintainable architecture. Writing the model ( ), simulating it, and testing the implementation with JTorX only took 17% of the total development time. Moreover, the errors found with model-based testing would have been hard to find with conventional test methods. Thus, we show that formal engineering can be feasible, beneficial and cost-effective. The findings above, reported earlier by us in (Sijtema et al., 2011) [1], were well-received, also in industrially oriented conferences (Ferreira and Romanenko, 2010) [2] and [3]. In this paper, we look back on the case study, and carefully analyze its merits and shortcomings. We reflect on (1) the added benefits of model checking, (2) model completeness and (3) the quality and performance of the test process. Thus, in a second phase, after the internship, we model checked the XBus protocol—this was not done in [1] since the Neopost business process required a working implementation after 14 weeks. We used the CADP tool evaluator4 to check the behavioral requirements obtained during the development. Model checking did not uncover errors in model , but revealed that model was neither complete nor optimized: in particular, requirements to the so-called bad weather behavior (exceptions, unexpected inputs, etc.) were missing. Therefore, we created several improved models, checked that we could validate them, and used them to analyze quality and performance of the test process. Model checking was expensive: it took us approx. 4 weeks in total, compared to 3 weeks for the entire model-based testing approach during the internship. In the second phase, we analyzed the quality and performance of the test process, where we looked at both code and model coverage. We found that high code coverage (almost 100%) is in most cases obtained within 1000 test steps and 2 minutes, which matches the fact that the faults in the XBus were discovered within a few minutes. Summarizing, we firmly believe that the formal engineering approach is cost-effective, and produces high quality software products. Model checking does yield significantly better models, but is also costly. Thus, system developers should trade off higher model quality against higher costs. [Copyright &y& Elsevier]

Abstract: The process of deploying a distributed system in a network of machines is often very complex, laborious and time-consuming, while it is hard to guarantee that the system will work as expected and that specific non-functional deployment requirements from the domain are supported. In this paper we describe the Disnix toolset, which provides system administrators or developers with automatic deployment of a distributed system in a network of machines from declarative specifications and offers properties such as complete dependencies, atomic upgrades and rollbacks to make this process efficient and reliable. Disnix has an extensible architecture, allowing the integration of custom modules to make the deployment more convenient and suitable for the domain in which the system is to be used. Disnix has been under development for almost four years and has been applied to several types of distributed systems, including an industrial case study. [Copyright &y& Elsevier]

Abstract: Test coverage is about assessing the relevance of unit tests against the tested application. It is widely acknowledged that software with a “good” test coverage is more robust against unanticipated execution, thus lowering the maintenance cost. However, ensuring good quality coverage is challenging, especially since most of the available test coverage tools do not discriminate between software components that require “strong” coverage from the components that require less attention from the unit tests. Hapao is an innovative test coverage tool, implemented in the Pharo Smalltalk programming language. It employs an effective and intuitive graphical representation to visually assess the quality of the coverage. A combination of appropriate metrics and relations visually shape methods and classes, which indicates to the programmer whether more effort on testing is required. This paper presents the important features of Hapao by illustrating its application on an open source software. [Copyright &y& Elsevier]

Abstract: Experimental software and toolkits play a crucial role in computer science. Elsevier’s Science of Computer Programming special issues on Experimental Software and Toolkits (EST) provide a means for academic tool builders to get more visibility and credit for their work, by publishing a paper along with the corresponding system in a peer-reviewed journal. Typically, tools are presented from both a user and a developer perspective, addressing tool-building issues such as architecture and design, requirements, methodologies and process aspects. This is already the fourth edition of EST with no less than 17 published systems covering application areas ranging from software analysis and visualization to teaching and software development support. [Copyright &y& Elsevier]

Abstract: Ambient Intelligence (AmI) systems need to be as transparent as possible, that is, their users should perceive only the effects of the features presented to them and, in some cases, some kind of interface. They should not be conscious of how these features are implemented, from a hardware or from a software point of view. In order to obtain such a high degree of transparency, it is necessary for the system to be able to provide its services regardless of location, adapting to the environment and the context in general and to the available hardware more specifically. This is known as ubiquity, and to achieve it requires considering many aspects, from security and privacy to system interoperability. This paper is mainly focused on the development of two elements related to ubiquity: physical migration of components between different platforms together with their associated runtime state, and the adaptation of those components to the destination platform and physical environment. These solutions are being addressed within our efforts for the development of a general-purpose middleware for Ambient Intelligence in the framework of the HI3 project. [Copyright &y& Elsevier]

Abstract: In this day and age of multicore architectures, programming language support is in urgent need for constructing programs that can take great advantage of machines with multiple cores. We present in this paper an approach to safe multicore programming in ATS, a recently developed functional programming language that supports both linear and dependent types. In particular, we formalize a type system capable of guaranteeing safe manipulation of resources on multicore machines and establish its soundness. We also provide concrete examples as well as experimental results in support of the practicality of the presented approach to multicore programming. [Copyright &y& Elsevier]

Abstract: The rising interest in Java for High Performance Computing (HPC) is based on the appealing features of this language for programming multi-core cluster architectures, particularly the built-in networking and multithreading support, and the continuous increase in Java Virtual Machine (JVM) performance. However, its adoption in this area is being delayed by the lack of analysis of the existing programming options in Java for HPC and thorough and up-to-date evaluations of their performance, as well as the unawareness on current research projects in this field, whose solutions are needed in order to boost the embracement of Java in HPC. This paper analyzes the current state of Java for HPC, both for shared and distributed memory programming, presents related research projects, and finally, evaluates the performance of current Java HPC solutions and research developments on two shared memory environments and two InfiniBand multi-core clusters. The main conclusions are that: (1) the significant interest in Java for HPC has led to the development of numerous projects, although usually quite modest, which may have prevented a higher development of Java in this field; (2) Java can achieve almost similar performance to natively compiled languages, both for sequential and parallel applications, being an alternative for HPC programming; (3) the recent advances in the efficient support of Java communications on shared memory and low-latency networks are bridging the gap between Java and natively compiled applications in HPC. Thus, the good prospects of Java in this area are attracting the attention of both industry and academia, which can take significant advantage of Java adoption in HPC. [Copyright &y& Elsevier]

Abstract: The development of reliable software for industrial critical systems benefits from the use of formal models and verification tools for detecting and correcting errors as early as possible. Ideally, with a complete model-based methodology, the formal models should be the starting point to obtain the final reliable code and the verification step should be done over the high-level models. However, this is not the case for many projects, especially when integrating existing code. In this paper, we describe an approach to verify concurrent C code by automatically extracting a high-level formal model that is suitable for analysis with existing tools. The basic components of our approach are: (1) a method to construct a labeled transition system from the source code, that takes flow control and interaction among processes into account; (2) a modeling scheme of the behavior that is external to the program, namely the functionality provided by the operating system; (3) the use of demand-driven static analyses to make a further abstraction of the program, thus saving time and memory during its verification. The whole proposal has been implemented as an extension of the CADP toolbox, which already provides a variety of analysis modules for several input languages using labeled transition systems as the core model. The approach taken fits well within the existing architecture of CADP which does not need to be altered to enable C program verification. We illustrate the use of the extended CADP toolbox by considering examples of the VLTS benchmark suite and C implementations of various concurrent programs. [Copyright &y& Elsevier]

Abstract: Lock-freedom is a property of concurrent programs which states that, from any state of the program, eventually some process will complete its operation. Lock-freedom is a weaker property than the usual expectation that eventually all processes will complete their operations. By weakening their completion guarantees, lock-free programs increase the potential for parallelism, and hence make more efficient use of multiprocessor architectures than lock-based algorithms. However, lock-free algorithms, and reasoning about them, are considerably more complex. In this paper we present a technique for proving that a program is lock-free. The technique is designed to be as general as possible and is guided by heuristics that simplify the proofs. We demonstrate our theory by proving lock-freedom of two non-trivial examples from the literature. The proofs have been machine-checked by the PVS theorem prover, and we have developed proof strategies to minimise user interaction. [Copyright &y& Elsevier]

Abstract: This paper presents the Navigation Maps Modeling approach (NMM), which provides platform independent models for characterizing navigation maps of web applications. The NMM approach is conceived to obtain a trade off between high and low-level design notations. As high-level design notations, NMM models permit architectural details that may hinder the overall understanding of the web application to be left out. As low-level design notations, NMM models can easily be transformed into detailed architectural designs, which are very valuable at coding and maintenance stages. [Copyright &y& Elsevier]

Abstract: Today’s complex applications must face the distribution of data and code among different network nodes. Computation in distributed contexts is demanding increasingly powerful languages and execution environments, able to provide programmers with appropriate abstractions and tools. Java is a wide-spread language that allows developers to build complex software, even distributed, but it cannot handle the migration of computations (i.e. threads), due to intrinsic limitations of many traditional JVMs. After analyzing the approaches in the literature, this paper presents our thread migration framework (called Mobile JikesRVM), implemented on top of the IBM Jikes Research Virtual Machine (RVM): exploiting some of the innovative techniques in the JikesRVM, we implemented an extension of its scheduler that allows applications to easily capture the state of a running thread and makes it possible to restore it elsewhere (i.e. on a different hardware architecture or operating system), but still with a version of the framework installed). Our thread serialization mechanism provides support for both proactive and reactive migration, available also for multi-threaded Java applications, and tools to deal with the problems of resource relocation management. With respect to previous approaches, we implemented Mobile JikesRVM without recompiling its JVM (Java Virtual Machine) source code, but simply extending JikesRVM functionalities with a full Java package to be imported when thread migration is needed. [Copyright &y& Elsevier]

Abstract: This paper presents a lock-free algorithm for mark&sweep garbage collection (GC) in a realistic model using synchronization primitives load-linked/store-conditional (LL/SC) or compare-and-swap (CAS) offered by machine architectures. The algorithm is concurrent in the sense that garbage collection can run concurrently with the application (the mutator threads). It is parallel in that garbage collection itself may employ several concurrent collector threads. We first design and prove an algorithm with a coarse grain of atomicity and subsequently apply the reduction method developed and verified in [H. Gao, W.H. Hesselink, A formal reduction for lock-free parallel algorithms, in: Proceedings of the 16th Conference on Computer Aided Verification, CAV, July 2004] to implement the high-level atomic steps by means of the low-level primitives. Even the correctness of the coarse grain algorithm is very delicate due to the presence of concurrent mutator and collector threads. We have verified it therefore by means of the interactive theorem prover PVS. [Copyright &y& Elsevier]

Abstract: We offer a reference model for nested transactions at the level of memory accesses, and sketch possible hardware architecture designs that implement that model. We describe both closed and open nesting. The model is abstract in that it does not relate to hardware, such as caches, but describes memory as seen by each transaction, memory access conflicts, and the effects of commits and aborts. The hardware sketches describe approaches to implementing the model using bounded size caches in a processor with overflows to memory. In addition to a model that will support concurrency within a transaction, we describe a simpler model that we call linear nesting. Linear nesting supports only a single thread of execution in a transaction nest, but may be easier to implement. While we hope that the model is a good target to which to compile transactions from source languages, the mapping from source constructs to nested transactional memory is beyond the scope of the paper. [Copyright &y& Elsevier]

Abstract: Software Architectures have evolved considerably over the last decade and, partly also due to the significant progress made in component-based development, have become a major subfield of Software Engineering. The associated field of Architecture Description Languages (ADLs) has also evolved considerably, providing numerous approaches to the formal specification and representation of architectural designs. In this field, one of its most interesting (and rather recent) aspects has been the exploration of different ways to map architectural specifications down to executable representations. In this paper, we present a methodology for mapping the generic features of any typical ADL to executable code. The mapping process involves the use of ACME, a generic language for describing software architectures, and the coordination paradigm. More to the point, we show how the core concepts of ACME can be mapped to equivalent executable code written in the coordination language Manifold. The result is the generation of skeletal code which captures and implements the most important system implementation properties of the translated architectural design, thus significantly assisting the programmer in filling in the rest of the needed code. [Copyright &y& Elsevier]

Abstract: Virtual machines (VMs) are a popular target for language implementers. A long-running question in the design of virtual machines has been whether stack or register architectures can be implemented more efficiently with an interpreter. Many designers favour stack architectures since the location of operands is implicit in the stack pointer. In contrast, the operands of register machine instructions must be specified explicitly. In this paper, we present a working system for translating stack-based Java virtual machine (JVM) code to a simple register code. We describe the translation process, the complicated parts of the JVM which make translation more difficult, and the optimisations needed to eliminate copy instructions. Experimental results show that a register format reduced the number of executed instructions by 34.88%, while increasing the number of bytecode loads by an average of 44.81%. Overall, this corresponds to an increase of 2.32 loads for each dispatch removed. We believe that the high cost of dispatches makes register machines attractive even at the cost of increased loads. [Copyright &y& Elsevier]

Abstract: This paper proposes several novel architectural styles for active documents. Active documents are documents that contain not only data, but also servlets, applets, expressions in spreadsheet languages, and other forms of software. To grasp the different forms of architectures, several novel concepts are defined. Invasive document composition is a type-safe form of template expansion and extension; transconsistency is a form of transclusion for architectures; and staged architectures provide a form of staged programming on the architectural level. With these concepts, it is possible to explain the architectures of many document processing applications for Web and office, and we define the architectural styles of wizard-parametrized, script-parametrized, transconsistent, stream-based, and staged active documents. Finally, we give a hypothesis of active document composition: it consists of four elements, namely, explicit architecture, invasiveness, transconsistency, and staging. On the basis of this hypothesis, many applications in Web engineering and document processing get a common background, and can be compared and simplified. [Copyright &y& Elsevier]

Often network components work correctly, yet end-to-end services don’t. This happens if configuration parameters of components are set to incorrect values. Configuration is a fundamental operation for logically integrating components to set up end-to-end services.Configuration errors arise frequently because transforming end-to-end service requirements into component configurations is inherently difficult. Such transformation is largely performed in a manual and localized fashion, resulting in high cost of network operations.The Service Grammar technique has been developed to solve the configuration error diagnosis problem, and, more generally, to formalize the process of building complex systems via configuration.At its core is a Requirements Language that contains global, high-level constraints upon configuration parameters. These are derived from identifying the notion of “correct configuration” associated with different protocols. These are composed to create system-wide requirements on architecture and policies. A Diagnosis Engine checks if constraints in the Requirements Language are true given definite component configurations, and is used recursively to check composite requirements.This paper describes an application of Service Grammar to diagnosing BGP configuration errors. As BGP architecture and policies differ widely from one network to another, it is not possible using previous techniques to check if router configurations implement the intended requirements. Our tools enable administrators to specify system-wide, network-specific requirements and check if they are correctly implemented by component configurations. [Copyright &y& Elsevier]

In this paper we examine formally the idea that the architecture of a system can be modelled by the structure of its interface expressed in terms of the interfaces for its components. Thus,System Interface Architecture=Structured set of Sub-system Interfaces.We specify an abstract model for interface definition languages (IDLs) based on this idea and the idea that anInterface=Name+Imports+Body.A set of interfaces is a repository. An interface architecture is a repository with some primary interfaces identified; the import dependencies between the interfaces of a repository are used to determine its structure.The abstract model uses algebraic specifications to define the abstract syntax of a general IDL, and interface transformations using structural induction. We examine a flattening process which assembles a system interface from its components.We use the general model to derive a simple IDL suitable for the design phase of object-oriented software development. This requires us to specify a form of Body that treats both data types and state, and in Body we explicitly distinguish between methods with and without side-effects, by commands and queries, respectively. We also consider alternative proposals for Body that yield new IDLs, including other object-oriented design languages and data type specification languages. [Copyright &y& Elsevier]

Complex software systems require expressive notations for representing their software architectures. Two competing paths have emerged. One is to use a specialized notation for architecture, an architecture description language (ADL). The other is to adapt a general-purpose modeling notation, such as UML. The latter has a number of benefits, including familiarity to developers, close mapping to implementations, and commercial tool support. However, it remains an open question as to how best to use object-oriented notations for architectural description, and, indeed, whether they are sufficiently expressive, as currently defined. In this paper, we take a systematic look at these questions, examining the space of possible mappings from ADLs into UML. Specifically, we describe (a) the principal strategies for representing architectural structure in UML; (b) the benefits and limitations of each strategy; and (c) aspects of architectural description that are intrinsically difficult to model in UML using the strategies. [Copyright &y& Elsevier]