Publications

We propose a formalism for modelling concurrent systems and for supporting stepwise refinement of concurrent systems. Our formalism allows one to describe the possible behaviours of a concurrent system in an operational manner, and to select from the operational description the desired behaviours using a logical approach. We discuss how our formalism can be used for incremental stepwise development where a high-level specification consisting of little operational aspect and largely logical assertions, is refined gradually into a low-lever specification consisting of mainly operational description and few or no logical dictations. We illustrate this refinement methodology with a simplified version of Lamport’s Bakery algorithm.

 It is a challenge for automatic tool support to formal design by refinement transformations. In this paper, we bring this matter to the attention of the research community and discuss a component-based model transformational approach for integrating refinement into software development tools. Models, their consistency and correctness, in an object-oriented and component-based development process are defined in rCOS, a refinement calculus recently developed at UNU-IIST. Correctness preserving transformations between models are formalized and proved as refinement rules in rCOS. In this paper, we will discuss on how these transformations can be implemented in the relations language of Query/View/Transformation (QVT) standardized by OMG.

 The RAISE Specification Language has no ``real time'' features. So, it is difficult to use it to specify real time applications. Now, we consider adding time to RSL. Our first attempt following Anne Haxthausen's proposal of encoding DC in RSL, we set up a proof assistant called DC/RJ. It is constructed from encoding of both DC semantics and proof system of Interval Logic and DC, and uses the RAISE Justification tool to do the verification for DC. In this paper, the author first introduces how DC can be integrated with RSL in detail. Then the construction and hierarchy of DC/RJ are explained. The Gas Burner example is used to show how DC/RJ works. A comparison among DC proof assistant systems, the problems and perspectives of our system are discussed at the end.

 A reactive system does not terminate and its behaviors are typically defined as a set of infinite sequences of states. In formal verification, a requirement is usually expressed in a logic, and when the models of the logic are also defined as infinite sequences, such as the case for LTL, the satisfaction relation is simply defined by the containment between the set of system behaviors and that of logic models. However, this satisfaction relation does not work for interval temporal logics, where the models can be considered as a set of finite sequences. In this paper, we observe that for different interval based properties, different satisfaction relations are sensible. Two classes of properties are discussed, and accordingly two satisfaction relations are defined, and they are subsequently unified by a more general definition. A tool is developed based on the Spin model checking system to verify the proposed general satisfaction relation for a decidable ubset of Discrete Time Duration Calculus. Keywords: model checking, finitary property, reactive system, interval temporal logic

 This paper presents an approach to formalizing and proving real-time properties of schedulers. The formal logic that we propose to use is the Duration Calculus, and the scheduler that we select here to serve as an example is the Deadline Driven Scheduling Algorithm. The specification and proof of the algorithm are formulated abstractly by using the Duration Calculus. The result may encourage others to formally treat more real-time aspects of operating systems which are conventionally a piece of ad hoc territory in computer science.