Advances in embedded computing technologies have made society extremely dependent on embedded software used in automobiles, mobile phones, home electronics, and for many other applications. Consequently, the reliability of embedded software is crucial for many aspects of daily life. In the past, the development of embedded software has been implementation-centric; however, due to an increase in size and complexity of software and a reduction in development time, it is difficult to produce reliable software using conventional techniques. Therefore, the quality of embedded software becomes a matter of concern. To solve this problem, various software engineering techniques, such as analysis/design methods and reuse technologies, have been introduced. Product line engineering is one of the most advanced software practices based on these results [2].
It is expected that scientific approaches such as formal verification will be introduced in addition to these engineering approaches. Unlike conventional testing in which we run a finite number of test cases, this technique, if successful, exhaustively verifies the properties of the target system. Formal verification has a long history and has been reported to be successful in many cases. However, most of these cases belong to the hardware domain or critical software fields, such as military and avionics. Further, the application of formal verification to embedded software development for civilian industries such as automobiles, communications, and consumer electronics has thus far been limited. One of the main reasons is that the techniques require a large amount of time and human resources. With this background, we examine the application of formal verification techniques in the context of software product line development [6, 7]. This is because a majority of embedded systems in civilian industries are developed as product lines, and we can expect to reduce the cost by reusing the verification schemes. The reuse of test schemes has already been proposed [9]; in this article, we extend it to formal verification.
Lightweight Software Design Verification
In this approach, we apply model checking techniques to design verification. A model checking technique is a formal verification technique in which we describe the target system as a finite state model and provide some logical properties, and model checkers automatically check whether the given properties are valid [10]. Since embedded software must appropriately react to every possible combination and sequence of events occurring in its environment, it is necessary to exhaustively check its behavior. Model checking techniques are suitable for this type of verification [4, 8]. Further, we focus on design verification instead of code verification; this is because many bugs are embedded in the design phase and it is important to verify the design before coding.
A conventional method for applying these techniques to design verification is described as follows. First, convert the target design into a finite state model (target model); further, express the environment of the target as a finite state model (environment model). The environment model is configured to send possible event sequences and combinations to the target model. Then, apply the apply model checker to the target and environment models along with the properties (expressed as temporal logic formulas) in order to verify the validity of these properties. A set comprising the target and environment models and properties is termed a verification model. It should be noted that the environment is what surrounds the verification target; it may be actual physical environment, sensors, or other software modules.
A majority of embedded systems in civilian industries are developed as product lines; we can expect to reduce the cost by reusing the verification schemes.
We use UML to define the target and environment models. Each class included in these models has state model that defines its behavior. Here, we call classes in environment model as actor class. Figure 1 shows an example (car audio system). The target model consists of two classes—EV-hdlr (event handler) and CD-Ctrl (CD controller), while the environment model consists of three actor classes—two BUTTONs (push buttons) and CD (CD drive). In this example, we verify the following property: if button 1 is released, the CD drive will be switched off.
In our design verification, we utilize test scenarios because this is a typical method for defining verification items [7]. Here, a test scenario for a target system is defined as a triple (I, {S}, F), where {S} denotes a set of event sequences that will convert T of the initial state I into the final state F. We develop the environment model that sends event sequences included in {S} to T and verify the following property P: if T of I receives any event sequence included in {S}, it eventually falls into F. In the conventional test, it is difficult to check every possible sequence included in {S} because the number of possible sequences is generally large. However, in model checking, we can verify properties, if successful, against every possible event sequence. For example, in Figure 1, the state model for each button generates an arbitrary length of event sequences defined as the state machine, and the order in which the target model receives events from the two buttons can be shuffled.
One of the problems in the application of model checking techniques is state explosion (for a large model, the state space is too large to handle). Though we have verified relatively small-size software (3K to 15K lines of C code), we have encountered the problem. In this case, we use conventional techniques such as dividing the system into subsystems or abstracting the design manually.
Verification by Reuse
Here, we examine the application of the design verification described previously in the context of product line development. In the application engineering phase, we derive a design for a product by selecting the required features. Although this process is systematic, the correctness of the developed design cannot be guaranteed because we could not verify every combination of features in the domain engineering phase, and the design should be verified each time it is derived. If we spend a considerable amount of time on the verification, the delivery of the product will be delayed. Our objective is to accelerate this process. For this purpose, we examine the reuse of the verification scheme throughout product line development. This concept is based on the following observation. Although each product may exhibit different behaviors, we can expect that a family of products will exhibit similar behaviors. This implies the verification models for each product are also similar; hence, we can reuse the verification model throughout product line development.
In order to reuse the verification model in product line development, we define variation points in the model, variants for each variation point, and links between the features and variants. In the product line field, a technique using UML has been proposed that denotes variation points and variants by attaching the certain stereotypes (such as “optional” and “alternative”) to the classes and associations [3]. We can employ similar techniques to define the variation points in the environment model, since we define the environment model by using UML. Each product may have different actors and each actor may have different types of events and generate different patterns of event sequences; therefore, the environment model for each product may be different. We examine the commonality and variability among these environment models and define a reusable model by utilizing UML techniques. Figure 2 shows an example of a reusable verification model. In this case, the target model includes an alternative class and an optional class that may or may not be used depending on the product. Similarly, the environment model has two optional actors. For an alternative class, multiple variant classes that exhibit different behaviors are defined.
We have developed a support tool for the previously described design verification (see Figure 3). The system is developed on an Eclipse platform (see www.eclipse.org) and uses a SPIN model checker [4]. Using Modeler, users can define UML models (target and environment models), feature models for describing the features of a product line [5], and verification items and links among them. A verification item is a set of properties and other necessary information, as described later. By specifying a product, Link Manager derives verification models and necessary verification items. Translator translates the model into the input language of SPIN (Promela), and SPIN verifies the properties defined in the verification item. Since the initial state, initial value of the attribute, and translation rule (for example, how to handle events not defined in the state model) may be different for each verification item, it contains this information along with SPIN options. When the verification fails, SPIN shows a counterexample (an execution trace that violates the given property). Since the counterexample is based on Promela, Viewer shows it in the form of a UML sequence diagram.
One of the important objectives of product line development is the timely delivery of products. In order to achieve this goal, we must reduce the time taken for both the derivation and verification of products.
We have evaluated our approach based on actual test scenarios provided by a company. In this evaluation, we can verify approximately 70% of the necessary test scenarios. We cannot test the other 30% because they include aspects such as real-time constraints that cannot be handled effectively by the model checker. Further, we can reduce about 10% of the test scenarios by combining scenarios that have the same values of I and F. With the exception of I, about 30% of the test scenarios are the same, and we can reuse the same state model for these test scenarios because our tool can change I for each verification item. We have verified the reusability of the test scenarios by selecting three products from the product family and have found that 70% of the test scenarios can be shared or reused. By considering that the target model can be systematically verified using a reusable verification model, the result seems positive.
Verification for Reuse
We have introduced an application of formal verification to the application engineering phase. Here, we briefly explain the application of formal verification to the domain engineering phase. In this phase, we develop core assets that can be used by many products. Therefore, these assets must be verified for every possible situation in which they will be used. Here, situation implies not only the usage of the components such as parameter values and calling sequences but also assumptions under which the components are used, such as relative priority of components and usage of shared resources. In an actual situation, it is unreasonable to verify the assets in every possible situation because a large number of situations must be considered [1, 10]. Hence, we must develop a strategy to reduce the number of situations.
For testing a core asset, a technique is proposed in which we concretely assume potential products that will use the core asset and test it from these products [9]. We apply the technique in our formal verification. In our scheme, a core asset is represented as a target model, and environment models are defined to represent the usages of the core asset from potential products. In Figure 2, let us assume that we want to verify EV-hdlr-A as a core asset. The environment model for EV-hdlr-A is developed as follows. First, as same as testing, the potential usages (products) are determined. In our approach, this corresponds to addition of constraints on models, such as selection of variants. Second, classes that directly interact with EV-hdlr-A are identified. Third, instance structure is defined by deciding concrete number of multiplicity on associations. Finally, classes that indirectly influence the behavior of EV-hdlr-A are examined; such classes share resources with EV-hdlr-A. We believe the final step is important because it is difficult to verify the design simply by considering direct interactions [10].
Conclusion
One of the important objectives of product line development is the timely delivery of products. In order to achieve this goal, we must reduce the time taken for both the derivation and verification of products. We have proposed a systematic method to verify products based on formal verification techniques. Though formal verification is one of promising techniques to develop reliable embedded software, it is expensive to apply. We will refine our verification approach in order to make formal verification more widely usable for embedded software development.
Join the Discussion (0)
Become a Member or Sign In to Post a Comment