2006/07 Student Project Proposals by Dr. Gerald Luettgen

List of Proposed Projects

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: Implementing a simple theorem prover for program verification [MEng, SWE]

Description:

Model checking is a modern technology for automatically checking at compile time whether a given system satisfies desirable properties at run-time. Most model checking techniques rely on theorem proving in order to refine abstract models. For example, the Berkeley Lazy Abstraction Software Verification Tool (BLAST) utilises Simplify as proof engine, which has been developed at Compaq Research and whose source code is available. Simplify uses the Nelson-Oppen method for combining decision procedures for several important theories, and also employs a matcher to reason about quantifiers. Instead of conventional matching in a term DAG, Simplify matches up to equivalence in an E-graph, which detects many relevant pattern instances that would be missed by the conventional approach. Unfortunately, neither Simplify nor the Modula compiler needed to build it are under active maintenance.

The aim of this project is to implement a Simplify-compliant proof engine in ANSI C, which can be used for future research into model checking at York. The student working on this task shall focus on providing a maintainable, reliable and mainly platform-independent implementation of Simplify.

The ideal project student will have a good understanding of discrete structures in Computer Science and a good knowledge of the C programming language.

Reading:

GL/02: Integrating new model checking techniques into the SPIN model checker [MEng, SWE]

Description:

Model checking is a modern technology for automatically checking at compile time whether a given system satisfies desirable properties at run-time. SPIN is a popular open-source model checker that can be used in the formal verification of distributed software systems. In order to increase SPIN's ability of model checking large scale systems, evaluating new algorithms for state space generation is necessary.

This project aims at integrating the Saturation algorithm, an efficient method for symbolic state space generation, into SPIN. Up to now, this algorithm has only been used in the SMART model checker, where it has proved that it can cope with extremely large state spaces. In order to use the Saturation algorithm for SPIN models, one could either interface SMART with the specification language Promela or re-implement the so-called "Pan" generator of SPIN. Having conducted one of these activities, the performance of the Saturation algorithm shall be compared to the one traditionally employed in SPIN.

The ideal project student will have extensive programming skills in C and C++ as well as an interest in evaluating algorithms.

Reading:

GL/03: Handling aliasing in the Chase verification tool [MEng]

Description:

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.

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/04: Inferring 'modifies' specifications in the Chase verification tool [MEng, SWE]

Description:

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 quality of the Chase's output 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/05: 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. 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/06: A PVS library for multi-valued decision diagrams [MEng, 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/07: Modelling reactive systems in the Promela modelling language [MEng, 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 project involves manually translating existing system models (provided in various modelling languages, particularly Petri nets) in Promela.

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

Reading:

GL/08: Implementing a logical semantics for Statecharts via SAT solvers [MEng, 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 build 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/09: Devising design patterns for Statecharts [MEng, SWE]

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. The work shall be evaluated by re-designing some of these examples using the devised design patterns.

This project is to be jointly supervised with Dr. Richard Paige.

Reading:

GL/10: Design and development of a web-based 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.

Action Tracker shall in first instance be a system usable in the Department, rather than a general-purpose action tracking system. Information on the Department's workflows can be obtained from various existing documents and by interviewing key members of the administrative and academic staff in the Department.

Reading:

© 2006 Gerald Luettgen