Editor’s Note: This article is based on material contributed by Guy Broadfoot to Embedded Systems Security , by David and and Mike Kleidermacher. He outlines how many features of model-driven development tools can also be used to create reliable software code for security- and safety-critical applications.
The majority of embedded software developers using traditional programming languages such as C and C++ make use of processes and techniques inherent in the language to improve reliability and reduce security flaws. However, another approach that has met with increasing success is the use of model-driven design (MDD).
The premise of MDD is to raise the abstraction of software development from the low-level imperative programming language that is fraught with opportunities to shoot one’s self in the foot to a higher-level modeling language that reduces the distance between design and implementation and by doing so reduces the flaws that lead to security and safety failures.
Modeling lends itself better to formal proofs of specifications and security policies than do traditional programming languages. Indeed, a side benefit of using some MDD platforms – especially the ones that support formal methods and automatic code generation – is the ability to make formal arguments regarding the correspondence between specification, design, and implementation, a core challenge in all formal approaches. The following will deal with MDD methods that lend themselves to formal analysis and therefore raise the assurance of quality, safety, and security.
In discussions about MDD and MDD platforms, the term verification tends to mean different things to different people. According to the IEEE, the term verification is given the following two definitions:
- The process of evaluating a system or component to determine whether the products of a given development phase satisfy the conditions imposed at the start of that phase.
- Formal proof of program correctness.
Most MDD vendors assume the first definition for the term, so throughout this article, we do the same. And in cases in which formal proof of program correctness is intended, we use the term formal verification.
This distinction is important: many MDD platforms offer facilities for verification, usually in the form of simulating execution on the development host before testing it on the target system. Test case generation features often support this activity. However, few MDD platforms offer facilities for formal verification to provide proof of correctness of a software design, and for those that do, this is an important distinguishing capability. Where these facilities exist, they offer great benefits, especially in multi-threaded and multicore designs.
We use the term ‘component’ to mean some physical hardware or software element of a system that satisfies one or more interfaces. We regard a system as comprising a collection of components. The term subsystem is a modeling concept defining the grouping of related components and/or other subsystems. It is a modeling abstraction to assist in the stepwise partitioning of large and complex systems. The physical realization of a subsystem is always by means of the components that it comprises.
Software development methodologies historically have tended to concentrate on tools that assist the software developer with system composition, integration, and especially testing. Various component-based technologies, such as CORBA and Microsoft’s COM, DCOM, and .NET have aimed at increasing software development productivity and quality by improving reuse through component abstraction in those domains where the technologies are applicable. Although increasingly sophisticated development tools such as optimizing compilers, source language debuggers, test generators, and test execution platforms have long been available to help software developers with implementation and testing, this conventional way of developing software is increasingly challenged by:
- the relentless pressure to reduce time to market and introduce new products in ever-shorter cycles, frequently leading to hardware and software being developed in parallel and final hardware platforms not available during most of the time the software is under development;
- the increasing complexity of embedded software, as essential product characteristics and end-user value are realized by software;
- the introduction of multi-core technologies, creating an environment in which software design and coding errors are more likely and conventional testing techniques are less effective;
- the continuing downward pressures on development costs;
- the trend toward distributed development sites, often in different time zones.
All these challenges must be met while achieving ever-higher quality levels to meet rising user expectations and regulatory pressures.
Conventional software development is labor intensive and bounded by human error. According to a recent Venture Development Corporation survey, software labor costs account for more than 50% of the total spent on embedded system development. Of this spending, according to Ebert and Jones, typical industry experience finds up to 40% spent on testing and rework. It is hard to think of another engineering domain that habitually spends 40% of its development budget identifying and removing defects that shouldn’t have been present in the first place.
Historically, organizations have attempted to address some of these issues by means of process improvement – that is, by introducing practices, procedures, and standards governing every aspect of specification, design, implementation, and testing. While some of this rigor is required in any high-assurance and high security development process, MDD can help to reduce that overhead, enabling higher assurance while improving developer efficiency.
Decreased efficiency due to development process overhead leads rapidly to diminishing return on investment and unsurprisingly to a loss of interest by senior management. Finally, beyond a relatively small threshold of complexity and size of a component, it is simply not feasible to try to achieve high-assurance security and safety with traditional software development techniques. MDD is a tool to address this scalability problem, enabling software developers to be more productive and deliver products more quickly and with significantly fewer defects.
What Is MDD?
MDD is based on the systematic use of models as primary artifacts throughout the software engineering life cycle. MDD aims to elevate functional models to a central role in the specification, design, integration, and validation of software.
In conventional software development, the definitive statement of software function is a mixture of informal functional requirements documents and the program source code. Establishing the correspondence between the two is often difficult. By raising the abstraction level in which specifications and designs are expressed, MDD aims to replace the specification and source code approach with a functional model expressed in an unambiguous, precise modeling language that can be understood by both the domain experts who determine what the resulting system does and the software developers who implement it. Additionally, code generated automatically from the model assures correspondence between specification and implementation.
MDD uses models to represent a system’s elements, the structural relationships between them, and their behavior and dynamic interactions. Modeling structural relationships supports design exploration and system partitioning; modeling behavior and interactions is essential for being able to verify designs by verifying models and for code generation. In practice, these last two points are the source of most of the benefits claimed for MDD.
But for many embedded software developers, code generation in particular seems to be difficult to accept. However, without code generation, much of the advantage of MDD is lost; in reality, deciding to adopt an MDD approach means accepting automatic code generation from models.
Models must be expressed in a modeling language with a formally defined grammar and semantics capable of expressing both static structure and dynamic behavior at an abstract level removed from the programming domain. We can divide these languages into two groups:
Vendor-specific language Languages developed and promoted by a specific vendor of an MDD platform such as MatLab and Simulink from MathWorks, Esterel from Esterel Technologies, and the ASD language (Figure 1 below) used in Verum Software Technologies’ ASD:Suite.
Standardized languages Languages that have been defined by industry groupings of interested users and MDD platform vendors. These are most commonly based on the Unified Modeling Language (UML).
Figure 1: Rather than coding, testing, and refining each component in separate steps, ASD Suite allows the developer to create an initial set of requirements. Based on this, the modeling tool captures both the external and internal behavior of the component using its two basic model types: interface models and design models. (Source: Vernum Software Technologies)
In practice, a significant difference between the vendor-specific modeling languages and the vendor-independent, UML-based languages is, of course, the degree of vendor lock-in that results from using them. The UML-based languages have the laudable goal of being vendor independent and, in principle, offering the possibility for models to be exchanged between platforms. Vendor-specific languages generally do not facilitate model exchange between platforms.
UML-based modeling languages are increasingly being adopted by MDD platforms (Figure 2 ) and other tools from several major vendors and are standardized.
Figure 2: The latest version of UML allows the developer to create 14 types of diagrams divided into two categories. For structural information it has seven diagram types, The second category is for general types of behavior and (Source: Wikipedia)
The quality of generated code and its suitability for a particular domain and use is an important consideration in choosing an MDD platform or even deciding to take the MDD route at all. We distinguish between two types of models, namely those that are executable and those that are both executable and formally verifiable.
The potential benefits of MDD
By raising the abstraction level in which specifications and designs are expressed and eliminating informal functional specifications, MDD has the potential to
- Eliminate specification and design errors early in the development cycle where they are cheapest and easiest to rectify
- Increase the degree of automation that can be applied to the development process by means of automatic code generation
- Facilitate parallel hardware/software design by enabling models to be verified by simulating execution behavior on development hosts before the target system is available
- Reduce the required testing effort by applying automated formal verification techniques to the functional models in combination with simulating execution behavior instead of relying solely on testing the implemented program code
Of course, eliminating errors is the primary impetus behind the discussion of MDD from
asecurity perspective. However, often the most valued benefits ofapplying MDD to embedded software development are significant reductionsin both cost and time to market needed to meet the required level offunctionality and quality.
The use of a suitable modelinglanguage contributes to reducing defects in the resulting product in twoways. First, it leads to increased precision and reduced ambiguity whenspecifying a system’s required behavior. Second, it reduces theabstraction gap between the concepts and language of domain expertsresponsible for specifying the system’s required behavior and thesoftware developers who must build it. The result is a functionalspecification that clearly and unambiguously specifies the requiredfunctional behavior and is understandable to all product stakeholders,domain experts, and developers alike.
Automation is increasedprimarily through automatic code generation, reducing manual programmingeffort and thus saving cost and preventing defect injection duringprogramming. Further automation is possible by using simulation andautomated test case generation, both increasing test coverage andreducing testing costs.
The application of formal verificationtechniques in industry to establish that the functional behavior of thecode generated from a model is as intended has been problematic. Thereare few MDD platforms that deliver fully automated verification forsoftware, and at the time of this writing, only Verum’s AnalyticalSoftware Design (ASD) platform can do this automatically, withoutspecialized knowledge and for large-scale embedded software systems withextensive concurrent behavior.
Where such tools are availableand applicable, automated verification carried out on functional modelscan reduce defects to unprecedented levels very quickly and providesignificant savings in time and cost; this directly addresses the 40% ofdevelopment effort currently spent testing and debugging software. Wereturn to this subject later in this section.
Inaddition to being rigorous and precise enough to allow for codegeneration and test case generation, executable models can be executedon the development system by means of simulation very early in thedevelopment life cycle.
Executable models provide the following significant benefits:
- Provide rapid and early feedback on requirements and specifications and serve to validate that the “right” product is being built. This is what most MDD vendors mean when they use the term verify
- Allow functional testing to take place on the development host without requiring access to software running on the eventual target machine. This is particularly important when the target hardware and the software are developed in parallel
Two well-known examples of such platforms areIBM’s Rational Rhapsody products and Mentor Graphics BridgePoint, bothof which use Unified Modeling Language (UML)-based modeling languages.These are discussed later in more detail.
Executable models arenot necessarily formally verifiable, and most MDD platforms do notprovide facilities for formally verifying the correctness of thesoftware being designed. These platforms, of course, ensure that themodels are well formed in the same sense that a compiler ensures aprogram conforms to the programming language syntax and grammar.
Formally verifiable executable models
Inaddition to being executable, some MDD platforms produce models thatare formally verifiable. This means that the MDD platform includes toolsfor automated formal verification based on mathematical principles.
Simulation,like testing, is a form of sampling. The sample is the set of testcases, or example scenarios, and the population is the set of allpossible execution paths through the software. In practice, for anythingother than very small developments, the sample size is statisticallyinsignificant in comparison to the population size. As E. W. Dijkstraonce famously observed, “program testing can be used to show thepresence of bugs, but never to show their absence!”
In contrast,formal verification uses mathematical techniques to compute and examineevery possible trace of behavior in a design to establish whether ornot a user-defined set of properties hold under every possiblecircumstance. If the property set is sufficiently large and complete inthe sense of covering all aspects in the software’s specification, thenformal verification establishes whether or not a design is correct withrespect to its specification. This is analogous to the formalverification methods available in some electronic design automation(EDA) platforms for verifying design intellectual property.
Inpractice, applying formal verification to software designs has proven tobe difficult. There are two major challenges to overcome:
Theability to derive the property sets from the specifications and specifythem in some formal notation, for example, temporal logic.
Derivinga complete set of properties to be verified such that all essentialaspects of the software’s specification are covered is a difficult andskilled job. Expressing the properties in a formal mathematical notationsuch as temporal logic also requires a skill set most embedded softwaredevelopers will not have and results in specifications that areinaccessible to most project stakeholders. Therefore, it is generallyimpossible to review them together with domain experts and establishthat they are a correct interpretation of the software’s specification.Even for the few MDD platforms that provide some form of formalverification, its use is challenging and not widespread.
Whyformal verification? The value of formal verification isthat it symbolically examines the entire state space of a softwaredesign to determine whether or not the specified properties hold underall possible inputs. In practice, this is rarely done; almost all usefulsoftware systems are far too complex to formally verify as a whole.Different MDD platforms use different approaches to these problems. SomeMDD platforms restrict the class of designs that can be verified; forexample, SCADE Suite (Esterel Technologies) deals with deterministic,synchronous designs.
ASD (Verum Software Technologies BV)provides a different approach called compositional verification wherebyan entire system is verified component by component in such a way thatthe proven properties still hold when the components are composed toform the complete system. This approach allows fully concurrent andasynchronous designs to be formally verified, both for compliance withthe specified properties and also to show the absence of typicalconcurrent and asynchronous design errors such as deadlocks, live locks,and race conditions. Simulation and testing are particularlyineffective at eliminating such errors. Formal verification should notbe seen as an alternative to verification based on simulation andtesting; rather, it is complementary.
Formal verification with well-designed tools brings a number of significant benefits:
- Enables early feedback on the correctness of component designs without requiring any test cases to be specified and before any code is generated. A component can be formally verified before any of the components it uses exist.
- Gives early feedback on defects before code is generated.
- Does not require simulation so no test sets need be prepared.
- Can completely replace or significantly reduce the need for component-level (unit) testing.
- Reduces integration and validation effort because software enters those phases with very low defect rates.
Thevalue of these benefits increases rapidly as the scale and complexityof the software grows. For example, earlier in this chapter, wediscussed the benefits of thorough code coverage testing. A byproduct offormal model verification is that complete multiple condition coverageis accomplished automatically.
MDD and code generation
Codegeneration has yet to gain widespread acceptance in the embeddedsoftware world. However, as mentioned earlier, much of the value of MDDis lost unless code is generated directly from the models. The MDDplatform vendor takes responsibility for ensuring that the generatedcode executes exactly as modeled. If code is handwritten using theverified models as a specification, or the generated code is modified,then all bets are off. Having verified the models, the developer willhave to re-verify the handwritten or modified code by conventionaltesting, nullifying the advantages of MDD.
Developers and managers must examine sample code generated from realistic models to be satisfied with at least the following:
Memory footprint Is the generated code small enough to fit in the target system? Is thememory footprint properly distributed between ROM and RAM memory (ifapplicable)? In the case of severely resource-constrained systems, theseissues can be showstoppers. Memory allocation model: Some targetenvironments, such as those compliant with the MISRA standards discussedearlier in this chapter, require all resources to be allocated beforeexecution starts and prohibit dynamic memory allocation; consequently,recursion and the language-specific equivalents of malloc() and free()are prohibited. Does the MDD platform provide a code generation optionfor complying with these language subsets (if applicable)?
Merging of handwritten code/legacy code Some code generators use proprietary calling conventions in thegenerated code. To what extent are these conventions compatible with thesystem’s legacy code? And if incompatible, what is the solution to makethe generated code compatible? If wrappers are needed, are thesecompletely handwritten (creating extra effort and maintenance as well aspotential fault injection risk), or does the code generator providesome assistance with this process?
Threading and runtime execution model Most MDD platforms have particular execution and threading models thatcannot be modified by the developer. For example, some platforms have astrict message-passing model to describe interactions between compo-nents and assume complete concurrency, with one thread being allocatedto each component. The platform supplies a means by which thesegenerated threads are mapped onto actual operating system threads atruntime. There are domains in which this threading model simply does notwork d for example, in the telecommunications domain where very largenumbers of component instances exist and there may simply beinsufficient system resources to support this number of threads.Designers need to understand the execution models of the candidate MDDplatforms and determine if they are sufficient for the targetenvironment.
Using MDD in safety- and security-critical systems
Theuse of MDD platforms in security-, safety-, security-, andmission-critical domains such as aerospace, military applications, railtransportation, and automotive is gradually increasing. The standardsgoverning software in such domains increasingly recognize that unittesting can be reduced if an MDD platform is used that providessufficient verification facilities on the model itself. The detailedrequirements governing the use of tools such as MDD platforms differ indetail from one standard to the next. Broadly speaking, the standardsfollow the same general approach:
1. The standards distinguishbetween the operational embedded software shipped as part of the productfrom the tools used to make that software. Certification usuallyapplies to the operational software, not to the tools. When tools arecovered in a certification, their requirements are quite different and,in general, not as rigorous.
2. The various standards for safety-and security-critical software – for example, IEC 61508, EN 50128, ISO26262, and ISO 15408 (Common Criteria) – often require the tool users toundertake an assessment of the tool to categorize it according towhether or not the tool itself can introduce errors into the operationalembedded software and to perform an assessment of the tool against theapplicable criteria in the standard to qualify the tool for safe andsecure use.
3. All users of software development tools mustqualify them to establish that they comply with the applicablestandards. The responsibility for this falls on the tool user and not onthe tool vendor. At the minimum, the user is required to ensure that ahazardous operation analysis is performed and a Safe Use Guide iswritten, specifying, for example, the checks that users must perform onthe resulting output (e.g., generated code) and tool features to beavoided because they are considered hazardous. Also, known errors in theversion of the platform being used must be identified together withpractices for avoiding them.
4. The user must establish that theMDD platform vendor’s software development practices and organizationcomply with the applicable standards. For example, EN 50182 requiresthat the MDD platform manufacturer have a named person external to thedevelopment team who is responsible for ensuring each release conformsto requirements and remains qualified. This person must report to thecompany’s most senior management and must have the authority to stop arelease. In some European Union jurisdictions, this person has a legalresponsibility.
When considering MDD platforms for use in a security-critical domain, an organization should consider at least the following:
- Is the MDD platform already in use within a domain governed by the same or similar standards and regulations as the organization’s and/or project’s domain?
- Has the platform vendor already conducted a qualification assessment supervised by a recognized external certification organization? Undertaking the assessment necessary to qualify an MDD platform for safe use is a time-consuming and expensive process; prequalification by the MDD vendor significantly reduces the costs of qualification to the user. Prequalification also provides evidence that the expensive and time-consuming qualification assessment is likely to be successful and shows vendor commitment to, and knowledge of, the development organization’s safety- or security-critical domain.
- What form of verification does the MDD platform offer? Especially in the safety- and security-critical areas, formal verification is particularly valuable.
- To what extent can the MDD platform’s verification be used to eliminate or reduce the amount of conventional unit testing? Can the MDD platform also simplify and reduce integration testing and result in savings with respect to end-to-end validation?
- Does the generated code comply with the applicable standards and regulations? For example, in the automotive domain, generated code must be compliant with the MISRA C standard.
- Does the platform assist in producing the embedded software documentation required by the applicable standards?
Becauseof its potential development cost and time efficiencies and ability toreduce the occurrence of software design flaws, model-driven design isan important software development technique worth considering forembedded systems that have stringent security, safety, and/orreliability requirements. Deciding on the most appropriate MDD platformfor a particular component and for the overall system requires thatengineers and managers understand the core technical advantages anddisadvantages of available solutions.
1. Object Management Group. OMG Uniﬁed Modeling Language (OMG UML), Infrastructure, Version 2.4.1; August 2011.
2. Mellor SJ, Balcer MJ. Executable UML, A Foundation for Model-Driven Architecture . Reading, MA, Addison-Wesley; 2002.
3. VDC Research. 2011 Embedded Engineer Survey; 2011.
4. Prowell SJ, Poore JH. Speciﬁcation, Foundations of Sequence-Based Software . IEEE Transactions on Software Engineering; May 2003:417e25.
5. Berry G, Gonthier G. The Esterel Synchronous Programming Language, Design, Semantics and Implementation . Science of Computer Programming; February 1992:87e152.
Guy Broadfoot isa founder and CTO of Verum Software Technologies. A veteran of thesoftware development industry, he combines deep academic expertise withsolid technical experience in developing products and turning aroundfailed software projects. Broadfoot has been designing and implementingsoftware projects since 1965, and in recent years has developed aspecialized interest in the application of formal methods. In 1986,Broadfoot founded Silverdata, a software company that developed productsfor marine navigation and hydrographic survey. He sold the productrights to private investors in 1998. He worked as a consultant toMountside Software Engineering from 1998, where he was responsible forestablishing a rigorous software project planning and financial controlsystem. Broadfoot graduated with distinction from the University ofOxford in 2001 with a master’s degree in software engineering.
This article is adapted from an excerpt from Embedded Systems Security ,by David and Mike Kleidermacher, and is used with permission fromNewnes, a division of Elsevier. Copyright 2012. All rights reserved.