The content of this page is likely to change, and no questions regarding these proposals will be answered until the beginning of week 7 in spring term.

2005/06 Student Project Proposals by Dr Gerald Luettgen

Projects in Reactive-Systems Design and Programming

Reactive systems are characterised by their ongoing interaction with their physical environment via sensors and actuators; real-world examples include flight control systems for aircraft and industrial production cells. The following projects deal with the design and programming of such systems using state-of-the-art tools and languages.


Projects with the Verification Tool Chase

The verification tool Chase is an extension of the ESC/Java tool developed at Compaq Research. Its goal is to efficiently find common programming errors in Java source code, such as indexing an array out of bounds or dereferencing null pointers, at compile time. The user can guide the search for such errors by putting appropriate annotations in the source code, including so-called modifies clauses that provide information on which variables or objects a method modifies; such information cannot always be calculated accurately at compile time. The following projects aim at making the underlying verification technology more powerful.


Projects with the Verification Tool SMART

SMART stands for Stochastic Model checking Analyzer for Reliability and Timing and is a software package that integrates various high-level logical and stochastic modelling formalisms (e.g., Petri nets) in a single modelling study. Recently, SMART has been extended by novel algorithms for state-space generation, reachability analysis, and symbolic model checking. The following projects deal with various aspects of this extension.


Projects in Statecharts and Message Sequence Charts

The following projects involve the development and construction of tools related to the supervisor's recent research activities in the semantics of engineering design languages, in particular Statecharts and Message Sequence Charts.


Projects in Information Technologies

The technology of the following projects centres around the engineering of web-accessible databases.


Student-defined Projects (using Lego Mindstorms)

Student-defined projects are very welcome, particularly in the wider area of formal methods, such as projects involving the semantics of engineering design languages or the formal verification of state machine models. Especially fun projects centred around the Lego(r) Mindstorms(tm) Robotics System will attract the lecturer's interest.

GL/01: Application of modern design tools for the analysis of mode confusion in aircraft cockpits [CS4, MScSWE]

Description:

The confusion of operating modes is a persisting problem in today's complex systems, for instance in the "glass cockpits" found in modern aircraft. A number of approaches have been suggested by academics to investigate mode confusion potential, which is the cause of many automation surprises, during the design of such systems. Model-checking is one such approach, which has recently been integrated in industrial tool for designing and programming avionics software, such as Esterel Studio(tm) and SCADE(tm).

The aim of this project is to investigate how state-of-the-art design tools, in particular Esterel Studio and SCADE, can be used for the analysis of models of dependable systems for their mode confusion potential. The project involves developing models that capture the relevant system aspects that are required for such an analysis. These models can for example elaborate on existing models of parts of aircraft cockpits, such as mode logics of flight-guidance systems, together with suitable user models. Of particular interest here is how the "features" of the human user of the system can be considered appropriately and what facettes of mode confusion problems may be analysed using the model-checking facilities of Esterel Studio and SCADE. Consequently, this project will contribute in assessing industrial design environments for analysing mode confusion potential.

Reading:

GL/02: Handling aliasing in Chase [CS4]

Description:

The Chase tool is limited in that it does not handle aliasing. Hence, when two references point to the same object and then a field of such an object is changed via one reference, the tool does not recognise that the other reference also points to a changed object.

The aim of this project is to extend the Chase tool by checking modifies clauses -- user-provided information on which variables or objects a method modifies -- in the presence of aliasing. This requires an intensive study of the literature regarding algorithms for detecting aliasing of variables and an investigation on how they relate to the problem of checking modifies clauses.

The ideal project student will have expertise in the Java programming language and an interest in modern compiler technology. It is helpful to have a good grounding into the semantics of programming languages, such as from the third-year option Semantics of Programming Languages.

Reading:

GL/03: Inferring 'modifies' specifications in Chase [CS4, MScSWE]

Description:

The quality of the output of the analysis algorithm implemented in Chase heavily relies on modifies clauses provided by the user, which help to keep track of the references that are changed within a Java program's method. As Chase is a tool which analyses Java code at compile time, there will be references for which it cannot decide for certain whether they are modified in a program.

The aim of this project is to increase the degree of automation provided by the tool. One way to do this is trying to infer, rather than to check, modifies clauses so that the analysis algorithm needs to rely less on user-provided information. The other is to calculate an approximate complement to the set of definitely modified references, i.e., the set of definitely unmodified references.

The ideal project student will have expertise in the Java programming language and an interest in modern compiler technology. It is helpful to have a good grounding into the semantics of programming languages, such as from the third-year option Semantics of Programming Languages.

Reading:

GL/04: Evaluating caching strategies for symbolic model checking [CS3, CSMath3]

Description:

