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, and formal methods. Inevitably they involve constructing some software (writing code or specifications), and may involve some maths.
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.
A CASE tool for drawing, manipulating, and storing object-oriented models in the BON modelling language has been constructed. BON, effectively, is equivalent to an Eiffel profile of UML, and supports modelling of static structure (e.g., via class diagrams that show classes, packages, interfaces, and relationships) and dynamic structure. The tool, implemented in Java/Swing using the GEF framework of the University of Southern California, currently supports static class diagrams, collaboration diagrams, use-case diagrams, generates XML and JML code, and implements most of the BON metamodel. A number of projects are possible, related to studying, evaluating, extending, and improving the CASE tool:
A key challenge with these projects is understanding an existing, substantial system. Additions (1), (2), and (4) above are more challenging than the preceding two. For the last addition, understanding the internal representation of images in BON-CASE will be essential. Adding the other new features and functionality to the CASE tool should not be overly difficult, given the extendible nature of its design.
Readings:
K. Walden and J.-M. Nerson, Seamless Object-Oriented Software Architecture, Prentice-Hall, 1995.
G. Booch, J. Rumbaugh, I. Jacobsen, The UML Reference Guide, Addison-Wesley, 1999.
The Argo/UML Tool documentation, available from www.argouml.org (the BON CASE tool is constructed using the framework of Argo/UML)
R. Paige, J. Ostroff, L. Kaminskaya, and J. Lancaric. BON-CASE: an Extensible CASE Tool for Formal Specification and Reasoning. Journal of Object Technology 1(5), 2002.
G. Leavens et al. Preliminary Design of JML, Iowa State Technical Report, available from www.cs.iastate.edu/~leavens/JML.html
The OMG. Meta-Object Facility Specification. Available at www.omg.org.
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 (see RFP/1). 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. However, it does not generate code. This project will involve extending the existing tool to output text representations of graphical TCSP models in XML/XMI. A DTD exists that can be used as the basis for the code generator. Challenges include understanding an existing piece of software, conformance testing (i.e., checking automatically generated XML against the DTD), and in building a code generator using an existing Java parser package, e.g., ANTLR, Java CUP, etc.
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.
The BON-CASE Tool is described in more detail in RFP/1; it is a CASE tool for the BON language. This project will involve modifying the presentation style (i.e., the concrete syntax) for BON-CASE and to produce a UML version of the tool. This will involve modifying the GUI, the internal representation of models in textual format, and will involve some minor modifications to the metamodel. Challenges include understanding the existing architecture, and in rewriting BON metamodel constraints to apply to UML.
Readings:
K. Walden and J.-M. Nerson, Seamless Object-Oriented Software Architecture, Prentice-Hall, 1995.
G. Booch, J. Rumbaugh, I. Jacobsen, The UML Reference Guide, Addison-Wesley, 1999.
The Argo/UML Tool documentation, available from www.argouml.org (the BON CASE tool is constructed using the framework of Argo/UML)
R. Paige, J. Ostroff, L. Kaminskaya, and J. Lancaric. BON-CASE: an Extensible CASE Tool for Formal Specification and Reasoning. Journal of Object Technology 1(5), 2002.
G. Leavens et al. Preliminary Design of JML, Iowa State Technical Report, available from www.cs.iastate.edu/~leavens/JML.html
The OMG. Meta-Object Facility Specification. Available at www.omg.org.
The Eiffel Refinement Calculus (ERC) was designed to allow provably correct Eiffel object-oriented programs from specifications. It does many of the same things as the B-Method, except in the object-oriented realm, and it targets an immediately executable language. A full set of refinement rules and techniques are available. This project will involve using the ERC in a detailed case study: reformulating the B-Bank (citation below) as an Eiffel specification, and refining it to immediately executable code. The B-Bank is a simulation of a bank (with a GUI). A detailed B refinement is in the citation below. It will provide guidance in carrying out the Eiffel refinement.
Challenges with this project include: obtaining some mastery of the Eiffel OO language, including reference types; understanding the process of refinement; precisely and clearly documenting a substantial refinement. The proof obligations to be discharged in refinement will not be unduly complicated; and the B version of the case study will prove very helpful in suggesting classes and contracts for refinement. A tool for automatically generating proof obligations may be explored as well.
Reading:
R. Paige and J. Ostroff. ERC - the Eiffel Refinement Calculus. Technical Report CS-TR-2001-05, York University, Canada. Available from the authors.
M. Buchi. The B Bank. In Program Development by Refinement, E. Sekerinski and K. Sere (eds.), FACIT Series, Springer, 1999.
B. Meyer. Eiffel - the Language, Prentice-Hall, 1992.
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.
The Compaq Extended Static Checker for Java (ESC/Java) is a modelling tool for finding errors in Java programs. ESC/Java detects, at compile time, common programming errors that are ordinarily not detected until run-time (if then!), such as NULL dereferences, array bound errors, type cast errors, and race conditions. ESC is based on theorem prover technology, but to the programmer it appears more like a type checker. It is an automated technology, focusing on finding specific types of errors, and sacrificing completeness. ESC includes an annotation language with which programmers can express design decisions using lightweight assertions, eg., pre- and postconditions, object invariants, etc.
In this project, an implementation of a metamodel - a set of model well-formedness constraints for an object-oriented modelling language - will be analyzed using ESC/Java. The metamodel is implemented in terms of the BON-CASE tool described in RFP/1. The project will focus on (a) completing the implementation of the metamodel in the BON-CASE tool; (b) annotating the metamodel portion of the tool with ESC/Java assertions; and (c) analyzing the implementation using ESC/Java. Primary challenges with this project include: understanding the metamodel and its implementation, and interpreting the results produced by ESC/Java.
Reading:
ESC/Java documentation. Available at SRC.
Documentation for the BON-CASE tool. Available at Eiffel@York.
This project will involve applying design by contract techniques, along with UML modeling, to the construct of an interactive game. Patterns for game design will be researched and applied in the process of building the gaming infrastructure and the GUI. The emphasis of this project is on drawing conclusions on
You should be proficient with C or C++ and have some familiarity with UML and object-oriented techniques in general; even though the game may be implemented in a non-OO language, contracts are often expressed in an OO style.
Reading:
B. Meyer, Object-Oriented Software Construction, Second Edition, Prentice-Hall, 1997.
Rudy Rucker, Software Engineering and Computer Games, AWL, 2003. Available in the library.
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.
University Radio York (URY) currently plays all its music and jingles from CDs and MiniDiscs (MDs). Discussion and investment has been put into transferring the music collection onto a computer system, but progress has been slow. This project would involve a number of elements of designing and implementing a system to manage music for URY.
Requirements for a computer assisted radio studio were previously defined some time ago; this project would firstly check that the previously defined requirements meet current needs, and then specify and build a high-reliability system which presenters can use to present an entire show without the use of CD and MD players. This would be especially useful for Outside Broadcasts, and there will be at least two opportunities during the duration of the project to test the system on an Outside Broadcast: Battle of the Bands (Beginning of Spring term) and SU Elections results night (Spring week 9).
The project will not aim to design and build the system which stores the music, but it will aim to design, test and build a robust interface for presenters. As such, it will emphasise user-centred design and frequent feedback from the presenters. The presenter interface would need to
Part of the project would require researching and testing different enabling technologies for implementing the system, particularly CORBA and Java. The project will emphasise user-centred design, so that the system can be used by a large number of people with a shallow learning curve. As such, a prototype/UI mockup will be first created and shown to the presenters. Short iterations will then follow, adding additional features during each iteration. At each stage, presenter feedback will be obtained. Given the small number of basic features required by the system, and the proposer's interactions with URY, it is feasible to obtain frequent and rapid feedback on the interaction design from presenters.
Details of current progress can be found at URY.
Readings
J. Preece et al, Interaction Design, John Wiley, 2002.
M. Campione et al, The Java Tutorial, Third Edition, AWL, 2002.
Any reasonable book on CORBA, e.g., Vinoski's Advanced CORBA Programming in C++.
This project involves a study into the architecture used in a multiplayer online game (a game played by many players simultaneously, typically involving a persistent state world). This project will involve taking an existing network game - specifically, ACM or Xpilot - and will extend it to deal with issues of scalability, particularly: how to add large numbers of players at run-time. The extension will be based on the publish/subscribe design pattern (which effectively allows both players and servers to enroll as the system executes) and will specifically consider two issues of performance: server load balancing and client-side prediction. Experiments will be carried out to establish whether the publish/subscribe pattern provides a scalable architecture for ACM/Xpilot-like games.
The deliverables will be an architecture and prototype of a publish/subscribe-like ACM/Xpilot game, as well as experimental data demonstrating the effect of the architecture on critical gaming attributes like lag time, latency, and frame rate. Resources are available from both York student systems and from University of Plymouth.
Reading