The Synchronous Modeling Language for Embedded Systems (SMOLES) demonstrates how powerful modeling concepts like aspects, design time constraints, and generative constraints can be used to build better systems. These modeling concepts are used to alert the engineer to behavioral errors before verification and synthesis. Some errors are eliminated completely because SMOLES can automatically correct problems.

Introduction to SMOLES

SMOLES takes a new approach to synchronous reactive (SR) programming by requiring lefspecifications to be constructed in a layered fashion. Each layer adds more dynamics to the model until the full SR semantics is reached. The first layer in a SMOLES model is a set of stateless n-ary dataflow operators. The semantics of an operator is simple: Each operator waits for all of inputs to be available, at which time it consumes these inputs and instantaneously produces all of its outputs. These operators impose an important constraint on their use. There must never be a situation where an operator does not receive data on its inputs. The figure on the right shows a common set of dataflow operators for the digital systems. (Click for a larger view.)

In the next layer, dataflow operators are connected together to form dataflow graphs. A dataflow graph contains inputs (far left-hand side) that can be fed by an external environment. It also contains outputs (far right-hand side) that can be read by an external environment. If an environment interacts with the system, it must provide data on enough inputs so that every dataflow operator can be scheduled. This part of the system is equivalent to a homogenous SDF of rate 1. (Click for a larger view.)

The next layer of the specification is the mode layer. Each mode reconfigures the underlying dataflow graph by removing zero or more operators from the graph. Operators that are colored black are removed from the graph and operators that are colored white remain in the graph. Each mode has an entry condition that must be satisfied before it can be applied. Entry conditions are encoded by specifying the availability of input data and by placing requirements on the values of that data. The one bit adder only has two modes. In left mode, no data is given to the adder and no operator is schedule. In the right mode, all the input data is provided and every operator is scheduled. If the environment interacts with the adder by giving only some inputs, then no mode can be applied and a runtime error is generated. Mode entry conditions encode all the possible ways that an environment can interact with the graph. (Click for a larger view.)

Modes must obey the aforementioned scheduling constraints. For example, we might be able to make a new mode that permits the third input of the one-bit adder to be absent. The modeling environment can approximate the consequences of this change and alert the modeler to any violation that might have been created. (Click for a larger view.)

In fact, this change has caused a number of errors. The operators that cannot be scheduled properly are colored red, and a window appears that describes, in detail, the cause of each error. The analysis performed at modeling time is polynomial in the size of the dataflow graph, and is described full here. (Click for a larger view.)

SMOLES tries to automatically complete as much of the specification as possible. For example, the modes shown in the previous figures were generated while the dataflow graph was being constructed. Any changes to the dataflow graph are automatically reflected in the modes. The user only has to specify the number of modes, the entry conditions, and the presence/absence of operators. (Click for larger view.)

SMOLES models can be embedded into other SMOLES models with hierarchical composition. For example, we can use the 1-bit adder to build a 1-bit ALU capable of logical operations, addition, and subtraction. The adder component is the darker green rectangle in lower center with the '+' symbol in its center. (Click for a larger view.)

SMOLES submodels cannot be assert present/absent in a mode. The presences/absences of the outputs of a submodel depend on the presences/absences of the inputs applied to the submodel and the particular data values of those inputs. The SMOLES model-time analysis tool attempts to approximate the mode that a submodel will apply when it is embedded inside of a larger model. This information is displayed graphically by altering the color of the input and output ports. In the mode on the left, the 1-bit adder submodel will see all of its inputs present, and so it will apply a mode that will result in all of its outputs being present. An error is generated if no mode is found that can accept the environment in which the submodel is placed. (Click for larger view.)

SMOLES includes support for building large scale systems from libraries of existing primitives and models. The instantiation tool observes the current modeling context and displays information about the possible objects that can be added to the current view of the specification. The user just needs to double-click on the object that should be added, and the tool takes care of the rest. All the necessary modeling actions to properly add the object to the model are performed. (Click for a larger view.)

Advanced SMOLES Example

SMOLES also supports another level of specification that builds on top of modes. This next level, called a mode machine, restricts the set of possible modes based on the state of the system. This allows the user to encode state dependent interaction protocols with a simple automaton defined over modes. Additionally, the state information captured in the mode machine can be used for state-dependent analysis of component interactions. To illustrate this, consider the dataflow graph on the right. This system will encode the low,rising,high, and falling edges of a continuous clock into 4 events for the SR system. The system on the right places two bit numbers 00,01,10,11 on the output o1. These number encode the clock states.

Next, we define the modes for this system. There are five modes, four of which define the possible clock encodings; one of which defines the response to clock absence. (Click for a larger view.)

The clock encoder must encode the clock based on state. For example, if the last clock event was a rising edge, then the current clock event should be a high clock. We could capture this behavior using the previous output of the model to pick the current output (i.e. with a delay edge). However, for this example, we will use a mode machine to define this sequence. The mode machine is pictured on the right. It contains four states, and each state lists the legal modes for that particular state, and this is a subset of the possible responses of the system. If the system is in state s, and it applies mode m, then the system takes the transition that starts on mode m in state s. The example on the right allows an arbitrary number of clock absences per clock event. (Click for a larger view.)

Simulating SMOLES Models

SMOLES includes a simulator built directly into the GME modeling tool. Users may simulate partial specifications at any time during the design process. The model on the right is the datapath for a 32-bit ALU. The bottom graph implements the ALU opcode decoder logic and instantiates a 32-bit ripple-carry adder model. The actual adder is shown above. (Click for a larger view.)

The SMOLES simulator can be invoked directly from the modeling tool. Any SMOLES model can be loaded into the simulator by the dropdown list on the upper right-hand side. Simulation events are entered or loaded into the left-hand side of the simulation view. The tree on the right-hand side allows the user to go arbitrarily deep into the model hierarchy and select the signals that should be plotted. (Click for a larger view.)

The plot view is a scaleable view for observing the simulation results. It provides easy conversion between hexadecimal, octadecimal, binary, signed, unsigned, and ASCII views of data. The watch window can be used to capture more detailed information about the simulation, such as the state trajectory of a particular model, or the precise sequence of mode applications. (Click for a larger view.)

Ongoing Work And Publications

The primary development for SMOLES is on a formal analysis tool that leverages the unique abstraction layers. This tool will not be polynomial time, as causality is NP hard, but it will incorporate new analysis strategies for SR systems. The second major development branch is on code generators that can produce quality embedded code from SMOLES models. The target platforms are TinyOS for embedded platforms and BrickOS for experimental robotics. The main publications for SMOLES are:

Jackson E., Sztipanovits J.: Using Separation of Concerns for Embedded Systems Design, EMSOFT '05, pp. 25-34, Jersey City, New Jersey, September, 2005.