Model Checking is a popular technology for verifying whether a finite-state machine satisfies a temporal-logic property, which is employed by modern tools for embedded-systems design. Symbolic model-checking algorithms work on compact encodings of state spaces using decision diagrams as primary data structure, and have found huge success in verifying synchronous hardware circuits. Recent research co-conducted by the project proposer has advanced these algorithms for dealing with embedded software systems, such as computer protocols, which exhibit asynchronous rather than synchronous behaviour. Core to the run-time efficiency of these algorithms is the use of various caches in order to avoid computing the same task more than once. Given the limited space that is available for storing caches on any computer, a key design decision of a caching strategy (such as "least recently used") is when cache entries shall be overwritten if memory becomes scarce.

The aim of this project is to implement and evaluate various caching strategies for symbolic model-checking algorithms. The implementation needs to be carried out in the programming language C++ and integrated in the verification tool SMART, of which the proposer's symbolic model-checking algorithm is a part. The performance evaluation shall be conducted experimentally by running the SMART model checker for each choice of caching strategy on a benchmark of asynchronous system models; such a benchmark already exists but may need extension. The performance measurements shall be carefully analysed and used to optimise the chosen caching strategies, e.g., by tuning the strategies' parameters.

The ideal project student will have an interest in evaluating algorithms for automated verification, programming in the language C++, and conducting experimental research.

Reading:

GL/05: A PVS library for multi-valued decision diagrams [CS4, CSMath4]

Description:

Multi-valued decision diagrams (MDDs) serve as a data structure for compactly representing functions whose arguments and results are taken from some finite initial set I of the integers. The case of I={0,1} where one speaks of binary decision diagrams (BDDs) representing boolean functions, has been particularly well studied. BDDs have been successfully employed in various formal verification techniques, such as symbolic model checking. Recently, MDDs have been given attention in the context of generating and storing state spaces of event-based asynchronous systems, such as those specified by Petri nets, as they permit a simple efficient encoding of sets of state vectors. The underlying algorithms are however non-trivial and need to be formally verified, e.g., by using the mechanised prover PVS. PVS is a verification system consisting of a specification language integrated with support tools and a theorem prover. It captures the state-of-the-art in mechanised formal methods and is extensively used in academic and industrial applications.

The aim of this project is to built a PVS library that supports (1) formal reasoning about state spaces, (2) the encoding of state spaces in MDDs, and (3) operations on MDDs, in particular a sophisticated operation for computing the MDD representing the union of MDD-encoded state spaces. This also requires the devising of simple proof strategies (tactics), and the ideal project student should have good skills in mathematical formalisation and proof. It should additionally be noted that the specification language of PVS is essentially a higher-order logic that reminds in style somewhat of a functional programming language.

Reading:

GL/06: Modelling reactive systems in Promela [CS4, CSMath4]

Description:

Current research efforts in York aim at comparing the efficiency of new-generation model checkers, which are automated tools for verifying reactive systems such as communications protocols and distributed algorithms. This comparison will be conducted by means of a benchmark which comprises a set of reactive system models frequently studied in the literature.

The aim of this project is to help populating the benchmark by modelling some of these well-studied systems in Promela (PROcess MEta LAnguage). Promela is a C-inspired modelling language that is incorporated in the widely recognised Spin model checker. The task involves understanding system models provided in various modelling languages, including the SMART dialect of Petri nets, and transferring them into Promela.

The ideal project student shall have an interest in formal modelling and modelling languages.

Reading:

GL/07: A Java Tool for MDD Visualisation [CS4, CSMath4, MScSWE]

Description:

State space generation plays a key role in automated tools for verifying reactive systems, such as communications protocols and distributed algorithms. A Multi Value Decision Diagram (MDD) is a directed acyclic graph that is used by a novel state space generation algorithm called Saturation to compactly store the state space of a model. For the purposes of analysis of the algorithm it is useful to be able to visualise how Saturation constructs the MDD. A basic tool has already been defined in Java/AWT that provides a graphical way to do this.

The aim of this project is to further advance this MDD visualisation tool in order to make it more useful to research on automated verification currently conducted in York. Examples for further improvement include the provision of facilities for "zooming in" on different parts of MDDs and for visualing information on the formation of threads.

The project breaks down into a number of clearly defined tasks as follows: (1) To understand the state space generation algorithm Saturation and the visualisation tool. (2) To gather the requirements on what extensions can be made to the tool that will be useful to the research group. (3) To come up with ideas and suggestions as to how the information can best be presented and the extension made. (4) To implement these extensions in Java/AWT (Abstract Window Toolkit).

The project will provide valuable experience in working with customers and other developers to define software requirements and in designing and implementing user interfaces and object-oriented systems. Java programming experience is required, while experience on using the AWT can be gained.

Reading:

GL/08: Translating Message Sequence Charts into temporal logic formulas [CS4, CSMath4]

Description:

