Publications

 This paper presents a formalization in the duration calculus (DC) of scheduling policies for tasks with shared resources. Two frameworks are presented for specifying classes of schedulers. With these specifications, some properties of these schedulers were proved using the formal deduction of DC. This paper aims to encourage other researchers to formally treat real-time aspects of operating systems which in the past were conventionally a piece of ad hoc territory in computer science.

 In this report, we introduce a Probabilistic Duration Calculus (PDC) as a probabilistic extension of Duration Calculus to express dependability requirements for real-time systems, and develop a technique to check a Durational Probabilistic System for a Probabilistic Linear Duration Invariant of PDC.

 Duration Calculus of Weakly Monotonic Time (WDC) is an extension of DC to allow description of discrete processes where several steps of computation can occur at the same time point. In this paper, we introduce Linear Occurrence Invariants (LOI) which is a subclass of WDC formulas and give an algorithm to check real-time automata for LOI using integer programming. LOI can be used effectively to specify system requirements in some cases including when the system is considered under the true synchrony assumption. We also extend WDC probabilistically to express dependability requirements of real-time systems and develop techniques to check deterministic probabilistic real-time automata for a class of probabilistic WDC formulas.

 This paper introduces infinite intervals into the Duration Calculus. The extended calculus defines a state duration over an infinite interval by a property which specifies the limit of the state duration over finite intervals, and excludes the description operator. Thus the calculus can be established without involvement of unpleasant calculation of infinity. With limits of state durations, one can treat conventional liveness and fairness, and can also measure out liveness and fairness by properties of limits. Including both finite and infinite intervals, the calculus can, in a simple manner, distinguish between terminate behaviour and nonterminate behaviour, and therefore directly specify and reason about sequentiality.

 In this paper we study a way to verify real-time systems using untimed model checking tools through an industrial case study with standard SPIN. We introduce a class of Duration Calculus whose formulas correspond to regular expressions over the set of special symbols, each of which is a state occurrence for one time unit or for less than one time unit. The length of a string reflects a time constraints. These regular expressions can easily be translated into untimed automata or a SPIN model. Then, we can verify real-time systems in the same way as for untimed systems with standard SPIN. The case study used in this paper is the well-known Bi-phase Mark Protocol.

 In this paper, we consider the problem of checking hybrid systems modelled by hybrid automata for a class of duration properties called linear duration invariants, which are constructed from linear inequalities of integrated durations of system states. Based on linear programming, an algorithm is developed for checking a class of hybrid automata for linear duration invariants

 In this paper, the problem of verifying a timed automaton for a Duration Calculus formula in the form of linear duration invariants is addressed. We show that by linear programming, a particular class of timed automata including the class of real-time automata as a proper subset, can be checked for linear duration invariants. The so-called real-time regular expressions is introduced to express the real-time behaviour of the timed automata in this class. Using real-time regular expressions, an algorithm based on linear programming is presented for checking an automaton in the class with respect to a linear duration invariant.

 In this paper, we consider the problem of checking hybrid systems modelled by hybrid automata for a class of duration properties called linear duration invariants, which are constructed from linear inequalities of integrated durations of system states. Based on linear programming, an algorithm is developed for checking a class of hybrid automata for linear duration invariants.

 The notion of contract was introduced to component-based software development in order to facilitate the semantically correct composition of components. We extend the form of this notion which is based on designs to capture probabilistic requirements on execution time. We show how reasoning about such requirements can be done in an infinite-interval-based system of probabilistic duration calculus.

 In this paper we present an approach to safety verification of Air-Traffic Control Systems (ATC) using probabilistic real-time model-checking. Namely we use ATC as a case study for the formal analysis of real time systems whose performance depends on uncertain or probabilistic behaviors. We construct a probabilistic timed automata model for ATC by extending the Operator Choice Model (OCM), a model of operators' behaviors in ATC system, with timed and probabilistic assumptions. Some properties of this system are then expressed in probabilistic real time computation tree logic (PCTL). The verification results produced by using the tool PRISM illustrate the uses of this approach to better understand the human errors in real time systems.

 In this report we propose a simple model for component based real-time systems using duration automata. A component based real-time system consists of a host which is a general duration automaton and several components which are duration automata with some restrictions. Components can communicate with the host only. For this model we propose an algorithm for solving the emptiness problem using black box testing for components and with a complexity in the same complexity class as for solving the emptiness problem for untimed component based systems. Furthermore, the verification of behavioural real-time properties in this model can be done with techniques from Duration Calculus.

 The present paper gives a systematic way to refine specifications of hybrid control systems written in DC (Duration Calculus) into their automata models. The iteration DC formulas are introduced together with rules for transforming, refining DC formulas into the forms that describe the systems in more details. Then, the plant automata derived from DC formulas are defined, which allow the designers to derive a specification of control automata more easily. A necessary and sufficient condition for a plant automaton and a requirement to have a control automaton is given. Some simple examples are presented to illustrate the method

We present a linear time algorithm for improving the time efficiency for a partition of a computing system into a parallel program with synchronous communication based on the program syntax. The technique can be used for for optimizing parallel and distributed systems or in hardware/software codesign.

 This paper addresses the problem of modeling railway systems. We use both Mean Value Calculus and Extended Duration Calculus to specify railway systems. For railway line, signal system is discussed and a simple scheduling strategy is presented, which result in safety and liveness of railway line; For linear railway region, both running map and feasibility conditions are described. The framework to verify correctness of scheduling, i.e. the running map satisfies feasibility conditions, is also presented.

 The paper presents an approach to the specification and verification of real-time hybrid systems using Duration Calculus (DC). By introducing a formula {\sl int} to DC to express the intervals of time between two ticks of the system clock, it is shown that DC can be used to specify both the digital states and the analog states as well as to reason about time in distributed systems. We illustrate our approach by giving an intuitive model for the communication protocols in which the verification can be done by using the familiar natural induction rules.

 The paper presents a model of Biphase Mark Protocols (BMP) using Duration Calculus, which seems to be more general and more intuitive than the others in the literature. With Duration Calculus we can model the behaviour of the bus in a natural way and in more detail. The model makes it possible to specify and verify BMP using PVS/DC tool. The mechanical verification not only ensures the correctness of the protocol, but also helps engineers to choose the optimal values for the parameters given the ratio between the clock rates of the sender and the receiver and the time for changing the signal from high to low and low to high.

 This paper deals with dependability of imperfect implementations concerning given requirements. The requirements are assumed to be written as formulas in Duration Calculus. Implementations are modeled by continuous semi-Markov processes with finite state space, which are expressed in the paper as finite automata with stochastic delays of state transitions. A probabilistic model for Duration Calculus formulas is introduced, so that the satisfaction probabilities of Duration Calculus formulas with respect to semi-Markov processes can be defined, reasoned about and calculated through a set of axioms and rules of the model.

 The aim of this work is to develop a template for component-based programs which can be used in different programming languages. First, we give a model of component based systems based on the unifying theory of programming. We define the concepts interface, contract and component, and component combination. The definition can be used as the basis for the component template development. We define a contract to include method specification, and define a component as an implementation of a contract. This implementation may require services from other components with some assumptions about the schedule for resolving the conflict of shared method and resource uses with the presence of concurrency. The assumption is expressed as interaction protocols. In our model, components are correct by its design. We then give a guideline for extending the model for real-time component systems.