Predictable Software Systems

This week I've been very entertained with a new module of the Engineering Doctorate I'm doing at the University of York. Prior to the module lessons, I had my first talk in a seminar meeting for some of the Enterprise Systems Research Group's colleagues. Although I think that there were no more 10 people in the room, I found it as an ideal opportunity to start to show some mates the stuff I'm working on, and more interestingly, to detect any interest and spark new possibilities of collaboration around the topic.

Nevertheless, I spent the most of the time of this week in assisting to a taught module called Predictable Software Systems which was organized in some lectures and practical sessions. Along the module we were learning about different techniques, formalisms, and tools which are being used when building critical-systems, for which traditional software solutions, its design and verification doesn't usually guarantee predictability and hence are not suitable for this kind of systems. Whilst it is very common having bugs in many software we have in our hands, the nature of these systems can't afford having any kind of bug since millions of euros and, even worse, human lives are involved. One could think many examples, like the software running in aeroplanes, vehicles or those machines controlling the drug doses of any hospital patient. However, there are other industry areas such as hardware manufacturers, in which after launching a large amount of microprocessors out, they can't afford having a "buggy" component in their chips, just due to the fact that they can't simply apply a patch to fix them, unfortunately.

During this course, we firstly saw some formal methods and notations mainly based in some mathematical principles in order to be able to describe in an abstract but formal way a complete model of the entities, its properties and the operations operating on them representing our system. By the means of the Z notation, which uses the principles of propositional and predicate logic as well as the set theory, one could describe a user of micro-blogging system and the required properties applying to them as follows:

Once you have your system properly described, you could use other techniques like Programming By Contract so that every constraint you have defined is ported in the form of invariants of your entities and as a pre or post condition of the operations which manipulate them. In this case, we were using JML to define these constraints in a form of annotated pseudo-language (using java comments). Although it's not a very user-friendly experience, it is quite amazing when you have an interesting test cases infrastructure generated from the specification of these class invariants and method pre/post conditions.

Finally we were also using model checking and quantitative model checking techniques in order to ensure the important safety, reachability and liveness properties of finite-state concurrent systems. Based on linear-time temporal logic and computation tree logic, the former focuses again in providing formulas to express different properties of your system which, with the aim of open source tools like NuSMV, allows you verify if a set of desired properties apply to your modeled system. More importantly, if those are not satisfied it provides you the counter-example which can help you to realize about what is wrong with the system: are the properties bad formulated/incomplete? Is the model of your system incorrect?. On the other hand, based on probabilistic computation tree logic and tools like PRISM, quantitative model checking allows you similarly build and verify systems in which the probability plays a key role along the behaviour of the system.

Although these techniques and tools are more focused on the idea of finite state-machines based systems, its powerful is undoubted and one could find that it's highly convenient when dealing for example with embedded software.

To conclude this blog entry, I didn't want to forget to mention one of the papers I could read this week:

• Variations on the Visitor Pattern. 

Although it's dated from 1996, it's a again a new illustrative paper in which it's explained some of the problems we may find when applying the pattern, how some variations of the original pattern try to overcome them, when the creativity may appear to try to solve other non-related issues and enforces my beliefs about:

•    Why I need to go beyond the essence of the pattern.
•    Why MDE needs to come up to the rescue.