2003/04 Project Proposals by Dr. Gerald Luettgen

Projects with LEGO Mindstorms

Lego(r) Mindstorms(tm) is a popular environment for constructing and studying simple reactive systems. Reactive systems are characterised by their ongoing interaction with their physical environment via sensors and actuators; real-world examples include cruise controllers for cars and industrial production cells. The Lego Mindstorms kit essentially consists of a Lego computer brick to which one may connect up to three actuators (e.g., motors) and three sensors (e.g., touch sensors, light sensors and/or revolution sensors). The following two projects involve programming of Lego robots with the help of state-of-the-art industrial tools for reactive-systems design.

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 four 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 Component-based Programming

The twin dreams of visual programming and of a component-driven software industry will have a marked effect on the way software will be produced in the new century. Within the domain of real-time applications in measurement and control, new academic and commercial tools are being developed which support the assembly of systems from components purely via signal flow graphs. A technology which honours this programming style while still allowing utmost flexibility in terms of which components are executed at a given time, is currently being investigated by the proposer of the following two projects.

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.

Information for the Projects' Moderators

The Lego Mindstorms' projects involve the purchase of two sets of the basic Lego Mindstorms kit together with some elementary expansion kits at a total cost of about GBP400. It is planned that these kits will be used in future projects and teaching within the Department as well. In addition, the tools Esterel Studio and SCADE, both from Esterel Technologies, need to be obtained and installed. Esterel Technologies offers a free academic license for both tools in the context of their University Partnership Programme. Previous experience has shown that both joining this programme and installing the software is straightforward.

GL/01: Programming a Lego punchcard reader and a plotter in Esterel Studio [CS3, CSMath3, CS4]


Esterel Studio(tm) is a commercial tool marketed by Esterel Technologies for designing and programming embedded systems. Its SyncCharts editor provides a Statecharts-like graphical notation which allows one to specify what a system should be doing under certain conditions and how the system should respond to input signals and requests. The models may then be simulated, formally checked for desired and undesired behaviour, and used for automatic code generation. Esterel Studio has its roots in the academic language Esterel, which is a textual synchronous language aimed at programming control-intensive reactive systems. The academic Esterel compiler can easily be interfaced to Esterel Studio and has also been adapted to facilitate programming for the Lego Mindstorms platform. This compiler generates C code which may then be cross-compiled to the LegOS operating system running on the Lego Mindstorms brick.

The aim of the project is to construct a simple punchcard reader and a plotter with Lego Mindstorms and to program these robots by developing their software in Esterel Studio. This requires an extensive familiarisation with the particular application domain of reactive systems, the Lego Mindstorms kit and the Esterel Studio tool. It should also be investigated whether the indirection via the academic Esterel compiler described above can be avoided, i.e., whether the C-code generator inside Esterel Studio can directly be used for compiling programs to Lego Mindstorms. Thus some knowledge in C programming would be beneficial. The project must be well documented on dedicated web pages which will be used as a resource in future teaching activities within the Department.


GL/02: Programming a multi-legged walker and a brick sorter in SCADE [CS3, CSMath3, CS4]


SCADE(tm) is a commercial tool for safety-critical systems development 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 code generation. SCADE has its roots in the academic language Lustre, which is a textual synchronous language aimed at programming data-flow-intensive reactive systems. The academic Lustre compiler can easily be interfaced to SCADE and has also been adapted to facilitate programming for the Lego Mindstorms platform. This compiler generates C code which may then be cross-compiled to the LegOS operating system running on the Lego Mindstorms brick.

The aim of the project is to construct a multi-legged walker (i.e., a spider-like creature) and a brick sorter with Lego Mindstorms and to program them by designing their software in SCADE. This requires an extensive familiarisation with the particular application domain of reactive systems, the Lego Mindstorms kit and the SCADE tool. It should also be investigated whether the indirection via the academic Lustre compiler described above can be avoided, i.e., whether the C-code generator inside SCADE can directly be used for compiling programs to Lego Mindstorms. Thus some knowledge in C programming would be beneficial. The project must be well documented on dedicated web pages which will be used as a resource in future teaching activities within the Department.


This project is analoguous to project GL1, but considers the tool SCADE instead of Esterel Studio as well as different example robots in Lego.


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


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.


GL/04: Modelling and analysing feature interactions in SMART [CS3, CSMath3, CS4]


Today's intelligent telephone network is distinguished by its huge number of features, which telephone companies offer their customers on top of the plain standard telephone service. Examples for such features are call forwarding, where calls made to some number A may be automatically forwarded to another number B, and call screening, where some recipient C may block calls received from number A. Many of these features work well in isolation but cause trouble when used together. In our example, consider what happens if A calls B, B has call forwarding to C engaged, but C employs call screening and wants to block all calls from A but not those from B. It is easy to imagine that dependencies between features may become quite complicated and difficult to detect.

