My projects involve software engineering in some way, typically: object-oriented or component technology (e.g., UML, BON, Java, Eiffel, EJB, CASE tools, patterns, metamodelling), method integration, distributed systems, security, and formal methods. Inevitably they involve constructing some software (writing code or specifications), and may involve some maths. I am willing to consider self-defined projects in these areas.
There are lots of projects suggested here; I will supervise no more than my quota of projects, since otherwise I will not be able to do a good job. I try to balance projects between those running over the summer (i.e., MSc SWE and MSc IP) versus those running over the undergraduate year (i.e., MEng and BSc/BEng). I allocate projects based on: student ability to carry out the project; my level of interest in the project; balancing load across the year.
IMPORTANT NOTE: I will not discuss these projects until the project database is open. However, I'm happy to discuss self-defined projects in the interim.
(This project is co-supervised with Gerald Luettgen.)
Statecharts is a popular visual notation for designing reactive systems, which is based on hierarchical, concurrent state machines. The aim of this project is to -- both manually and with the aid of suitable automated tools -- extract statecharts from existing Ada source code. This is to be carried out in order to promote design understanding, to identify problems or areas for improvement with designs, and to provide documentation for designs that may have migrated from their initial conception, The Statecharts dialect of interest is Stateflow(r) by MathWorks, which is available as an add-on module to the company's successful Matlab/Simulink(r) design environment for control systems.
The deliverables of the project will include: Stateflow statecharts for subsets of a system, as well as recommendations and guidance on any supporting tools that were used to assist in the process. Challenges with this project include understanding a dialect of statecharts; understanding source code from a real system; and managing complicated, perhaps very messy statecharts.
Source code from real, industrial case studies will be provided where possible.
Readings:
The PVS system is an industrially applicable theorem prover and type checker based on higher order logic. It is strongly typed and provides semi-automatic support for reasoning. It has been successfully applied to a number of industrial verification tasks, e.g., microprocessor verification, software verification, compiler verification, etc. This project examines the use of the PVS specification language for object-oriented modelling. PVS provides no object-oriented constructs (e.g., classes, associations, objects, etc.) so the project will focus on designing an encoding of object-oriented models in PVS. In particular, the project can take two approaches:
Readings: K. Walden and J.-M. Nerson, Seamless Object-Oriented Software Architecture, Prentice-Hall, 1995. Available from the supervisor, and also as a PDF document from the authors.
G. Booch, J. Rumbaugh, I. Jacobsen, The UML Reference Guide, Addison-Wesley, 1999.
S. Owre et al., The PVS Specification Language, CSL-SRI Technical Report, September 1999. Available from The PVS Web Site.
Bunch theory is a simple set theory for specification. It represents unpackaged, unindexed data. You can think of a bunch as the contents of a set. Here are some examples of bunches:
This project will involve expressing bunch theory in the PVS specification language, and proving some sample theorems using the PVS automated theorem prover. Two approaches seem feasible: a direct axiomatization using [Hehner 1993], and an implementation of bunch theory using another PVS data structure. The two approaches should be compared and contrasted. It should be explained how to use PVS to specify and reason about bunch theory via examples and case studies.
The main challenge with this project is in determining the best way to represent bunches (though it will likely involve a set-based representation), and in becoming experienced with PVS.
Readings:
E.C.R. Hehner, A Practical Theory of Programming, Springer-Verlag, 1993.
S. Owre et al., The PVS Specification Language, CSL-SRI Technical Report, September 1999. Available from The PVS Web Site.
A UML profile is both a subset and extension of UML, tailored for some particular domain (for example, database systems, knowledge-based systems). A profile for knowledge-based systems has been developed at York by Syazwan Abdullah. This project aims at building an Eclipse plug-in to support the profile. The plug-in will allow profile-compliant diagrams to be drawn and checked, and XML/XMI representations produced. Challenges include: understanding Eclipse and its underlying metamodel, EMF; understanding the UML profile; and developing a GUI. It is to your advantage to have a reasonable amount of Java experience.
Readings:
www.eclipse.org for information on Eclipse
Mohd Syazwan Abdullah, A. Evans, I. Benest, R.Paige, C. Kimble. Modelling Knowledge Based Systems Using the eXecutable Modelling Framework (XMF), Proceedings of the IEEE Conference on Cybernetics and Intelligent Systems (CIS), Singapore, December 1-3, 2004. ISBN 0780386442, pp. 1054-1059.
Any reasonable book on UML, e.g., UML Distilled by Martin Fowler.
The Object Constraint Language is part of standard UML. It is used for writing constraints that can be applied to models, for example:
I expect this to be a challenging project. The semantics of OCL is unclear in many places, and there are likely many pitfalls in mapping it to a well-founded language like PVS. However, the potential for making a contribution to the UML development and to our understanding of OCL is great (this may lead to publishable work). I think the main challenge in this project will be in considering the alternatives for mapping OCL to PVS, and weighing the pros and cons of each.
Reading:
J. Warmer and A. Kleppe, The Object Constraint Language, Addison-Wesley, 1999.
S. Owre et al, The PVS Specification Language, CSL SRI Technical Report, Sept 1999, available from pvs.csl.sri.com
E.C.R. Hehner, A Practical Theory of Programming, Springer-Verlag, 1993.
In collaboration with Phil Brooke at the University of Plymouth, a graphical notation for Timed CSP has been created. Timed CSP is a formal language for specifying timed, concurrent, distributed systems. Timed CSP (TCSP) has tool support via the FDR model checker. The graphical syntax is to be used for more easily constructing larger TCSP specifications, and to help generate target code. The syntax is documented formally in the paper cited below. A prototype tool, written in Java/Swing, has been created for drawing and manipulating the models. It also generates XML code based on an existing DTD. The goal of this project is to implement the GTCSP syntax as a plug-in for Eclipse. The plug-in should support the functionality of the existing tool: drawing GTCSP diagrams, generating XML (based on the existing DTD that we will provide), and, if time permits, should implement metamodel constraints to validate the diagrams.
Reading:
P. Brooke and R. Paige. The Design of a Graphical Notation for Timed CSP. In Proc. Integrated Formal Methods 2002, LNCS, Springer-Verlag, May 2002.
Any book on Java/Swing, e.g., the Java/Swing Tutorial from Sun.
S. Schneider. Concurrent and Real-Timed Systems, Wiley, 2000.
www.eclipse.org for information on Eclipse
The Eiffel programming language (www.eiffel.com) is a clean, expressive, powerful object-oriented language supporting single and multiple inheritance, generic types, covariance, and contracts. There are two powerful compilers available for it: Eiffel Studio from ESI, and the GNU Smart Eiffel compiler. Both generate C code from Eiffel. In both cases it is difficult to see the relationship between the Eiffel code and the C code. This project aims at defining and prototyping (parts of) a seamless Eiffel-to-C compiler. The emphasis will be on designing and implementing the simplest possible translation of each Eiffel construct. The main mapping will be to translate each Eiffel class to a .h/.c file, dynamic dispatch to a virtual function table, and method dispatch to function pointers.
This is an open-ended project: we shall define a subset of Eiffel to attack, and as much emphasis should be put on designing a seamless mapping as in implementing it efficiently. It is to your advantage to have taken a course on compilers (particularly code generation) and you should be a good C programmer. You should also be familiar with at least one OO language (Eiffel preferably, but this isn't required).
Reading:
Documentation on Eiffel at http://www.eiffel.com
GNU SmartEiffel available at http://smarteiffel.loria.fr/
When describing systems using UML, different diagrams are used, e.g., class and communication diagrams. These diagrams can be inconsistent, and rules have been defined to capture what consistency means for different diagram types. This project aims at using an OCL engine to capture and carry out multi-view consistency checking in UML. Two UML diagrams will be chosen (e.g., class and sequence diagrams), rules for consistency expressed in OCL, and an OCL engine used to simulate the rules against sample models. The difficulties associated with using the OCL engine for this process will be studied. It is expected that either the KMF OCL engine, or an alternative, will be used. Challenges include capturing the rules in OCL, understanding the OCL engine, and processing feedback from rule failures. You need to be comfortable with UML and OCL (e.g., from taking the OOD module or MSD module).
Reading:
UML information available at http://www.omg.org/uml
OCL information available at http://www.klasse.nl/ocl/
KMF OCL engine available at http://www.cs.kent.ac.uk/projects/kmf/
A software product line (SPL) is a set of software-intensive systems that share a common, managed set of features satisfying the specific needs of a particular market segment or mission and that are developed from a common set of core assets in a prescribed way.
Software product lines are rapidly emerging as a viable and important software development paradigm allowing companies to realize order-of-magnitude improvements in time to market, cost, productivity, quality, and other business drivers. Software product line engineering can also enable rapid market entry and flexible response, and provide a capability for mass customization.
Agile development techniques (like XP, Feature-Driven Development) aim to be responsive to change, while providing flexible development processes that de-emphasize documentation. There is an apparent disconnect between the requirements of building SPLs and the facilities offered by agile development.
This project aims at exploring the feasibility of using Agile techniques to build SPLs. It will start with a thorough overview of the requirements of SPL development and the characteristics of agile development techniques. A proposal for where agile techniques could help in building SPL will be made, and a methodology proposed. The methodology will then be used in a small case study illustrating the approach.
Reading:
Product line documentation at http://www.sei.cmu.edu/productlines/
Agile documentation available at http://www.agilealliance.org/home
TXL is a language transformation tool due to Jim Cordy at Queens University, Canada. When using TXL, two or more grammar specifications of languages are provided (e.g., a C grammar and a Java grammar). Transformation rules are then described which show how one language is transformed into the second language. The transformations can be partial and algorithmic, and emphasise reuse - rules defined for transforming one set of language constructs can be used to transform new constructs.
This project will focus on using TXL to define transformations of modelling languages, particularly transformations applied to UML. The focus will be on transforming a profile (subset) of UML class diagrams to a programming language, e.g., Java or C++. Challenges include: learning TXL, defining UML class diagrams using XML/XMI in TXL, and defining the mapping. A set of small examples will be carried out to show how the TXL tool works in this domain.
Reading:
TXL information at www.txl.ca
An overview of the process in the paper Towards Model Transformation with TXL, available from the supervisor.
In collaboration with Phil Brooke, University of Plymouth, an abstract architecture for networked multiplayer games (similar to, e.g., Half-Life Firearms) has been produced. The basic idea is to partition functionality - scenario processing, ambient processing, security - amongst several processes (possibly distributed over several machines) and to assume that (simple, possibly differently enabled) clients are untrustworthy. This project can involve one or two of the following elements:
Reading:
Rudy Rucker, Software Engineering and Computer Games, AWL, 2003. Available in the library.
A. Rollings and D. Morris, Game Architecture and Design, Coriolis, 2000. Available in the library.
OCL is the standard constraint language for UML. The Eiffel programming language supports a construct called agents, which is essentially an iterator. Agents have been used to implement quantifiers (e.g., forall and exists) as well as traversal algorithms. This project will design and implement a translator for mapping OCL into Eiffel agents. Potential incompatibilities will be identified, and a prototype translator implemented in a suitable translation engine will be produced. You will need to be comfortable with object-oriented programming (experience with Java is helpful), and have some background with UML and OCL (e.g., through MSD or OOD).
Reading:
UML information available at http://www.omg.org/uml
OCL information available at http://www.klasse.nl/ocl/
Eiffel information (including agents) available at www.eiffel.com
A tool is required to provide two-way translation of text between an architectural description language and its XML representation. The notation in question is AIM, developed in the DARP HIRTS project at the University of York. The student will be provided with the description of AIM (particularly its grammar in BNF form), and its equivalent XML Schema, and a two-way mapping will be designed and implemented. The ideal implementation platform is C# under .NET, but C++, Delphi, and Java are alternatives that could be considered. A clear justification for choosing an implementation platform is a part of the project. The deliverables include a clear set of mapping rules (i.e., AIM constructs to XML, XML schema constructs to AIM), an implementation of both mappings, and several small case studies illustrating how to use the mappings and their supporting tools.
The AIM notation (and schema) is stable at the moment. However, minor modifications and extensions are anticipated and the tool should be flexible enough to support these changes.
Reading:
AIM architectural notation, documentation available from the supervisor.
L. Bass, P. Clements, and R. Kazman, Software Architecture in Practice, AWL, 2000.
C# information, available from Microsoft at http://msdn.microsoft.com/vcsharp/
XML information, available at http://www.xml.com/. The material on XML schema is particularly important: http://www.xml.com/schemas/
This project aims at developing a small UML profile and a lightweight development process for building safety critical C++ systems, achieving at least SIL1/SIL 2 level. It will consider selecting diagram elements of UML that are both useful for building safety critical systems, and feasible for achieving SIL1/2. It will also aim to briefly examine the issue of autocode generation for safety critical C++.
The deliverables of this project include:
References:
R. Hawkins, I. Toyn, and I. Bate. An Approach to Designing Safety Critical Systems using UML. Proc. Workshop on Critical Systems Development with UML, TU Munich, 2003.
J. Jurjens, Developing Safety Critical Systems with UML. TU Munich, 2003.
D. Reinhardt, Use of the C++ Programming Language in Safety Critical Systems, MSc SCSE Project, 2004.
MODELWARE is a European Sixth Framework Programme project to enable the large scale industrial exploitation of Model-Driven Development (MDD) through the development of tooling and patterns. The aim is to move modelling from being an aid to the requirements gathering and design process, to being integral to the entire software engineering lifecycle, through execution and test. The continued development of UML and subsets provides an extensible notation which can be used for the description of models relevant to the stages of the development process.
The transformation of models between these stages is at the core of the MODELWARE project. Tools to support MDD must ensure the consistency of models generated through potentially sophisticated transformations. By attaching extra information at the meta-level, the provenance of model elements can be traced from initial requirements.
The aim of this project is to develop algorithms and tools to guarantee (or check) the traceability and consistency of models as they undergo these transformations. This will be carried out by building a MOF-level extension to include versioning information, and by extending IBM's MDA Alphaworks tool with this versioning information, so as to support traceability. Both the metamodel implemented in the tool, and the transformation engine, will need to be extended to support versioning. Challenges include understanding the MOF metamodel and its extension; implementation the extension in the Alphaworks tool; and carrying out a case study to evaluate the extension. The metamodel extension is not difficult: it requires adding time and date-stamp information to modelling elements. Making the transformation engine aware of these extensions is moderately more challenging.
Reading:
MODELWARE web site: http://www.modelware-ist.org
Selected papers on model versioning in proceedings of Workshop in Software Model Engineering (WiSME'04}: http://www.metamodel.com/wisme-2004/programme.html
A hypothesis that is made in parts of the model-driven development community is that some refactorings are very hard to do once a system architecture has stabilized. One of these posited refactorings is for security, i.e., adding authentication, authorization, and audit facilities. This project aims at proving (or disproving) this hypothesis by means of a careful experiment. The experiment will proceed as follows.
Reading:
http://csdl.computer.org/comp/proceedings/icsm/2004/2213/00/22130492.pdf
http://csdl.computer.org/comp/proceedings/eee/2004/2073/00/20730025abs.htm
http://www.webopedia.com/TERM/W/Web_services.html