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

2004/05 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 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.


Project in Requirements Engineering

The acceptance of any software system crucially depends on the degree to which it meets its intended purpose. Within the software engineering life cycle, requirements engineering is the activity in which a system's purpose is captured, its stakeholders are identified, and the stakeholders' needs are documented, modelled, analysed and communicated.


Student-defined Projects

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: Evaluating programming environments for Lego Mindstorms [MScIP]

Description:

Various efforts have recently been made to aid the teaching of reactive-systems programming within Computer Science degree courses. The Lego Mindstorms Robotics System has emerged as one of the most popular vehicles for demonstrating the principles of programming reactive systems. In particular, many dialects or subsets of existing programming languages, such as C, Java, Ada, Haskell and Forth, have been introduced, together with compilers, cross-compilers, and bytecode-machines for running such programs on the Lego Mindstorms platform.

The aim of the project is to systematically evaluate the available programming environments regarding their ability for programming complex Lego Mindstorms robots and regarding their suitability as a teaching aid for undergraduate and advanced masters courses in reactive-systems design and programming. This evaluation shall be based on an extensive study of the rich literature and online information on the various programming environments, and also on practical experiences by programming a few Lego robots using these environments.

Conducting this project requires an extensive familiarisation with several imperative, object-oriented and functional programming languages and with the Lego Mindstorms robotics system. The project must be well documented on dedicated web pages which will be used as a resource for future teaching activities in the Department.

Reading:

GL/03: Communicating Reactive Systems with SCADE and Lego Mindstorms [CS4]

Description:

SCADE(tm) is a commercial tool for safety-critical systems development, which is marketed by Esterel Technologies. Its graphical editor enables precise specifications on the basis of data flow and finite state machine block diagrams. The specified models may then be simulated, formally checked for desired and undesired behaviour, and used for C-code generation. A previous student project has built a facility to port SCADE-generated C-code for the Lego Mindstorms platform. This allow one to use SCADE for programming Lego robots running the LegOS operating system.

The aim of the project is to provide a mechanism for allowing multiple Mindstorms bricks, which are programmed in SCADE, to communicate with each other via their infrared ports. This involves the embedding of send and receive primitives into SCADE, and the modification of the above mentioned porting facility in order to translate these primitives into the basic communication mechanism supported by LegOS. Further, the conducted work shall be tested in practice by first building a quite complex production cell which relies on two communicating Mindstorms bricks for its control, and then programming the two bricks in SCADE. Ideas for designing a production cell may be taken from the Lego Mindstorms literature. The project must be well documented on dedicated web pages which will be used as a resource in future teaching activities within the Department.

The student should have interest in programming networked systems and working with operating systems, as well as a basic knowledge of the C programming language.

Reading:

GL/04: Translating SMART's Petri nets into Spin's Promela [CS3, CSMath3]

Description:

Spin is a widely distributed software package which supports the formal verification of asynchronous systems. To specify systems descriptions, it uses a C-inspired high-level language, called Promela (PROcess MEta LAnguage). Spin's validation and verification engine comprises a simulator, a state-space analyser and a model checker. However, the way state spaces are generated and stored in Spin is radically different to SMART. It would thus be interesting to compare the performance of Spin and SMART on those kinds of example systems, namely asynchronous systems, that are typically fed into these tools.

The aim of this project is to write a translator from SMART's dialect of Petri nets into Spin's Promela language, which is able to run under the Linux operating system. This can be done in any programming or scripting language of the project student's choice, but requires basic knowledge in topics of compiler construction, including parsing and code generation. The tool should then be applied to compare the performance of SMART and Spin on a few examples systems taken from the SMART literature.

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, 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/06: A SMART benchmark for asynchronous systems verification [CS3, CSMath3]

Description:

Model checking is a technique for deciding whether a given finite state machine satisfies a property specified in a temporal logic. Properties that can be checked for include safety properties (e.g., "can a protocol deadlock?") and liveness properties (e.g., "is a transmitted message eventually received?"). Symbolic model checkers work on compact encodings of state spaces and have been used to successfully verify synchronous systems with huge state spaces, such as hardware components. The performance of symbolic model checkers is often measured by applying them to the well-established ISCAS85 and ISCAS89 benchmarks that include synchronous systems taken from circuit design.

Recently, symbolic model-checking algorithms that are suitable for verifying asynchronous systems, such as communications protocols, have been developed and implemented in SMART. For evaluating the performance of these algorithms, the ISCAS benchmarks are not suitable. Indeed, the current literature does not provide any suitable benchmark for such asynchronous systems, with many papers just briefly studying one or two small example systems each. In this light, this project shall devise a new benchmark by systematically collecting a variety of asynchronous example systems proposed in the literature, together with interesting temporal properties to verify about them. This benchmark should be well-documented and be applied to evaluating the performance of SMART's model-checking algorithms. This involves representing all examples and their desired temporal properties in SMART's dialect of Petri nets and SMART's variant of the temporal logic CTL, respectively.

Reading:

GL/07: 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/08: MDD Visualisation in SMART [CS3, CS4, CSMath3, CSMath4]

Description:

Binary Decision Diagrams (BDDs) representing Boolean functions have been well studied and employed in formal verification techniques, in particular to represent the state spaces constructed by symbolic model-checking algorithms. Multi-valued Decision Diagrams (MDDs) are data structures employed to compactly represent integer functions. While less well studied than BDDs, MDDs are currently being exploited in order to represent state spaces for the verification of asynchronous digital systems. In particular, the model checker of the verification tool SMART relies on a special-purpose built MDD package that is written in C++.

The project goal is to create a way of visualising simple MDDs created in SMART, thus assisting the debugging of SMART's current and future model-checking algorithms. As MDDs are essentially directed acyclic graphs, the visualisation will be achieved by creating a back end providing graphical output of methods manipulating the arcs and nodes of a given MDD. Particular attention should be given to sensibly support zooming in and out of MDD areas that are currently being investigated by the SMART model checker. It should be noted that, since SMART is written in C++ and runs under the Linux operating system, the visualisation package should be implemented in C++ using some publicly available graph layout tool for Unix's Xwindows system.

The student is likely to have an interest in data structures and algorithms. Skills in OO-programming using C++ can be practised during the course of the project.

Reading:

GL/09: 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/10: 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/11: 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/12: Evaluating tool support for requirements engineering [MScIP]

Description:

The aim of this project is twofold. On the one hand, the project shall give a good survey of the tool support currently available for requirements engineering and management by consulting the large amount of academic and commercial literature available. On the other hand, an extensive case study, employing IBM's Rational(r) RequisitePro(r) as a representative commercial tool, shall be conducted in order to study which parts of the requirements engineering process are best and worst supported by today's tools, respectively.

Ideas for the case study may be taken from examples published in textbooks, which must however be elaborated upon, with a focus on considering non-functional requirements and exercising some envisioned change scenarios. The conduct of the case study shall be well illustrated and documented such that it may easily be integrated into the teaching of introductory modules to requirements engineering within the Department.

Reading:

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