To help build reliable software systems e ciently, the component based model-driven design approach is widely used, and lots of modeling languages have been designed. In this paper, we propose an integrated graphical development toolkit Tsmart-BIPEX 1 in support of building complex systems in the BIP modeling language, which features a rich semantics for composing sub-systems. First, we build a graphical interface for model construction and simulation, which is more intuitive than the command-line based toolchain. Furthermore, to enhance the original BIP veri cation tool RTD-Finder, we translate the graphical model to a labeled transition system for a thorough veri cation in verier VCS. Finally, we can generate executable C++ code directly from the graphical model. Tsmart-BIPEX has been successfully applied in the development of a real-world train network controller.
As embedded devices gain more and more computing power, the systems on
these platforms are expected to accomplish much more sophisticated tasks, which
brings new challenges to ensure the correctness of embedded softwares in the
traditional development approaches [
A promising way to alleviate the pain of detecting design defects in later
phases is the component-based model-driven design approach [
Among them, BIP features its semantics with the support of complex
interaction and dynamic priorities which can be further used to express complex
scheduling policies. It brings BIP strong expressiveness that cannot be matched
by other modeling languages, but also results in the limited veri cation support
of the tool RTD-Finder [
In this paper, we improve the convenience and veri cation e ciency of BIP by developing an integrated graphical design toolkit Tsmart-BIPEX. The overall structure of the toolkit is shown in Fig. 1. First, graphical model editor and simulator are implemented to assist the engineers according to the BIP syntax and semantics. Then, a translator is developed to translate the model to an equivalent labeled transition system, which can be directly veri ed by the VCS model checker. Finally, the original code generator is seamlessly integrated for C++ code generation. While the original supported compiler and engine are only provided on Linux with a command-line interface for textual model construction, Tsmart-BIPEX can be installed on Mac-OSX, Linux, and Windows.
Graphical
Models Graphical Model
Editor
Simulation Visualization Interactive Simulator
Safety Critical
Properties
Executable Code
on Devices Model Checker
Code Generator
Tsmart-BIPEX Platform
Related work is presented in Section 2. Some backgrounds on the computation model BIP are presented in Section 3. The implementation of TsmartBIPEX is introduced in Section 4. A case study of a real-world system design is presented in Section 5, and we conclude with Section 6. 2
During the last decades, lots of component based modeling languages such as
safety state machine, statechart, state ow, and BIP have been proposed
for the modeling of complex systems. Based on those modeling languages, many
design toolkits have been implemented, such as SCADE[
For example, SCADE is a development suite for building safety-critical embedded systems based on the synchronous modeling language safe state machine, and is widely used in safety-critical applications such as avionics and train control. Simulink State ow is a modeling and simulation platform based on the event-driven modeling language State ow, which highlights its tight integration with Matlab computing environment. It also provides numerous toolboxes such as Design Veri er and Polyspace for model construction and synthesized code analysis. Statemate developed by IBM is a working environment for the development of complex reactive software based on the reactive modeling language Statechart, where the software can be modeled and synthesized from a set of parallel and synchronized automata.
Except for those famous but expensive industrial tools, there are also many academical prototypes for system design such as Ptolemy, LabView, BIP and ForSys. They add new modeling and analysis features to the original industrial tools. For example, Ptolemy supports the design of heterogenous systems. BIP features its semantics with the support of complex interaction and dynamic priorities which can be further used to express complex scheduling policies, which cannot be matched by other modeling languages. In our work, we try to improve the convenience and veri cation e ciency of BIP by developing an integrated graphical design toolkit Tsmart-BIPEX. 3
In BIP, a system is speci ed in textual description with the composition of components and the interaction between components. There are two types of components, where the atomic components are a class of components which specify the behavior of independent sub-systems in labeled transition graphs, and the compound components schedule the communication between atomic components by de ning interactions connecting atomic components and priorities of the interactions. The textual model can be compiled, validated and synthesized with command-line support on Linux system.
User
press Press Interaction
pressed
Lamp Controller Time Sync synctime reset Interaction
Reset Interaction
Off true {time = 0;} press Low true sync{}time Wait time >=5 {} press time <5 {} press
High true {} press true {} reset
Rest synctime reset eexxppoorrtt ienPtPoortrt rseysnectt(i)me(int time)
Clock ienxtptoimrtee=Po0rt press() Fig. 2. A visual example of BIP model, including the compound and atomic component, interactions, ports, states, transitions with actions and guards, local variables.
We depict the main features by an example constructed in the graphical
interface of Tsmart-BIPEX in Fig. 2. This model represents how a user controls
the brightness of a lamp. The left part shows the top-level model with three
components: User, Lamp Controller, and Clock. Components communicate with
each other through interactions. The interaction between User and Lamp
Controller is Press Interaction. The interactions between Lamp Controller and Clock
are Time Sync Interaction and Reset Interaction. Interactions and components
are connected via ports (the black dots attached to components). When an
interaction is red, it triggers the computation of its connected components via
related ports. The right part shows the detailed behavior of the Lamp Controller
by an automaton. To obtain a full description for BIP, please refer to [
The overall structure of Tsmart-BIPEX is presented in Fig.1, and is
implemented on the Eclipse Rich Client Platform. The whole project contains 74,719
lines of Java codes and 2,358 lines of Clojure code, where 36,278 lines are
inherited from Tsmart-GalsBlock[
Graphical Model Editor. The graphical model editor is based on Eclipse
RCP and Eclipse Graphical Modeling Framework which implements the BIP
syntax de ned in [
Graphical Model Simulator. The graphical simulator is based on the execution semantics of BIP and provides interactive simulation of the constructed graphical model. In each step, an interaction or component is selected according to their state and execution priority, and the computation inside this candidate is executed. The graphical simulator helps users explore the system's behavior in a through way. Some basic functions are provided by the simulator, including model states traversal and execution traces recording, etc.
The simulation interface includes ve main views. (1) The simulation action
toolbar includes initialization, step-forward, step-backward and reset actions.
(2) The canvas view visualizes the simulated model in the same layout as the
editor, with the enabled components or interactions highlighted for choice. (3)
The candidate view displays all candidates (enabled components or interactions)
with the highest priority in the model's current state, whose inner computation
will be triggered if this element is selected. Users can manually select one
candidate to trigger by double-clicking the corresponding item or let the simulation
engine selects one randomly. (4) The data view lists values of local variables of
every component in the current state. (5) The model structure view shows the
hierarchical structure of the simulated model.
Model Checker. The model checker is VCS [
Code Generator. The code generator for BIP is integrated based on the
source-to-source transformation architecture introduced in [
We have applied Tsmart-BIPEX in the component-based model driven
development of a network interface controller to evaluate the e ectiveness of the
graphical toolkit. Network interface controller is an embedded device widely used
for the communication in several kinds of vehicle buses. The key component
of the network interface controller is the multi-function vehicle bus controller
(MVBC), which con rms with the protocol de ned in IEC 61375 [
First, strictly following the description of the standard IEC 61375, we build a top-level model for the network layer of an MVBC device in Tsmart-BIPEX as shown in Fig. 3. The top-level model of the network layer contains three components: the producer of a message, the consumer of a message, and the router which transmits a message from the source device to its destination device. The router is modeled as an atomic component abstracted in Fig. 5, which extracts the source device address and the destination device address from the processed message and composes a new message to send.
After several rounds of graphical model simulation, the MVBC model is automatically translated to an equivalent labeled transition system for VCS verication. We check several key requirements on the model, such as\the message should not be sent to the link-layer if the source device address equals the destination device address ". For the violated property, we need to check and revise the constructed model manually based on the counter example. This veri cation process strengthens the con dence in the constructed BIP model of MVBC.
When all properties pass the veri cation, we can automatically generate C++ code from the veri ed BIP model. The generated C++ source les contain 2,537 lines of code, including 623 lines of the BIP engine code to coordinate the components and interactions. Also, we write 146 lines of interface code to handle the embedded device's I/O communications. All codes are compiled by the armgcc-3.8 compiler to get an executable le running on the ARM processor of the MVBC device. Then, we connect the automatically synthesized MVBC device with the existing well-tested hand-written MVBC device, the communication between the two devices functions well. 6
In this paper, we present an integrated graphical development toolkit TsmartBIPEX to support the widely used BIP modeling language. With the integration of the graphical model editor interface and the model simulation interface, the convenience is greatly raised compared to the original textual model construction and command-line based simulation. By translating the BIP model to an equivalent labeled transition system, the veri cation e ciency is increased compared to the original RTD-Finder. Our future work may focus on the development and integration of more e cient code generation algorithms. 7
This research is sponsored in part by NSFC Program (No. 91218302, No. 61527812), National Science and Technology Major Project (No. 2016ZX01038101), Tsinghua University Initiative Scienti c Research Program (20131089331), MIIT IT funds (Research and application of TCN key technologies ) of China, and The National Key Technology R&D Program (No. 2015BAG14B01-02).