*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.

- GL/01: Application of modern design tools for the analysis of mode confusion in aircraft cockpits
**[CS4, MScSWE]** - GL/02: Evaluating programming environments for
Lego Mindstorms
**[MScIP]** - GL/03: Communicating Reactive Systems with SCADE and Lego Mindstorms
**[CS4]**

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.

- GL/04: Translating SMART's Petri nets into Spin's Promela
**[CS3, CSMath3]** - GL/05: Evaluating caching strategies for symbolic model checking
**[CS3, CSMath3]** - GL/06: A SMART benchmark for asynchronous systems verification
**[CS3, CSMath3]** - GL/07: A PVS library for multi-valued decision diagrams
**[CS4, CSMath4]** - GL/08: MDD Visualisation in SMART
**[CS3, CS4, CSMath3, CSMath4]**

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*.

- GL/09: Translating Message Sequence Charts into temporal logic formulas
**[CS4, CSMath4]** - GL/10: Implementing a logical semantics for Statecharts via SAT solvers
**[CS4, CSMath4]** - GL/11: Devising Design Patterns for Statecharts
**[CS4, MScSWE]**

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 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.

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.

**Internet resources**

**Academic papers and books**- G.Luettgen and V. Carreno. Analyzing Mode Confusion via Model Checking. In Theoretical and Practical Aspects of SPIN Model Checking (SPIN '99), vol. 1680 of LNCS, pp. 120-135, Springer-Verlag, 1999
- K. Loer. Model-based Automated Analysis for Dependable Interactive Systems, YCST-2003-06, Department of Computer Science, University of York, UK, 2003
- A. Degani and A. Kirlik. Modes in Human-Automation Interaction: Initial Observations about a Modelling Approach. In Proceedings of the IEEE International Conference on Systems, Man and Cybernetics, pp. 3443-3450, IEEE Computer Society Press, 1995
- A. Degani, A. and M. Heyman. Formal Verification of Human-Automation Interaction, Human Factors Journal, 2002
- J. Rushby. Analyzing Cockpit Interfaces Using Formal Methods. ENTCS, vol. 43, Elsevier Science Publishers, 2001

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.

**Internet resources**

**Academic papers and books**- A. Vento, C. Beltran, and E. Taniuchi. A Quantitative Analysis of Robotic Languages. Journal of Computing in Small Colleges, 17(5):72-80, ACM Press, 2002
- M. Jadud, B. Chenoweth and J. Schleter. Little Languages for Little Robots. University of Canterbury, 2003
- B. Bagnal. Core Lego Mindstorms: Programming the RCX in Java. Prentice Hall, 2002

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.

- Lego Mindstorms
- SCADE
- Synchronous Languages and Lego Mindstorms
- LegOS: Open-Source Operating System for Lego Mindstorms

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.

- The SMART tool
- The Spin verifier
- Promela language reference
- T. Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541-579, 1989
- G.C. Gannod and S. Gupta. An automated tool for analyzing Petri nets using Spin. In proceedings of the 16th Automated Software Engineering Conference. IEEE, 2001
- B. Grahlmann and C. Pohl. Profiting from Spin in PEP. In Proceedings of the 4th Spin Workshop, 1998

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.

- The SMART tool
- G. Ciardo, G. Luettgen, and R. Siminiceanu. Saturation: An efficient iteration strategy for symbolic state-space generation. In Proceedings of TACAS 2001, LNCS 2031, pp. 328-342, Springer-Verlag, 2001
- K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993

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.

- The SMART tool
- G. Ciardo, G. Luettgen, and R. Siminiceanu. Saturation: An efficient iteration strategy for symbolic state-space generation. In Proceedings of TACAS 2001, LNCS 2031, pp. 328-342, Springer-Verlag, 2001
- ISCAS85 benchmark information
- ISCAS89 benchmark information
- T. Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541-579, 1989
- E.M. Clarke, O. Grumberg and D. Peled. Model checking. MIT Press, 1999

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.

- The PVS specification and verification system
- S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107-125, 1995
- T. Kam, T. Villa, R.K. Brayton, and A. Sangiovanni-Vincentelli. Multi-valued decision diagrams: Theory and applications. Multiple-Valued Logic, 4(1-2):9-62, 1998.
- G. Ciardo, G. Luettgen, and R. Siminiceanu. Saturation: An efficient iteration strategy for symbolic state-space generation. In Proceedings of TACAS 2001), LNCS 2031, pp. 328-342, Springer-Verlag, 2001
- K. McMillan. Symbolic model checking, Kluwer Academic Publishers, 1992

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.

- T. Kam, T. Villa, R.K. Brayton, and A. Sangiovanni-Vincentelli. Multi-valued decision diagrams: Theory and applications. Multiple-Valued Logic, 4(1-2):9-62, 1998.
- G. Ciardo, G. Luettgen, and R. Siminiceanu. Saturation: An efficient iteration strategy for symbolic state-space generation. In Proceedings of TACAS 2001), LNCS 2031, pp. 328-342, Springer-Verlag, 2001

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.

- W. Damm and D. Harel. LSCs: Breathing life into Message Sequence Charts. Formal Methods in System Design, 19:45-80, 2001
- B. Sengupta and R. Cleaveland. Triggered Message Sequence Charts. In Foundations of Software Engineering (SIGSOFT2002/FSE-10), ACM Press, 2002
- The Concurrency Workbench of the New Century

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.

- D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231-274, 1987
- A. Pnueli and M. Shalev. What is in a step: On the semantics of Statecharts. In Proceedings of Theoretical Aspects of Computer Software, LNCS 526, pp. 244-264, Springer-Verlag, 1991
- G. Luettgen and M. Mendler. Statecharts: From visual syntax to model-theoretic semantics. In Proceedings of the Workshop on Integrating Diagrammatic and Formal Specification Techniques, pp. 615-621, Austrian Computer Society, 2001
- T. Friedrich. How to implement Statecharts intuitionistically. Darwin research report, The University of Sheffield, 2002
- M.W. Moskewicz et al. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference, 2001
- SAT Live: A web site dedicated to SAT solvers

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.

- D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231-274, 1987
- The MathWorks. Stateflow User's Guide, 2003
- J. Barnes. High Integrity Software: The SPARK Approach. Addison Wesley, 2003
- E. Gamma, R. Helm, R. Johnson and J. Vlissides. Design Patterns. Addison Wesley, 1994
- S. Yacoub and H. Ammar. A Pattern Language of Statecharts. In Proceedings of Pattern Languages of Programs, 1998
- A. Isazadeh, G. MacEwen, and A. Malton. Behavioral Patterns for Software Requirement Engineering. In Proceedings of the 1995 Conference of the Centre for Advanced Studies on Collaborative Research, 1995

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.

- G. Kontoya and I. Sommerville. Requirements Engineering - Processes and Techniques. John Wiley, 1998
- S. Robertson and J. Robertson. Mastering the Requirements Process. Addison Wesley, 1999
- IBM Rational(r) RequisitePro(r)

© 2004 Gerald Luettgen

luettgen@cs.york.ac.uk