System Specification

Neal Harman and Monika Seisenberger

This is a course on specification - that is, on writing down precisely what a system is supposed to do, without (hopefully) having to know (or assume) how it works. In the next chapter, we will see some examples of the difficulties of specification, and (again hopefully) show why we need to use an unambiguous notation (derived, ultimately, from mathemtics). There are many such notations available to us - but at Swansea we have a strong interest in Algebraic concepts (as you may already know from other modules). In a 'spiritual' sense (though not a technical one), this module follows on from Modelling Computer Systems, in that it is also about modelling, and it is also about formal methods - applying mathematical techniques to software and hardware. Essentially, the course will cover the following topics.

Some Motivation. We will have a quick look at (a) why we need to specify systems precisely; (b) what problems can arise; and (c) what (ideally) we can do about it.
Algebra and Equations. We will quickly revise the basics of algebra, and show how we can attach meaning to signatures by axiomatization (writing down equations, essentially).
Term Rewriting. Once we have represented algebras using equations, we need some way of implementing them. This is so we can 'run', and 'bring to life', our specifications. (Actually, we do not need to do this at all - and some people feel very strongly that we should not. However, we (or at least I) do not agree with them.
Maude. The software we will use to write examples (and to do the coursework) is called Maude. Maude is available for Linux and a few other platforms (including Windows but only an Alpha version - so You Have Been Warned) and is freely-available. You can download it from a local mirror for Linux and FreeBSD. Over the course of the module, we will introduce Maude - starting obviously at a basic level and progressively looking at more advanced aspects. We will not however do more than touch the surface of Maude's advanced capabilities.
Maude Examples. Throughout the module we will see a range of examples - mainly simple data types and simple hardware components. Most of these will be in Maude, but in the early part of the module we will use a more abstract 'Maude-like' syntax.
Using Maude to represent microprocessors. The coursework for this module involves writing a Maude representation of a simple microprocessor. We will see some more examples of microprocessors, that will hopefully be helpful for the coursework.
The web pages. In case you're not reading this online the URL is http://www-compsci.swan.ac.uk/~csneal/SystemSpec/. Note that printed copies of the notes will be distributed in lectures - it is cheaper and more convenient for everyone to collect and use these. However, in addition, notes will be available in HTML and PDF form from this URL. Note that: (a) this means you can read online if you with; and (b) you can download and print notes yourself if necessary. The corollaries of this are: (a) do not under any circumstances ask for notes; and (b) print out the PDF files - not the HTML files

Reading

The bad and good news is that there is no text available to support this module. There is some documentation about Maude at its web site, but frankly for anyone who does not have much background on the underlying concepts, most of it is not that helpful. The exception to this it the Maude Primer, which is more readable and accessible. I have tried to make the material on Maude in the notes as comprehensive as possible. Similarly, there is not yet any texts on the main application of Maude in this module - specifying microprocessors.

Assessment

This module is assessed by a combination of a single coursework (20%) and a written examination (80%). There will be tree courseworks: the first two will be marked out of 25 and will each be worth 5% of the module overall; and the third will be marked out of 50 and be worth 10% of the module overall.

One More Thing

This is not a theory course but sometimes we will need to touch on some theoretical issues to explain what is going on. These will be kept as simple as possible - so simple in fact, that a theoretician would probably claim they are not strictly true. Well never mind. We will resort to the following quote.

'Accuracy is the enemy of pedagogy.' - Richard Feynman

In other words, trying to teach everything without simplifying and glossing over issues is just confusing.

Contents Next