Blogs
A quarterly blog on the subject of Model Driven Development.
If you feel like voicing your opinion in response to this blog entry or contributing to this discussion in any other way, please email me at blogs@critical-software.co.uk. José Reis (MDD Specialist)
Autumn 2010: In a period of instability can Formal Methods make things more predictable?
The recent economic downturn has increased pressures across industries to cut costs while maintaining (or even increasing) the quality of their software products. Surely therefore, it is down to major industry players and suppliers to identify ways of operating more efficiently without jeopardising quality. Despite the current economic turmoil, continual technical evolution is pushing systems to be more autonomous (witness the huge interest in UAVs) and thereby also increasing complexity. Moreover, existing complex systems are showing signs of weaknesses; particularly evident with the many recent car manufacturing recalls, numerous fatal helicopter crashes and possibly even the Deepwater Horizon oil spill.
So what can be done to make systems development more predictable while preventing overspend?
My experience as a software engineer tells me that standards such as ECSS-E40 (space systems) and DO-178B (avionics) make development more predictable, but only if project schedule is feasible, the team follow the processes without exception, and customer pressure is handled appropriately and without forcing extreme "tailoring decisions" onto the project team!
I do not think a dramatic change is necessary; we should go back to basics (i.e. sound engineering practices!) and revisit methods developed in the past which formalised key phases of the development process. For example, for the requirements engineering phase, much has been written about eliciting, analysing and recording requirements but time and again we witness projects failing due to incomplete, poorly specified and incorrect specifications. These issues will only be further magnified when under pressure and people resort to cutting corners.
My experience with the formal language Event-B, a new generation formal language, highlights that these tools force engineers to fundamentally change their behaviour by establishing a robust and proper groundwork at the early stages in development, thinking in more abstract terms about the system, refining the problem and maintaining a specification with explicit statements, replacing requirements that were previous missing or only ambiguously defined.
A model specified using a formal language like Event-B will define a set of events composed by pre-conditions and actions. Pre-conditions must be true before the execution of the event, actions specify the status of the system after the event occurs. Invariants capture system properties that must hold regardless of the system status/actions. Event-B uses set theory and 1st order logic for the specification of invariants and events, which automatically removes any ambiguity from the specification. Furthermore, through a set of theorems and provers, each invariant is formally verified ensuring that the events specified do not lead the system into an inconsistent state - the verification of an invariant against one event is called proof obligation.
I find the whole approach quite elegant but one thing that I always like to highlight is that engineers do not need to worry about generating test data, because the specification uses abstract types based on basic sets (e.g. natural numbers) defined in Set Theory. The properties and values of the set are formally defined meaning that it is possible for a model to be conclusively proved correct. If the model contains omissions or errors, for example where the engineer has missed a system property (functional or non-functional), this model prover will fail. This will force the engineering team to reanalyse the model and thereby identify the inconsistencies in the requirement's set.
This approach involves a higher degree of abstraction but from my experience significantly increases the level of confidence in the requirements and design phase and therefore also the end system (not to mention the potentially significant reduction in effort in not having to fix errors only identified late in the development process).
Another area where Formal Methods excels is in the refinement of system properties. Complex system features are typically developed in incremental steps, with each step refining the model either horizontally or vertically. The former allows the specification of new features and the latter expands the specification of an existing property. This is a fundamental concept in Formal Methods and facilitates the development of a system through the separation of concerns principle. The difficulty lies in ensuring that each step of the refinement does not introduce new errors; furthermore, properties specified at higher levels of abstraction must still hold in the refined model. With Event-B it is possible to verify that:
a) system properties are carried forward, hence properties specified at higher levels of abstraction hold in the refined model; b) new conditions are specified in the invariant ensuring that the properties introduced in the refined model are correct.
With Event-B and the tool that supports it - RODIN- it is possible to adhere seamlessly to a basic principle of engineering which is the separation between requirements and implementation. The language and the tool also allow verification of decisions earlier in the development cycle through controlled experiments.
I believe that the new generation of Formal Methods make system behaviour more predictable and also reduces the chance of overspending because the characteristics of the system are formalised and thoroughly tested early in the lifecycle.
With Formal Methods the quality is effectively in the process!
Summer 2010: Why Flexibility is Key to Model Driven Development
On many programmes a great deal of time is spent in the selection of tools for requirements management, system architecture design, document and code generation. One of the reasons why these choices are not straightforward is that the tools that vendors offer often have broad functionality and roadmaps that are not clearly defined. Why make an investment on a tool which could be off the market this time next year? What happens to models when a new release of the tool or modelling standard is issued? Can the tool interface with legacy models or models developed by other parties?
In reality, a tool is only one element to consider and while it is crucial to get the choice right, the overall process used to manage the model’s metadata, stakeholder views, compliance with standards and open interfaces is, in my opinion, more important.
Metadata is data pertaining to the model that captures its attributes and relationships and is usually stored in a tool’s database. In more recent developments it can also be used to customise a tool’s interface to match specific user needs.
Stakeholder views capture and present business requirements from the perspective of each functional department. For example, they may capture security restrictions that need to be in place to ensure that classified information is only visible to those users with the appropriate access rights. Information classification is obviously a major issue on defence programmes but in my experience tends to be considered too late in the process.
Standards and Open Interfaces is an area where current toolsets can excel and really differentiate themselves from the competition. Unfortunately, they often don’t. Standards have been created to facilitate interoperability across different industries, between industry sectors or simply within an organisation. Experience tells me that while standards don’t solve all modelling problems, they are fundamental in promoting the exchange of models (i.e. ideas!), allowing different organisations with perhaps different languages and processes to interoperate, and increasing the long term maintainability of the models. Standards also generally have a more defined roadmap that is less susceptible to sudden organisational or market changes and other commercial pressures.
On large programmes involving a broad supply chain, the interchange of models is always challenging with every organisation often using different modelling tools and methodologies. There are solutions to address this issue such as XMI (XML Metadata Interchange) which has been defined and promoted by the Open Management Group (OMG). However, it has limitations which are not rooted in the standard itself, but more due to its differing implementations by tool vendors. This is not only due to their reluctance to fully adopt the standard, but also the standard not meeting the diverse needs of all the tool vendors. A working group has been set up by OMG to improve the interoperability of XMI based tools. This working group is composed of key tool vendors and also some of the key users of these tools.
I think a more interesting solution is Eclipse’s M2M project which aims to create a generic framework for model transformation (and not just UML models). The framework enables the transformation of models between different modelling tools, the generation of UML models from syntactical models of the English language, and the interchange of models from quality control tools such as Bugzilla, Mantis and Excel. A tool like M2M that promotes open interfaces and open standards, clearly allows effective automatic translation and interchange of models. This is in fact a key principle of the Model Driven Development approach: flexibility.
So, design flexibility is key to the success of engineering programmes, especially those where a wide range of modelling and design tools are in use. Flexibility enables solution analysts, architects and developers to adapt to changing requirements in an efficient manner. It also enables the interchange of models between different stakeholders and organisations. The question of which tools to use is certainly a major consideration and, foremost among the selection criteria, it is crucial to obtain the ability to interchange models through the use of open interfaces and by adherence to international standards.
