Starvation-free mutual exclusion with semaphores

The standard implementation of mutual exclusion by means of a semaphore allows starvation of processes. Between 1979 and 1986, three algorithms were proposed that preclude starvation. These algorithms use a special kind of semaphore. We model this so-called buffered semaphore rigorously and provide mechanized proofs of the algorithms. We prove that the algorithms are three implementations of one abstract algorithm in which every competing process is overtaken not more than once by any other process. We also consider a so-called polite semaphore, which is weaker than the buffered one and is strong enough for one of the three algorithms. Refinement techniques are used to compare the algorithms and the semaphores.     

The Multi-Mode Resource-Constrained Multi-Project Scheduling Problem

Scheduling projects is a difficult and time consuming process, and has far-reaching implications for any organization’s operations. By generalizing various aspects of project scheduling, decision makers are enabled to capture reality and act accordingly. In the context of the MISTA 2013 conference, the first MISTA challenge, organized by the authors, introduced such a general problem model: the Multi-Mode Resource-Constrained Multi-Project Scheduling Problem (MRCMPSP). The present paper reports on the competition and provides a discussion on its results. Furthermore, it provides an analysis of the submitted algorithms, and a study of their common elements. By making all benchmark datasets and results publicly available, further research on the MRCMPSP is stimulated.     

A hierarchical modeling approach for risk assessment in developmental toxicity studies

Within the past decade, there has been an increasing interest in the problem of joint analysis of clustered multiple outcome data, motivated by developmental toxicity applications. Typically, a toxic insult early in gestation may result in a resorbed fetus or a fetal death. If however the fetus survives the entire gestation period, growth reduction such as low birth weight may occur, or can exhibit a malformation. Ideally, a model should take the complete hierarchical structure of the data into account. So far, however, one has tackled the challenges in this setting only partly each time making different restricting assumptions (e.g., restriction to viable fetuses only). In addition, because of genetic similarity and the same treatment conditions, offsprings of the same mother behave more alike than those of another mother. Thus, responses on different fetuses within a cluster are likely to be correlated. The ultimate scientific question requires assessing the full effect of dose administration, not only in the malformation and weight outcome, but also in the death outcome. A hierarchical Bayesian method is proposed to this effect. Such a model can serve as a basis for quantitative risk assessment.     

An illustration of verification and validation in the modelling phase of KBS development

Reliability has become a key factor in KBS development. For this reason, it has been suggested that verification and validation (V&V) should become an integrated part of activities throughout the whole KBS development cycle. In this paper, it will be illustrated how the PROLOGA workbench integrates V&V aspects into its modelling environment, such that these techniques can be of assistance in the process of knowledge acquisition and representation. To this end, verification has to be performed incrementally and can no longer be delayed until after the system has been completed. It will be shown how this objective can be realised through an approach that uses the decision table formalism as a modelling instrument.     

Inverse Routh table construction and stability of delay equations

Based on an inversion of the Routh table construction, a unimodular characterization of all Hurwitz polynomials is obtained. In parameter space, the Hurwitz polynomials of degree n correspond to the positive 2ⁿ-tant. The method is then used to construct classes of stable continuous-time delay-difference equations and delay differential equations of neutral type, by a suitable limiting process.     

Mining frequent conjunctive queries in relational databases through dependency discovery

We present an approach for mining frequent conjunctive in arbitrary relational databases. Our pattern class is the simple, but appealing subclass of simple conjunctive queries. Our algorithm, called Conqueror $^+$ , is capable of detecting previously unknown functional and inclusion dependencies that hold on the database relations as well as on joins of relations. These newly detected dependencies are then used to prune redundant queries. We propose an efficient database-oriented implementation of our algorithm using SQL and provide several promising experimental results.     

Formalizing a hierarchical file system

An abstract file system is defined here as a partial function from (absolute) paths to data. Such a file system determines the set of valid paths. It allows the file system to be read and written at a valid path, and it allows the system to be modified by the Unix operations for creation, removal, and moving of files and directories. We present abstract definitions (axioms) for these operations. This specification is refined towards a pointer implementation. The challenge is to have a natural abstraction function from the implementation to the specification, to define operations on the concrete store that behave exactly in the same way as the corresponding functions on the abstract store, and to prove these facts. To mitigate the problems attached to partial functions, we do this in two steps: first a refinement towards a pointer implementation with total functions, followed by one that allows partial functions. These two refinements are proved correct by means of a number of invariants. Indeed, the insights gained consist, on the one hand, of the invariants of the pointer implementation that are needed for the refinement functions, and on the other hand of the precise enabling conditions of the operations on the different levels of abstraction. Each of the three specification levels is enriched with a permission system for reading, writing, or executing, and the refinement relations between these permission systems are explored. Files and directories are distinguished from the outset, but this rarely affects our part of the specifications. All results have been verified with the proof assistant PVS, in particular, that the invariants are preserved by the operations, and that, where the invariants hold, the operations commute with the refinement functions.     

A criterion for atomicity revisited

Concurrent and reactive programs are specified by their behaviours in the presence of a nondeterministic environment. In a natural way, this gives a specification (ARW) of an atomic variable in the style of Abadi and Lamport. Several implementations of atomic variables by lower level primitives are known. A few years ago, we formulated a criterion to prove the correctness of such implementations. The proof of correctness of the criterion itself was based on Lynch’s definition of atomicity by serialization points. Here, this criterion is reformulated as a specification HRW in the formal sense. Simulations from HRW to ARW and vice versa are constructed. These now serve as a constructive proof of correctness of the criterion. Eternity variables are used in the simulation from HRW to ARW. We propose so-called gliding simulations to deal with the problems that appear when occasionally the concrete implementation needs fewer steps than the abstract specification.     

Robustness assessment via stability radii in delay parameters

This paper focuses on the robust stability analysis of a class of linear systems including multiple delays subjected to constant or time‐varying perturbations. The approach considered makes use of appropriate stability radius concepts (dynamic, static) and relies on a feedback interconnection interpretation of the uncertain system. Various computable bounds on stability radii are obtained that exploit the structure of the problem. Systems including perturbations on both system matrices and delays are also dealt with. Copyright © 2008 John Wiley & Sons, Ltd.     

A Multicast-Enabled Delivery Framework for QoE Assurance of Over-The-Top Services in Multimedia Access Networks

Over-The-Top (OTT) video services are becoming more and more important in today’s broadband access networks. While original OTT services only offered short duration medium quality videos, more recently, premium content such as high definition full feature movies and live video are offered as well. For operators, who see the potential in providing Quality of Experience (QoE) assurance for an increased revenue, this introduces important new network management challenges. Traditional network management paradigms are often not suited for ensuring QoE guarantees as the provider does not have any control on the content’s origin. In this article, we focus on the management of an OTT-based video service. We present a loosely coupled architecture that can be seamlessly integrated into an existing OTT-based video delivery architecture. The framework has the goal of resolving the network bottleneck that might occur from high peaks in the requests for OTT video services. The proposed approach groups the existing Hypertext Transfer Protocol (HTTP) based video connections to be multicasted over an access network’s bottleneck and then splits them again to reconstruct the original HTTP connections. A prototype of this architecture is presented, which includes the caching of videos and incorporates retransmission schemes to ensure robust transmission. Furthermore, an autonomic algorithm is presented that allows to intelligently select which OTT videos need to be multicasted by making a remote assessment of the cache state to predict the future availability of content. The approach was evaluated through both simulation and large scale emulation and shows a significant gain in scalability of the prototype compared to a traditional video delivery architecture.