This problem of feature interaction is of great concern to telephone companies which thus became very interested in automated verification technologies, especially in model checking. Model checking requires one to model the underlying protocols used for features in telephone services as finite-state machines (e.g., using safe Petri nets) and to represent the service specifications as formulas in a temporal logic. It then allows one to automatically check whether the state machines satisfy the formulas. Unfortunately, although this technique is in principle what is desired by developers of telephone services, it does not scale to today's complexity of these services, which is due to the very large number of states in the state machine models.

Recently, novel algorithms for efficiently model-checking asynchronous systems with huge numbers of states have been introduced into SMART. The aim of this project is to apply this new technology to the problem of feature interaction in the context of a case study. This requires the project student (1) to conduct a thorough literature review on features in phone services, (2) to model some suitable subsets of these features in the Petri net dialect supported by SMART, (3) to encode appropriate service specifications in SMART's simple temporal logic and (4) to systematically analyse SMART's performance when model checking the developed service models.


GL/05: A SMART benchmark for asynchronous systems verification [CS3, CSMath3]


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.


GL/06: A PVS library for multi-valued decision diagrams [CS3, CSMath3, CSMath4]


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 and reminds of a functional programming language.


GL/07: Translating Message Sequence Charts into temporal logic formulas [CS3, CSMath3, CS4]


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.


GL/08: Implementing a logical semantics for Statecharts via SAT solvers [CS3, CSMath3, CSMath4]


Statecharts is a popular visual design notation for embedded systems which extends state machines by 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 of the model-theoretic Statecharts semantics 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 abovementioned 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.


GL/09: CSA Concurrency Workbench [CS3, CSMath3]


The Calculus of Communicating Systems (CCS) is a well-studied process algebra that allows the modelling of concurrent and distributed systems. CSA extends CCS with notions of clocks and maximal progress, which proves very convenient for modelling many hardware and software systems, including distributed schedulers for component-based signal-processing applications. Clocks in CSA allow one to express qualitative timing behaviour, i.e., how behaviour is ordered across time by synchronisations. Maximal progress formalises the viewpoint on time where communications within a system happen considerably faster than external events.

For CCS and some previous extensions, there exist tools that allow the modelling, simulation, manipulation and verification of concurrent systems, such as the Concurrency Workbench for the New Century (CWB-NC). The aim of this project is to accommodate the treatment of CSA in the CWB-NC, via the CWB-NC's Process Algebra Compiler (PAC). This work must necessarily be carried out in the functional programming language SML-NJ, a flavour of ML. The resulting tool will be a concurrency workbench in its own right.


GL/10: Visual Programming Tool [CS3, CSMath3, CS4]


The aim of this project is to develop a tool for the graphical assembly of programs in a hierarchical signal-flow-graph-style. A library of blocks containing components for signal-processing, which will be made available, should be represented. The tool should allow instances of these components to be placed in a design and connected up into a graph. As well as composing systems in this fashion, the design of modules as signal graphs should be allowed in order that these can be saved within a user library and reused as component instances in other systems.

Execution of these `programs' will be via a scheduler that will also be made available. In order to allow this integration, it is highly desirable that the tool be written in the functional programming language Haskell and that the internal representation of systems, as they are constructed and persisted, should be achieved via a provided data structure which already encapsulates the link to external components, written in other programming languages. It is suggested that the user interface be written by the Haskell interface to the Gnome Toolkit (GTK).


GL/11: Evaluation and comparison of popular tools for requirements management [MScIP]


The aim of this project is to conduct two case studies in specifying and managing software-systems requirements using at least one of two popular commercial tools, Rational(r) RequisitePro(r) and Telelogic DOORSrequireIT(tm), in order to compare the tools as well as to demonstrate their practicality.

The two case studies will involve different--style software systems, a business software system, such as a web-based membership database system of a sports club, and an engineering software system, such as an automatic locking system for cars. Suitable candidates of software systems and their functional and nonfunctional requirements shall be identified in the first phase of the project and will be taken from the rich literature on requirements engineering. Their requirements shall than be mapped into the considered commercial tools for requirements management.

As requirements normally change during the software development process, several change scenarios concerning the example systems shall be envisioned and exercised using both tools, in order to judge the ease with which requirements can be traced and managed within the commercial tools. This should lead to an example-led comparison of the strength and weaknesses of requirements-engineering tools, as well as the differences between requirements engineering for business-oriented and engineering-oriented software systems.

The case studies shall be well illustrated and documented such that they may be easily integrated into the teaching of introductory modules to requirements engineering within the Department.


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