How to mathematically model formal systems and their environments. Unlike other engineering artifacts that are mathematically-modelled (bridge stresses, aircraft aerodynamics, etc.), many concepts in computer science are brand new, and a research challenge is simply how to mathematically model these concepts. Such concepts of course include modelling software and hardware and the environments in which they operate.
The fact that much of the work we're doing in the computer science area is brand appears curious, but if you think that in many cases the mere act of formalising something reveals how little is understood about the underlying theory. So while a new design of bridge can be built, it still uses well known and (importantly!) well understood underlying theories to verify and validate its design. Compare this to situations that arise in computer science, eg: the formalisation of policy structures for privacy, or the design of a space-based semantic web inspired, personal cloud and you quickly realise how little we know.
Privacy is an interesting issue, for example we have many groups proposing "engineering methods" for design of software systems but then failing on the actual theory.
Another case was the M3 project [1,2] and now there's a group trying to replicate that work without even attempting to learn the underlying theory...go figure...
But as the paper goes on to state, verification is truly difficult - the size, internal relationships and complexity and interactions within a computer system is immense and very fragile. The paper notes a comparison between aircraft and computer systems; while an aircraft as complex as the Airbus A380 has as many "parts" as a typical large software installation, it can survive partial failure and, more importantly, we knew how the thing would behave mechanically before it even was built.
The discussion, and source of the second quote I'll take, then moved to the ethics and morality of using formal methods as best practice:
Sadly this quote is too true, but is deeply troubling when you consider how much software is actually in production.
Another case was the M3 project [1,2] and now there's a group trying to replicate that work without even attempting to learn the underlying theory...go figure...
But as the paper goes on to state, verification is truly difficult - the size, internal relationships and complexity and interactions within a computer system is immense and very fragile. The paper notes a comparison between aircraft and computer systems; while an aircraft as complex as the Airbus A380 has as many "parts" as a typical large software installation, it can survive partial failure and, more importantly, we knew how the thing would behave mechanically before it even was built.
The discussion, and source of the second quote I'll take, then moved to the ethics and morality of using formal methods as best practice:
If formal methods is a best practice of software engineering, then an engineer who does not employ it is either negligent or incompetent. But formal methods is beyond the capability of typical software engineers (otherwise, why do we need formal methods experts and researchers?) or is too time-intensive to employ, so it cannot be considered to be a best practice today.
Sadly this quote is too true, but is deeply troubling when you consider how much software is actually in production.
I feel there is an irony here operating at many levels. After years of working with the UML - a language severely criticised by some for not being formal (and vice versa by others) and techniques such as MDA, we had developers using formal mechanisms without even really knowing it. Programming languages themselves are formal languages.
Then there's the irony of agile methods which apparently eschow any use for formality and modelling (so I am told and have experienced) - the irony here is that agile methods rely upon very strict communication between the developers, testing, validation, verification and common, consistent shared understanding of what is being developed.
Our own experiences of formal methods (Alloy, B-Method [4]) being used as a best practice have been documented [3] and the results we had very extremely encouraging. Though I do remember one episode where some "uber-architect" almost had a fit that we reduced his grand designs to a single page of relatively simple specification. I guess that simplicity was overrated - suffice to say, that particular design failed for many of the reasons given the the above paper.
Overall, the paper "When Formal Systems Kill..." is an extremely important discussion on software engineering failure to embrace and utilise the very techniques that it is based upon will some very damaging and frightening outcomes.
References:
References:
- [1] Oliver I, (2009) Information Spaces as a Basis for Personalising the Semantic Web. 11th International Conference on Enterprise Information Systems6 - 10, May 2009 Milan, Italy
- [2] Oliver Ian, Honkola Jukka, Ziegler Jurgen (2008). “Dynamic, Localized Space Based Semantic Webs”. WWW/Internet 2008. Proceedings, p.426, IADIS Press, ISBN 978-972-8924-68-3
- [3]Ian Oliver (2007). Experiences of Formal Methods in 'Conventional' Software and Systems Design. BCS FACS Christmas Workshop: Formal Methods in Industry, BCS London, UK, 17 December 2007.
- [4] Ian Oliver (2006). A Demonstration of Specifying and Synthesising Hardware using B and Bluespec. Forum on Design Languages FDL'06
No comments:
Post a Comment