Formal Specification Module Result – 96%

Z Notation PDF Render

The other module I was working on alongside “Topics in Privacy and Security” was “Formal Specification”.

In this module I used Z notation to formally specify a navigation system for Robot Vacuum Cleaners (A bit of a computer science obsession it seems). I then used the technique of promotion to allow for more than 1 robot vacuum cleaner to be in a room and observed some emergent interaction.

Comparison of the two movement algorithms I formally specified.

Comparison of the two movement algorithms I formally specified.

I really enjoyed this module, I like the challenge of working more on a mathematics level rather than a programming level — you have to work with different ‘data structures’ and work with different operators and structures of notation.

I would recommend for anyone to look in Z as it really makes you think about methods and functons in a different way. In terms of pre-conditions (what must be true for the function to start?), post-conditions (what must be true at the end of the function?) and invariants (what must always hold true?). It strikes me as a very good way to think about testing programs, even if you don’t formally specify them before producing them.

A visualisation of some of the emergent behaviour that happened with two robots -- one robot could effectively trap the other in the middle of the room.

A visualisation of some of the emergent behaviour that happened with two robots — one robot could effectively trap the other in the middle of the room.

Formal specification is probably a bit over the top for most software engineering projects, but if I were to ever work on a Planes autopilot system, or a system which moved the control rods in a Nuclear Power Station, I’d want to know formal specification had taken place. So it’s a useful skill to have learnt. It was also a nice refresh on discrete mathematics.

Danny

Advertisements

Tags: , ,

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s