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-directed 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.
[Note to Students (Updated 8 March 2004): all of my project places have been allocated; unfortunately I cannot supervise any additional projects.]
(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.
Object-Z and BON are languages for the (formal and precise) specification of object-oriented systems. There are similarities between the notations (e.g., both have graphical elements, both build on set theory and predicate logic, both support a core suite of OO constructs such as inheritance and composition). And there are differences as well (Object-Z has a formal semantics while BON has a different partial formal semantics, BON supports reference types, etc). A translator from BON to Object-Z has been implemented in the BON-CASE tool. It generates LaTeX files. An alternative representation of Object-Z is XML/XMI, as proposed by Jin Song Dong and supported by his toolset (see reference below). This project will involve extending the existing code generator to produce XML/XMI.
The challenges with this project include understanding an existing code generator, adapting an XML/XMI DTD, and substantial software testing.
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.
R. Duke and G. Rose. Formal Object-Oriented Specification using Object-Z. Palgrave, 2000.
J. S. Dong et al. Z Family on the Web and their UML Photos. Available at Jin Song's web page.
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
Eclipse (www.eclipse.org) is an extensible IDE. Numerous plug-ins for different programming and visual language (such as C++ and UML) have been created for it. AADL -- the Architectural Avionics Description Language -- is a primarily text-based language for described avionics architectures. It is a standard being proposed by the US Military. It has a standard syntax, a rigorous semantics, and tool support.
This project will involve the design and implementation of an Eclipse plug-in for AADL, so that AADL descriptions can be entered and syntax checked.
Challenges with this project include: learning and understanding how to build Eclipse plug-ins; understanding AADL and its syntax and semantics; designing features and functionality to implement beyond mere syntax checking and highlighting. For example, type checking would be suitable to implement, as would other lightweight semantic checks and analyses. It is expected that a reasonable, comprehensive subset of AADL will have to be implemented for this project.
Reading:
Eclipse documentation available at the Eclipse community page: www.eclipse.org
AADL tutorial available at: http://www.axlog.fr/R_d/aadl/seminar.html
(This project is related to project RFP/7. You should also read that project proposal to learn something about Eclipse and AADL.)
SysML is a proposed graphical syntax for AADL (see RFP/7). It has a number of similarities to the Unified Modelling Language, UML, but is tailored specifically for system modelling (incl. architectures) and as such adds features that are very useful for avionics system modelling.
This project will entail building an Eclipse plug-in for SysML. SysML is a large language, and as such the first step will involve selecting those diagram elements that are to be implemented. Challenges are very similar to project RFP/7: learning both Eclipse and SysML, and deciding what functionality to provide with the plug-in. Given that SysML is a graphical notation, it is expected that more time will be spent on designing and implementing the GUI for the plug-in instead of adding new functionality.
Reading:
As for RFP/7.
SysML partners web page at http://www.sysml.org/
Contracts are used in object-oriented design for capturing benefits and obligations on classes. They are also used in designing components (e.g., CORBA components), and in use case modelling. This project will involve a thorough literature survey and analysis of the different types of contracts that are described in the literature and used in practice. The investigation will include:
Reading:
B. Meyer, Object-Oriented Software Construction, Second Edition, Prentice-Hall, 1997.
R. Mitchell and J. McKim, Design by Contract by Example, AWL, 2001.
Proceedings of TOOLS USA 2002, available from me.
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.
Fault tree analysis (FTA) is a `method for acquiring information about a system' [1]. It is regularly referenced in the context of developing safety-critical, i.e., high-integrity software. The aim in these contexts is to analyse a system design to identify areas of risk (which can then be addressed). There are a number of commercial tools [2] which support the method by providing drawing and probabilistic calculation facilities.
[3] recently applied FTA to determining risks in security critical systems. This project will involve building a simple Java based tool for drawing secure fault trees as in [3], which should also include functionality for integrating a library of templates (ie., recurring security problems). It is not generally in the scope of this project to research taxonomies of security problems, but contributions along these lines are certainly possible. The tool should allow input and editing of templates in a standard format to be determined by reading the fault tree and security literature.
Deliverables include the Java tool (built using Swing components), and a simple pattern for describing security problems.
Reading:
1. US Nuclear Regulatory Commission, Fault Tree Handbook, {NUREG}-0492 (January 1981).
2. Fault tree analysis programs, http://www.enre.umd.edu/ftap.htm, materials and Engineering Department, University of Maryland.
3. P.J. Brooke and R.F. Paige. Fault Trees for Security System Analysis and Design, Journal of Computers and Security, 22(3):256-264, Elsevier, May 2003
The theme of this project is to model software systems using domain specific modeling techniques, and reduce writing of redundant code using automated code generation based on these models. The approach is make use of implementations of metamodel of domain specific modeling languages. The domain to be considered in this project will be information systems (e.g., accounting, e-finance) domain, though analysis will also be applied to the real-time systems domain as it offers a number of differences.
The first step will be to define the domain meta-model (the concepts of the domain). The second step will be to create models that comply with the meta-model. Next, we will generate a set of components, that represent the meta-model concepts and that are able to parse models. The final step is to script these components using a scripting environment (e.g., an ASP-like mechanism) in order to produce (code) artifacts from the metamodels.
The specific goals of this project are to find, define, and extend a suitable meta-modeling language and a mechanism for the transformation of models to scriptable components. At this point, XML Schema Definition (XSD) is considered (along with some extensions) to be a good candidate, and it will be the initial technology used for representing and scripting components.
The project will develop an architecture and an efficient set of algorithms to deal with the problem involved in broadcasting deformation changes to the models of objects in multiplayer gaming environments. For example, if a player fires a rocket at a wall and it makes a hole in it, all of the other players must see the hole as well. These updates have to be performed in near real-time, but must not have a significant impact on the latency or frame rate of the game. Broadcasting such changes to all players must be carried out in a reliable way, so that all players have a consistent view of the world.
The goal of the project is to produce a working (though prototypical) solution to the deformation problem which can handle a large number of players (based on analysis of typical multiplayer games, a number in the range of 50-75 will be considered) using a client-server architecture, based on the publish-subscribe paradigm. The implementation solution will restrict itself initially to one type of deformable object (e.g., walls) so as to reduce the need to consider complicated deformation models of different types of shapes, but the design will consider multiple types of deformable objects. If time is available, the implementation will include multiple deformable objects. The implementation will likely modify an existing graphics engine (for example, Crystal Space - http://crystal.sourceforge.net) if appropriate.
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.
D. Bauer, S. Rooney, and P. Scotton. Network infrastructure for massively distributed games. IBM Research, Zurich Laboratory, Technical Report, 2003.
A. Bharambe et al. Mercury: a scaleable publish-subscribe system for Internet Games, Technical Report, School of Computer Science, Carnegie-Mellon University, 2003. [Also published in Proc. NetGames 2003].