18394118
Formalizing Real-Time Scheduling as Program Refinement
This paper shows how the feasibility of scheduling a realtime program consisting of a number of parallel processes (tasks) can be proved as a step in the refinement of the program from its specification. Verification of this step of refinement makes formal use of methods and results from real-time scheduling theory.
7323063
rCOS: Refinement of Component and Object Systems
We present a model of object-oriented and component-based refinement. For object-orientation, the model is class-based and refinement is about correct changes in the structure, methods of classes and the main program, rather than changes in the behaviour of individual objects. This allows us to prove refinement laws for both high level design patterns and low level refactoring. For component-based development, we focus on the separation of concerns of interface and functional contracts, leaving refinement of interaction protocols in future work. The model supports the specification of these aspects at different levels of abstractions and their consistency. 
 
Based on the semantics, we also provide a general definitional approach to defining different relational semantic models with different features and constraints.
5135154
Linking UML models of design and requirement
Both a UML model of requirement and a UML model of a design are defined as a pair of class diagram and a family of sequence diagrams. We then give an unified semantics for models of requirements and designs. We define the consistency between a design class diagram and the interaction diagrams and show how the removal of inconsistency can be treated as a model refinement. We then formally define the correctness of UML model of design with respect to the model of requirement.
14189544
Verification, refinement and scheduling of real-time programs
Abstract A real-time program can be developed by refining a specification into program code. Verification of the timing properties of the program is then usually done at two levels: verification of the ordering of timed actions in the program and proof that execution of the program on a specific system will meet its timing requirements. Refinement is done within a formal model but the second step requires a different framework in which scheduling theory analysis is used and actual program execution times can be taken into account. The implementation of a program on a system is said to be feasible or schedulable if it will meet all the timing deadlines. This paper shows how the feasibility of scheduling a real-time program can also be proved as a step in the refinement of the program from its specification. Verification of this step of refinement makes use of methods from scheduling theory within a formal system development framework.
39997807
Component-Based Software Engineering
We discuss some of the difficulties and significant issues that we need to consider when developing a formal method for component-based software engineering. We argue that to deal with the challenges, there is a need in research to link existing theories and methods of programming for effective support to component-based software engineering. We then present our initiative on a unified multi-view approach to modelling, design and analysis of component systems, emphasising the integration of models for different views.
16560725
rCOS: A refinement calculus of object systems
This article presents a mathematical characterization of object-oriented concepts by defining an observation-oriented semantics for a relational object-based language with a rich variety of features including subtypes, visibility, inheritance, type casting, dynamic binding and polymorphism. The language can be used to specify object-oriented designs as well as programs. We present a calculus that supports both structural and behavioural refinement of object-oriented designs. The design calculus is based on the predicate logic in Hoare and He's Unifying Theories of Programming (UTP).
16029762
Preemptive Scheduling with Variable Profile, Precedence Constraints and Due Dates
Abstract This paper is concerned with the problem of scheduling preemptive tasks subject to precedence constraints in order to minimize the maximum lateness and the makespan. The number of available parallel processors is allowed to vary in time. It is shown that when an earliest due date first algorithm provides an optimal nonpreemptive schedule for unit-execution-time (UET) tasks, the preemptive priority scheduling algorithm, referred to as smallest laxity first, provides an optimal preemptive schedule for real-execution-time (RET) tasks. When the objective is to minimize the makespan, we get the same kind of result between highest level first schedules solving nonpreemptive tasks with UET and the longest remaining path first schedule for the corresponding preemptive scheduling problem with RET tasks. These results are applied to four specific profile scheduling problems and new optimality results are obtained.
9905546
Mean eccentricities of de Bruijn networks
Given a graph G = (V; E) we deene e(X), the mean eccentricity of a vertex X, as the average distance from X to all the other vertices of the graph. The computation of this parameter appears to be nontrivial in the case of the de Bruijn networks. In this paper we consider upper and lower bounds for e(X). For the directed de Bruijn network, we provide tight bounds as well as the extremal vertices which reach these bounds. These bounds are expressed as the diameter minus some constants. In the case of undirected networks, the computation turns out to be more diicult. We provide lower and upper bounds which diier from the diameter by some small constants. We conjecture that the vertices of the form a a have the largest mean eccentricity. Numerical computations indicate that the conjecture holds for binary de Bruijn networks with diameters up to 18. We prove that the asymptotic diierence, when the diameter goes to innnity, between the mean eccentricities of an arbitrary vertex and that of a a is smaller than a small constant tending to zero with the degree. We also provide a simple recursive scheme for the computation of the asymptotic mean eccentricity of the vertices a a. A by-product of our analysis is that in both directed and undirected de Bruijn networks, most of the vertices are at distance near from the diameter and that all of the mean eccentricities tend to the diameter when the degree goes to innnity.
36184486
Image-Based Surface Detail Transfer
We present a novel technique, called Image-Based Surface Detail Transfer, to transfer geometric details from one surface to another with simple 2D image operations. The basic observation is that, without knowing its 3D geometry, geometric details (local deformations) can be extracted from a single image of an object in a way independent of its surface reflectance, and furthermore, these geometric details can be transferred to modify the appearance of other objects directly in images. We show examples including surface detail transfer between real objects, as well as between real and synthesized objects.
10909052
Trust in the preservation of digital information
An institutional guarantee can help address the major hurdle of digital preservation---winning people's trust.
17231470
Dynamic scheduling of parallel computations
Structures of parallel programs are usually represented by task graphs in the scheduling literature. Such graphs are sometimes obtained at compile time. In many other cases, however, they can be determined only at run time. In this paper, we consider the scheduling of parallel computations whose task graphs are generated at run time. We analyze the case where the task graph is a random out-tree. When the number of offspring of a task has a geometric distribution whose parameter is decreasing and convex in the level, then the breadth-first policy stochastically minimizes the makespan. If, however, this parameter is increasing and concave, then the depth-first policy stochastically minimizes the makespan.