Formalising progress properties of non-blocking programs

A non-blocking program is one that uses non-blocking primitives, such as load-linked/store-conditional and compare-and-swap, for synchronisation instead of locks so that no process is ever blocked. According to their progress properties, non-blocking programs may be classified as wait-free, lock-free or obstruction-free. However, a precise description of these properties does not exist and it is not unusual to find a definition that is ambiguous or even incorrect. We present a formal definition of the progress properties so that any confusion is removed. The formalisation also allows one to prove the widely believed presumption that wait-freedom is a special case of lock-freedom, which in turn is a special case of obstruction-freedom.

A tool for a formal pattern modeling language

This paper presents a formal but practical approach for defining and using design patterns. Initially we formalize the concepts commonly used in defining design patterns using Object-Z. We also formalize consistency constraints that must be satisfied when a pattern is deployed in a design model. Then we implement the pattern modeling language and its consistency constraints using an existing modeling framework, EMF, and incorporate the implementation as plug-ins to the Eclipse modeling environment. While the language is defined formally in terms of Object-Z definitions, the language is implemented in a practical environment. Using the plug-ins, users can develop precise pattern descriptions without knowing the underlying formalism, and can use the tool to check the validity of the pattern descriptions and pattern usage in design models. In this work, formalism brings precision to the pattern language definition and its implementation brings practicability to our pattern-based modeling approach.

A patttern based model evolution approach

In this paper, we present a framework for pattern-based model evolution approaches in the MDA context. In the framework, users define patterns using a pattern modeling language that is designed to describe software design patterns, and they can use the patterns as rules to evolve their model. In the framework, design model evolution takes place via two steps. The first step is a binding process of selecting a pattern and defining where and how to apply the pattern in the model. The second step is an automatic model transformation that actually evolves the model according to the binding information and the pattern rule. The pattern modeling language is defined in terms of a MOF-based role metamodel, and implemented using an existing modeling framework, EMF, and incorporated as a plugin to the Eclipse modeling environment. The model evolution process is also implemented as an Eclipse plugin. With these two plugins, we provide an integrated framework where defining and validating patterns, and model evolution based on patterns can take place in a single modeling environment.

Verifying metamodel coverage of model transformations

Since the object management group (OMG) commenced its model driven architecture (MDA) initiative, there has been considerable activity proposing and building automatic model transformation systems to help implement the MDA concept. Much less attention has been given to the need to ensure that model transformations generate the intended results. This paper explores one aspect of validation and verification for MDA: coverage of the source and/or target metamodels by a set of model transformations. The paper defines the property of metamodel coverage and some corresponding algorithms. This property helps the user assess which parts of a source (or target) metamodel are referenced by a given model transformation set. Some results are presented from a prototype implementation that is built on the eclipse modeling framework (EMF).

Axiomatisation of an Interval Calculus for Theorem Proving

We provide an axiomatisation of the Timed Interval Calculus, a set-theoretic notation for expressing properties of time intervals. We implement the axiomatisation in the Ergo theorem prover in order to allow the machine-checked proof of laws for reasoning about predicates expressed using interval operators. These laws can be then used in the machine-assisted verification of real-time applications.