Theme leader: Martin Ward
Our advances under this theme have concentrated on program transformations and their realization within our industry-strength tool-set FermaT. We have introduced a compositional and practical technique for extracting formal specification from large-scale legacy systems. We have also introduced some generalisations of traditional slicing, amorphous slicing and conditioned slicing, which are possible in the framework of Wide Spectrum Languages (WSL) transformations. One generalisation is ``semantic slicing'' which combines slicing and abstraction to a specification. Conditioned slicing can be applied to reverse engineering problems which involve the extraction of executable fragments of code in the context of some criteria of interest.
We have also introduced ConSUS, a conditioner for WSL. The symbolic executor of ConSUS prunes the symbolic execution paths, and its predicate reasoning system uses the FermaT Simplify transformation in place of a more conventional theorem prover. We have also shown that this combination of pruning and simplification-as-reasoner leads to a more scalable and powerful approach to conditioning.
In additiom, we have also introduced the Representation Theorem of WSL that allows us to show that for any WSL program there exists a WSL specification which implements that program. This finding provides a very practical implemetation of Conditioned Semantic Slicing via both abstraction and refinement.
Further, scalable and provably correct technique for extracting UML diagram from legacy code has been successfully implemented in FermaT and used in a large scale application in the tele-communication domain.
Another fundamental achievement is the establishment of a framework
known as K-Mediator (here 'K' stands for Knowledge) which is a
basis for a sound theory of Co-Evolution for Information System
(IS) design and the development of its underlying IT. The K-Mediator
framework could be viewed from different levels of abstractions. At a
conceptual level, the framework provides the role of an architect in
the procurement process which results in making decisions at an early
stage of software development life cycle. At a concrete level, the
framework provides a set of business-specific components from which a
system may be constructed and configured/re-configured rapidly and
efficiently from new or existing business components. Three main
attributes must therefore be satisfied for such component-based
development infrastructure. Components must be able to be plugged
together easily. Agility is another important characteristic for it
permits rapid modifiability. For business-critical applications, high
integrity is fundamental as it ensures high level of assurance through
'provably correct' components. A key advantage of such a rapid
assembly is that the assembler, who is also playing the role of a
'mediator', has a clear understanding of the business goals. Hence the
constructed system is guaranteed to be driven by the business need; a
requirement that is crucial for the success of the
system. Additionally, a gained advantage is that system requirements
need not to be captured (or negotiated) as the 'mediator' can freely
articulate system's intentions through components selection without
the intervention of a technology expert. This view is predicated on
the need for fast product development, turbulence in the business
environment, semantic inoperability, the individual nature of
requirements and the limited availability of IT resources due to
downsizing and outsourcing.