Search

Abstract Many metrics have been proposed to measure coupling—the degree of association between modules in a system. They have often been described in different ways, hindering comparison and research. Their definitions are often incomplete regarding language features in some languages, meaning that different tool developers may implement the same metric differently. This complicates comparing results from studies that use different tools. This paper therefore aims to define coupling metrics consistently and unambiguously. The paper describes a model of coupling that uses the reification of the concept of dependency as its fundamental unit. Based on this model, it defines a framework for defining coupling metrics. It shows how to define several well-known coupling metrics in the framework, and how defining different metrics based on the same model facilitates direct comparisons. It discusses how the framework resolves issues due to incomplete metric definitions, such as different language features. This formal framework is sufficiently simple that it can be implemented in such a way as to provide multiple metrics. [ABSTRACT FROM AUTHOR]

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: Invariant assertions play an important role in the analysis and documentation of while loops of imperative programs. Invariant functions and invariant relations are alternative analysis tools that are distinct from invariant assertions but are related to them. In this paper we discuss these three concepts and analyze their relationships. The study of invariant functions and invariant relations is interesting not only because it provides alternative means to analyze loops, but also because it gives us insights into the structure of invariant assertions, hence it may help us enhance techniques for generating invariant assertions. [Copyright &y& Elsevier]

Abstract: Unsatisfiable cores, i.e., parts of an unsatisfiable formula that are themselves unsatisfiable, have important uses in debugging specifications, speeding up search in model checking or SMT, and generating certificates of unsatisfiability. While unsatisfiable cores have been well investigated for Boolean SAT and constraint programming, the notion of unsatisfiable cores for temporal logics such as LTL has not received much attention. In this paper we investigate notions of unsatisfiable cores for LTL that arise from the syntax tree of an LTL formula, from converting it into a conjunctive normal form, and from proofs of its unsatisfiability. The resulting notions are more fine-grained than existing ones. We illustrate the benefits of the more fine-grained notions on examples from the literature. We extend some of the notions to realizability and we discuss the relationship of unsatisfiable and unrealizable cores with the notion of vacuity. [Copyright &y& Elsevier]

Abstract: In this paper we have been influenced by those who take an “engineering view” of the problem of designing systems, i.e. a view that is motivated by what someone designing a real system will be concerned with, and what questions will arise as they work on their design. Specifically, we have borrowed from the testing work of Hennessy, de Nicola and van Glabbeek, e.g. Hennessy, 1988 , de Nicola , de Nicola, 1992  and van Glabbeek, 2001, 1990 . Here we concentrate on one fundamental part of the engineering view and where consideration of it leads. The aspects we are concerned with are computational entities in contexts, observed by users. This leads to formalising design steps that are often left informal, and that in turn gives insights into non-determinism and ultimately leads to being able to use refinement in situations where existing techniques fail. [Copyright &y& Elsevier]

Abstract: In recent years, network streaming becomes a highly popular research topic in computer science due to the fact that a large proportion of network traffic is occupied by multimedia streaming. In this paper we present novel methodologies for enhancing the streaming capabilities of Java RMI. Our streaming support for Java RMI includes the pushing mechanism, which allows the servers to push data in a streaming fashion to the client site, and the aggregation mechanism, which allows the client site to make a single remote invocation to gather data from multiple servers that keep replicas of data streams and aggregate partial data into a complete data stream. In addition, our system also allows the client site to forward local data to other clients. Our framework is implemented by extending the Java RMI stub to allow custom designs for streaming buffers and controls, and by providing a continuous buffer for raw data in the transport layer socket. This enhanced framework allows standard Java RMI services to enjoy streaming capabilities. In addition, we propose aggregation algorithms as scheduling methods in such an environment. Preliminary experiments using our framework demonstrate its promising performance in the provision of streaming services in Java RMI layers. [Copyright &y& Elsevier]