Publications

 A mean value calculus is presented. It is an extension of the Duration Calculus. The calculus reasons about mean values of durations of Boolean functions instead of integrals. With mean values, we can define integrals and specify point values of functions, and therefore instant actions, including state transitions and events. A state transition of a system determines the system states in a neighbourhood of the transition, and is called a state germ using terminology from topology. State transitions of an automaton are caused by events. Thus the behaviour of an automaton can be formulated by predicates of events and state germs. As an application of the calculus, state germs and their inference rules are introduced and are used to specify and reason about combinational circuits and automata. {\bf Keywords:}Duration Calculus, Mean Value Calculus, State Germs,Combinational Circuit, Automata,Real-Time System.

 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.

 This paper is to present an algorithm to decide whether a real-time system satisfies a set of invariants which are constructed from linear inequalities of integrated durations of system states. Real-time systems in the paper are taken to be real-time automata which set up for each of state transitions a lower time bound and an upper time bound. The satisfaction problem can be translated into a family of {\em linear programming problems}. The algorithm is, according to the invariants, to reduce the infinite family of linear programming problems to an equivalent one with only finite members, and then to solve each of linear programming problems efficiently. The algorithm is so simple that no prerequisite of linear programming theory is assumed.

This report introduces a component calculus, whereby a system can be divided into a number of interconnected components. We model the behaviour of individual service by a design, which enables one to separate the responsibility of clients from the commitment made by the system. We adopt the notion of refinement to formalise the replaceability of components. This allows developers to improve the system performance by reorganising its data components.

 This paper presents a predicative semantic model for integrating models from UML class diagrams and sequence diagrams. The integrated model is used for dealing with consistency problems of UML class diagrams and sequence diagrams. We also define the notion of consistent refinement of these integrated models.

 This report presents a general method to cope with hybrid control system specification and verification by making full use of both the simplicity of finite automata and the excessive expressing power of Mean Value Duration Calculus. The method consists of four steps: First, specify the requirements of the whole system through Mean Value Duration Calculus formulas. Second, use two real-time communicating automata to characterize the design decisions, which describe the plant and control subsystems respectively. Third, translate the automata into Mean Value Duration Calculus formulas. Finally prove the design decisions conforming to the requirements specification. Taking the steam-boiler problem raised by J.-R. Abrial[1] as a running example, we demonstrate the above method in three versions of abstractions. Each version represents an abstract level for capturing the original problem requirements and provides a complete procedure of applying the above method. In addition to specifying safety property, emphasis is put on capturing non-functional requirements such as performance, reliability, and optimization. Some formal design techniques about finding an optimal implementation conforming to the system specification are also discussed.

 A Mean Value Calculus based formal method is provided in this report to specify and verify the steam-boiler control problem raised by J.-R. Abrial[1] for Dagstuhl seminar. In addition to specifying safety property, emphasis is put on capturing non-functional requirements such as performance and optimization. Some formal design techniques about finding an optimal implementation conforming to the system specification are also discussed.

We present a model for component software. We describe how components are specified at the interface level, design level and how they are composed. From its external view, a component consists a set of interfaces, provided to or required from its environment. From its internal view, a component is an executable code that can be coupled with other components via its interfaces. The developer has to ensure that the specification of a component is met by its design and implementation. We also combine component-based and object-oriented techniques in component-based software development This report is a refined version of UNU-IIST Report 276 and is to be presented at and published in the proceedings IFIP WCC-TCS2004, 24-26 August 2004, Toulouse, France.

 We present a method for automatically generating a prototype from a UML model of system requirements that consists of a use-case model and a conceptual class model. The method is based on a formalization of UML in which a use case is formally specified by a pair of pre and post conditions in the context of a conceptual class model. To generate a prototype, we translate the pre and post conditions of a use case into a sequence of executable atomic actions. These actions are to create or delete an object, update an object, establish or remove a link between two objects with respect to an association. Such a prototype can be used to validate requirements and check system invariants. An automated prototype generator is developed in Java, and a simple library system is used as an example to illustrate the feasibility of the method.