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]
Description:
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.
Reading:
- Internet resources
- Academic papers and books
GL/02: Programming a multi-legged walker and a brick sorter in SCADE [CS3, CSMath3, CS4]
Description:
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.
Note:
This project is analoguous to project GL1, but
considers the tool SCADE instead of Esterel Studio as well as
different example robots in Lego.
Reading:
- Internet resources
- Academic papers and books
GL/03: 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/04: Modelling and analysing feature interactions in SMART [CS3, CSMath3, CS4]
Description:
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.
Reading:
GL/05: 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:
- 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
GL/06: A PVS library for multi-valued decision diagrams [CS3, CSMath3, 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 and reminds of a
functional programming language.
Reading:
- 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
GL/07: Translating Message Sequence Charts into temporal logic formulas [CS3, CSMath3, CS4]
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/08: Implementing a logical semantics for Statecharts via SAT solvers [CS3, CSMath3, CSMath4]
Description:
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.
Reading:
- 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
GL/09: CSA Concurrency Workbench [CS3, CSMath3]
Description:
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.
Reading:
GL/10: Visual Programming Tool [CS3, CSMath3, CS4]
Description:
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).
Reading:
- C. Szyperski. Component software. ACM Press/Addison-Wesley, 1998
- J.A. Sharp. Data flow computing, Ellis Horwood/John Wiley, 1985
- M. Burnett, A. Goldberg, T. Lewis. Visual object-oriented programming. Manning, 1995
- W.A. Najjar, E.A. Lee and G.R. Gao. Advances in the dataflow computational model. Parallel Computing, 25:1907-1929, 1999
- The Ptolemy project
- Haskell: A purely functional language
- The Gnome Toolkit (GTK)
GL/11: Evaluation and comparison of popular tools for requirements management [MScIP]
Description:
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.
Reading:
© 2003
Gerald Luettgen
luettgen@cs.york.ac.uk