The paper formulates HEQ, an institution for hybrid equational logic to provide a uniform setting to express and reasoning about diferent sorts of properties of complex software. It is also shown how, through the denition of a suitable comorphism to FOL, this can be integrated in Hets, providing suitable tool support for teaching and research. The whole exercise was motivated by the need to unify, in a single under-graduate course in a Computer Science curriculum, the specication of data and behavioural constraints of recongurable systems.

The transmission of multimedia content between mobile devices is increasingly an area of exploration. The evolution of mobile devices and networks that support them, provide potential to create more sophisticated and innovating services. The fact that the Android platform does not provide the SIP protocol in its architecture, is a limiting factor for the development of new streaming applications. Throughout this paper the Android platform is presented, and more specifically the streaming protocols supported by the current streaming Media Framework. Based on the current Android Media Framework, this paper presents a possible architecture for the integration of the SIP protocol. The integration of this architecture is to surpass the limitations of the current Android platform and promote an improved performance in the current SIP applications, which is reflected in a lower power consumption of the device.

QoS analysis of coordinated distributed autonomous services is currently of interest in the area of service-oriented computing and calls for new technologies and supporting tools. In previous work, the first three authors have proposed a compositional automata model to provide semantics for stochastic Reo, a channel based coordination language that supports the specification of QoS values (such as request arrivals or processing rates). Furthermore, translations from this automata model into stochastic models, such as continuous-time Markov chains (CTMCs) and interactive Markov chains (IMCs) have also been presented. Based on those results, we describe in this paper a case study of QoS analysis. We analyze a certain instance of the ASK system, an industrial software system for connecting people offering professional services to clients requiring those services. We develop a model of the ASK system using stochastic Reo. The distributions used in this model were obtained by applying statistical analysis techniques on the raw values that we obtained from the real logs of an actual running ASK system. These distributions are used for the derived CTMC model for the ASK system to analyze and to improve the performance of the system, under the assumption that the distributions are exponentially distributed. In practice, this is not always the case. Thus, we also carry out a simulation-based analysis by a Reo simulator that can deal with non-exponential distributions. Compared to the analysis on the derived CTMC model, the simulation is approximation-based analysis, but it reveals valuable insight in the behavior of the system. The outcome of both analyses helps both the developers and the installations of the ASK system to improve the performance of the system.

Coalgebras provide a uniform framework to study dynamical systems, including several types of automata. In this paper, we make use of the coalgebraic view on systems to investigate, in a uniform way, under which conditions calculi that are sound and complete with respect to behavioral equivalence can be extended to a coarser coalgebraic language equivalence, which arises from a generalised powerset construction. We illustrate the framework with two examples: non-deterministic automata, for which we recover Rabinovich’s sound and complete calculus for language equivalence, and weighted automata, for which we present the first sound and complete calculus for weighted language equivalence.

Recent study has shown that accurate knowledge of the false negative rate (FNR) of tests can significantly improve the diagnostic accuracy of spectrum-based fault localization. To understand the principles behind FNR modeling in this paper we study three error propagation probability (EPP) modeling approaches applied to a number of logic circuits from the 74XXX/ISCAS-85 benchmark suite. Monte Carlo simulations for random injected faults show that a deterministic approach that models gate behavior provides high accuracy (O(1%)), while probabilistic approaches that abstract from gate modeling generate higher prediction errors (O(10%)), which increase with the number of injected faults.

In practically all development processes, regression tests are used to detect the presence of faults after a modification. If faults are detected, a fault localization algorithm can be used to reduce the manual inspection cost. However, while using test case prioritization to enhance the rate of fault detection of the test suite (e.g., statement coverage), the diagnostic information gain per test is not optimal, which results in needless inspection cost during diagnosis. We present RAPTOR, a test prioritization algorithm for fault localization, based on reducing the similarity between statement execution patterns as the testing progresses. Unlike previous diagnostic prioritization algorithms, RAPTOR does not require false negative information, and is much less complex. Experimental results from the Software Infrastructure Repository’s benchmarks show that RAPTOR is the best technique under realistic conditions, with average cost reductions of 40% with respect to the next best technique, with negligible impact on fault detection capability.