My projects involve software engineering in some way, typically: object-oriented technology (e.g., UML, BON, Java, Eiffel, CASE tools, patterns, metamodelling), method integration, and formal methods. Inevitably they involve constructing some software (writing code or specifications), and may involve some maths.
Selected by E. Yau.
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. The last two additions 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)
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, 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). This project will involve two tasks:
This project is of reasonable difficulty. The first part will require a thorough understanding of Object-Z and BON (as well as an understanding of OO technology). The second part is more challenging, and will require considering alternative mechanisms for translation.
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.
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 are 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. This project will involve specifying and designing a GUI tool framework, in Java/Swing, for drawing graphical TCSP models. Part of the project will involve user interface design and evaluation: what mechanisms can best be used for selecting and placing the graphical TCSP components on the drawing canvas. The second part of the project will involve implementing the framework. The framework will use an internal representation of TCSP models, and should make it easy to generate code in a variety of output formats, particularly Latex, but also FDR. This internal representation is already used in a prototype text-based tool framework; it is documented in the first reference below. The student will likely have to correspond with Dr. Brooke when working with the existing internal representation.
Much of this project will involve becoming familiar with the various technologies (particularly Java/Swing, TCSP, and XML) and implementing the tool. Interesting research angles will arise from the user interface elements, from issues associated with redesign of the graphical language, and from how to best generate code.
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.
This project involves carrying out a case study in Agile Modelling, using a UML-based approach. Agile Modelling attempts to integrate the tenets of Extreme Programming and object-oriented modelling. A number of methods and techniques have been defined to carry this out.
Reading:
R. Paige and J. Ostroff. A Proposal for a Lightweight Rigorous UML-Based Development Method for Reliable Systems. In Proc. Workshop on Practical UML-Based Rigorous Development Methods 2001, GI Series 7, German Society, October 2001.
Literature on Agile Modelling: www.agilemodelling.com
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.
The BON-CASE tool is briefly described in project RFP/1. It is a full-featured CASE tool for drawing BON object-oriented models and for generating code from those models. In particular, the tool supports the generation of JML specifications. JML is a modelling language for Java. It is syntactically very similar to Java, but provides formal specification constructs for expressing pre/postconditions of methods, invariants of classes, and other properties. JML also provides a suite of tools, including a run-time assertion checker, and eventually theorem proving support.
This project will involve exploring the link between BON and JML by carrying out a CASE study in using BON and BON-CASE, generating JML, checking the JML using the JML tool suite, and revising the BON models appropriately. This process is documented informally in the technical report cited below. Effectively, the project will involve exploring and documenting how feedback provided by the JML tool suite can be introduced into the BON process, BON models, and the BON-CASE tool. It will involve: a precise description of the BON process that includes tie-ins to JML; an explanation of how the BON models were revised based on JML-derived feedback, and possibly modifications to BON-CASE to support easier introduction of changes to models.
The first step of the project will involve selecting a case study. Then, BON models will be constructed, JML generated, and a process developed. The main challenge with this project will be in documenting the process, describing rules for evolving the BON models, and explaining how to use JML-based feedback (which uses the JML syntax) in modifying BON models.
Reading:
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. Leavens et al. Preliminary Design of JML, Iowa State Technical Report, available from www.cs.iastate.edu/~leavens/JML.html
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.
The goal of this project is to analyze the requirements for, and implement, automated tool support for capturing software requirements and for generating and evaluating test plans and test cases from these requirements. Elements of the Unified Modelling Language (UML), will be assessed and supported by the automated tools for these purposes, and the ability to check test cases and test plans against requirements will be provided as well.
Requirements engineering is a critical element in the software development process. The larger and more complex the system is, the more likely that requirements that have been elicited are incomplete, vague and inconsistent. This makes it harder to implement an appropriate system, and also poses difficulties in later stages of development, e.g., testing. For example, inconsistent and incomplete requirements make it difficult to produce a complete and executable testing plan that can be used against the requirements, to identify flaws and misunderstandings.
Since the processes of requirement engineering and testing are tedious and error prone, it is useful to develop languages, tools, and processes to enhance the quality of these activities and the productivity of the staff involved. Automated tools for gathering requirements, and for generating test plans that can later be checked against requirements (particularly as the requirements change during development) can be viewed as essential for large-scale development.
Some useful languages, processes, and standards have been developed to assist in requirements engineering and test plan generation, like UML, RUP, IEEE830-1993, IEEE829-1998, etc. Further effort is required to develop new tools to support these standards and languages.
With the support and assistance of HISL, this project will focus on the development of tools to automate the process of capturing requirements and generating test plans that can be used to help validate and verify those requirements. This project will discuss how to bridge the gap between the requirements and testing, utilizing the benefits of OO models with automated tools. These issues are of importance to HISL, which focuses on automated technology for writing models and generating code from models.
In this project , we will explore the following issues:
Bibliography Jacobson, I., Booch, G., Rumbaugh, J., 1999, The unified software development process, Addison-Wesley.
Kaner, C., Falk, J., Nguyen, H., 1998, Testing computer software, 2nd edition, Van Nostrand Reinhold.
Kotonya, G., 1997, Requirements Engineering: process and techniques, John Wiley& Sons.
Sommerville, I., 2001, Software Engineering , 6th edition, Pearson Education LTD
Poston, R., 1996, Automating specification-based software testing, IEEE Computer Society Press.