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