Embedded Code Integrity

With an estimated 60% of development time being spent on design, test and debugging, there is obviously a need for a reliable means of producing accurate code and verifying that it performs exactly to the specification of the application. State machines or statecharts represent a well-established and recommended technique for characterizing the behaviour of complex event-driven systems. Tool-assisted state machine design, such as IAR visualSTATE, provides designers with a reliable and intuitive way to design, simulate, generate, and test code, by using a visual representation of the logical "states" and "events" in the problem domain. By using a subset of the unified modelling language (UML), users can take advantage of previous familiarity with the notation, while beginners will find it easy to grasp.

FORMAL VERIFICATION
Verification based on formal methods offers the capability of finding dead ends, ambiguities and parts of the design that cannot be reached, and can be used to find unwanted scenarios defined by the user: all this is virtually impossible to do exhaustively without formal verification. Figure 1 shows graphically the way "reachability" can be verified: the forward mode explores the state space working from the initial states, while the backwards mode—as its name suggests—explores the state space from a given state trying to reach the initial state. The area marked in red is never reached because no transitions are enabled to join the two areas together.

The environment of an embedded system determines the stimuli it must react to and how it should react to them. A typical embedded system will contain devices such as sensors, actuators, buttons, and indicator displays. Inputs from sensors to the system are called events, and can result in state changes, as long the machine is in a state where it is prepared to react to the event. Each transition has an event associated with it, and a single event can be associated with several transitions that are all performed when the event takes place. A transition, or entry of a state, can invoke "actions" (C functions) that act on the environment, i.e. blink a LED, advance a stepper motor, update a display, etc. Signals are similar to events, but are broadcast internally within the state machine.
<%@ LANGUAGE="VBSCRIPT" %>
<% Randomize: ord=int(rnd*1000000000) %>


APPLICATION EXAMPLE— VEHICLE PASSENGER COMPARTMENT LIGHT
There are six stages involved in designing a visualSTATE model, and these are illustrated using the example of programming a passenger compartment light in a car:

1. Identify events, signals and actions Figure 2 shows the events, signals and actions related to the car light example. These are the occurrences that precipitate a move between states.

2. Identify states States can be identified from the requirement specification and knowledge about the problem domain. In the car light example, the states are as follows:
- The door can be open or Figure 1: Graphical representation of unreachable states. closed
- The door can be locked or unlocked
- The switch can be in any of the three positions (on, off or door-sensitive)
- The light can be on or off

3. Group by hierarchy This is achieved by examining which states have a dynamic behaviour of their own, and which states can only be active under certain conditions. For the purpose of the grouping in Figure 3, the model assumes that the door is neither open nor closed when it is locked, and only permits the option of opening the door when it is unlocked.

4. Group by concurrency Next it is necessary to examine which states can be active at the same time, and to group them accordingly, as shown in Figure 4. This demonstrates the fact that it has to be possible to open, close and lock the door in parallel with changing the switch and the switching of light.

5. Add transitions The next step is to identify which state changes must take place, and what actions must be executed when specific events occur.

6. Add synchronizations Finally one needs to identify the transitions that need to be protected by "guards," and if necessary introduce additional transitions. The transitions might need to send internal messages, or signals, to trigger other transitions that will generate the required actions.


IMPLEMENTATION
The IAR visualSTATE suite comprises several inter-related modules, all co-ordinated via the Navigator project management workspace. The visualSTATE Designer interface (Figure 5) features a number of userconfigurable windows: the main window shows one or more state machine diagrams. New elements (states, transitions, guards, etc.) can be added, modified or deleted using the icons in the vertical toolbar. The developer can examine the behaviour of the state machine model either by using the interactive simulator, by creating a prototype resembling the final application; and by performing dynamic formal verification. All the tools use the same state machine model created by visualSTATE Designer, which ensures that the model from which the target code is generated is identical to the one that has been tested.

TESTING
The interactive simulator allows the developer to execute a state machine model, and monitor its reaction to events, one transition at a time. This allows all the details of the state machine model to be tracked, including the current state, active events, guards, triggered actions, and signals. The simulator allows the developer to record one or more computations in a log file, which can be used either for documentation or as a script for repeat testing. visualSTATE Validator reports any differences found between current and previous simulations.

PROTOTYPING
Third party software from Altia, or GUI code written for the pc, can be used with visualSTATE to allow the creation of a customized simulation environment, for example a graphical model of the final product such as the mobile phone interface shown in Figure 6. The prototype allows the developer to experiment with the user interface before going into detailed—and costly—implementation and can be used later on for training and demonstration purposes.

DYNAMIC FORMAL VERIFICATION
It is not uncommon to have billions of state combinations in a real-life application—the so-called "state space explosion"—so it is unrealistic to check all of them by testing individually. Developers generally rely on a carefully selected set of up to a few thousand test inputs, even though there are many combinations of events and states that are not covered, which means the product can malfunction in use if the untested combinations occur. The visualSTATE dynamic formal verification function performs within a matter of seconds an exhaustive check of all the combinations of states, events and internal states of all machines in the model and identifies any unreachable states or dead ends.

CODE GENERATION
visualSTATE Coder transforms a state machine model into very compact executable ANSI-C compliant code for any target processor that is combined with an API (application programming interface) for interfacing with target-specific firmware. State machine models can be ported from one target to another. At the same time visualSTATE generates documentation that is fully synchronized with the target code running in the application, a facility that is of crucial importance not only during development, but also for maintenance that might take place some years after the initial development project.

CONCLUSION
The ability to simulate and exhaustively test an embedded application before producing hardware is crucial to optimizing both the reliability and the time to market of the final product. IAR visualSTATE provides an intuitive tool for testing every possible combination of states, events and internal states in a state machine model of a product. It also provides the means of generating compact and accurate code direct from the state machine model, along with documentation that will always ref lect the latest update to the model.

Reference

1. “Statecharts: A Visual Formalism for Complex Systems�, David Harel, Science of Computer Programming 8 (1987) 231 - 274

2. “Practical Verification of Embedded Software�, J. Staunstrup et al., Computer, May 2000, IEEE