STRL STRL


Software Evolution

Theme leader: Martin Ward

Theme members: Feng Chen, Antonio Cau, Hongji Yang

Projects:
FermaT - UML.
    
SML
 
FermaT - DOC.
    
SML
 
FermaT Integrated Platform.
    
SML
 
Re-engineering Large programs
    with Program Transformations.
EPSRC
 
Program Migration.
    
SML
 

Technologies:
FermaT download flyer

Abstract:

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.











Feb 18 2014
Home | Training | Research | Members | About | News