Message Sequence Charts (MSCs) is a well-known formalism for specifying and visualising the communication behaviour of distributed processes and cooperating objects. It has been successfully applied in the telecommunications industry, and a variant of MSCs, known as interaction diagrams, is included in the UML. In the context of embedded systems design, it has recently been investigated how the MSC formalism can be extended to specify temporal system properties, including safety properties (e.g., "can a protocol deadlock?") and liveness properties (e.g., "is a transmitted message eventually received?").

The aim of this project is first to combine several of the ideas presented in the literature for extending MSCs into a single visual specification formalism which is suited to simple linear-time temporal properties over abstract system events. Then a tool shall be built that supports the unified graphical syntax and is able to translate a visually specified temporal property into a temporal logic formula which can be fed into existing design and verification tools (such as the Concurrency Workbench of the New Century). This MSC editor and translator can be written in a language of the project student's choice, e.g., in JAVA using the Swing library.

Reading:

GL/09: Implementing a logical semantics for Statecharts via SAT solvers [CS4, CSMath4]

Description:

Statecharts is a popular visual design notation for embedded systems which extends state machines with the concepts of concurrency, hierarchy, and priority. It is increasingly used by engineers in the automotive and avionics industry for developing embedded-systems software. One shortcoming of the operational semantics for Harel's original Statecharts variant is its lack of support for component-based design, validation and code generation. Recent research has suggested a new model-theoretic semantics supporting composability. This semantics structurally reads Statecharts as propositional formulas that are interpreted in a simple fragment of intuitionistic logic. Distinguished models of these formulas then correspond to executable steps within the Statechart under consideration. A straightforward but practically inefficient algorithm for computing such models, based on the data structure of binary decision diagrams (BDDs), has been developed and implemented using the C programming language.

The aim of this project is to pursue a different implementation strategy based on SAT solvers instead of BDDs. SAT solvers check whether a given propositional formula is satisfiable and implement sophisticated heuristics for doing so efficiently. Several SAT packages, written in C, are available in the public domain and need to be evaluated within this project. It also needs to be investigated how exactly the above mentioned intuitionistic models shall be encoded as propositional formulas in classical logic. Various approaches should be identified, implemented and evaluated regarding their performance. In doing so, the project student can built on techniques and C code developed and used in the original BDD-based implementation. However, good basic knowledge of the C language is required.

Reading:

GL/10: Devising design patterns for Statecharts [CS4, MScSWE]

Description:

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 identify and document design patterns for Statecharts, i.e., semantics-preserving transformations between Statecharts diagrams. This would enable one to reason about and simplify Statecharts designs, and is similar to the motivation for using patterns in object-oriented design which has proved increasingly popular in recent years.

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. For the purpose of this project, a subset of Stateflow is augmented with a provision to specify contracts such as in Spark Ada, in order to express conditions that should hold when entering and exiting states as well as to specify state invariants. This results in a very expressive design language with an enormous potential for identifying design patterns. One type of design pattern emerges, for example, when contracts are used to constrain the interaction between concurrent states, which may well be equivalently expressed via event broadcasting.

The design patterns shall be identified by studying various examples of systems designed in Stateflow(r) and implemented in Spark Ada, which will be provided by the HiSE Research Group in the Department. This project is to be jointly supervised with Dr. Richard Paige.

Reading:

GL/11: A Wiki Benchmark [CS3]

Description:

Benchmarks are popular for measuring and comparing the performance of software tools. Researchers in the Department have recently compiled a new benchmark for comparing model checkers for event-based software, i.e., automated tools for reasoning about the behaviour of, e.g., communications protocols and distributed algorithms. In its current form, the benchmark is a suite of examples, each of which comprises of a brief description, a list of properties, and references to the literature where this example has been studied.

The aim of this project is to develop a customised database for storing the benchmark, which can be accessed via the web. This web-based database shall be collaborative, i.e., allow (registered) users to edit the contents of the benchmark and add more examples. Of course, the database shall also support typical functionality, such as searching the benchmark or restricting the view of the benchmark to those examples satisfying a particular property. A recommendation, but not a directive, for implementing the database is to consider wiki software, such as used for the collaborative encyclopedia Wikipedia.

The ideal project student should have good skills in basic database and web technologies, e.g., XML, PHP, and SQL.

Reading:

GL/12: Action Tracker [MScIP]

Description:

The administration within University Departments involves many committees which discuss various topics and agree on lines of actions. Each of these actions typically delegates some task to a person, who either carries out the task and reports back to the committee, or passes on the task to some better qualified colleague. It is notoriously difficult to formally track actions in order to monitor their progress and satisfy auditors.

The aim of this project is to capture the requirements for and built a prototype of a web-based software tool, Action Tracker, that supports the management of actions. This involves learning about and practising the software-engineering activity of Requirements Engineering, in which a system's purpose is captured, its stakeholders are identified, and the stakeholders' needs are documented, modelled and analysed. Part of this activity involves producing prototypes, for which basic skills of database and web technologies are required here.

Reading:

© 2005 Gerald Luettgen
Send email!  luettgen@cs.york.ac.uk