Publications

 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.

 This report aims at developing a technique for verifying if a timed automaton satisfies a linear duration constraint on the automaton states. The constraints are represented in the form of linear duration invariants - a simple class of Chop-free Duration Calculus (DC) formulas. We prove that linear duration invariants of a timed automaton are discretisable, and reduce checking if a timed automaton satisfies a linear duration invariant to checking if the integer timed region graph of the original automaton satisfies the same linear duration invariant. The latter can be done with exhausted search on graphs. In comparison to the techniques in the literatures, our one is more powerful; it works for the standard semantics of DC and general form of timed automata while the others cannot be applied.