MOdel-based DEsign & Verification for Safety-Critical Embedded Systems

Overview of Selected Researches

Sr #

Author

Overview

Method of Validation

Category

Details

1

2012

Guglielmo et al. [1]

This paper presents integration approach of Model Driven Design (MDD) and Assertion Based Verification (ABV) in embedded systems for efficient design and verification.

Experiments and examples

General

This paper introduces integration of MDD and ABV by developing two tools i.e. radCASE and radCHECK. radCASE is developed to specify requirements in UML. Use case diagrams are used to specify high level requirements. Structure can be defined through Class, Composite structure, object and component diagrams. Behavior can be defined in state chart, sequence and activity diagrams. The developed models are then transformed to EFSM. It also incorporates the facility to generate complete C-code including ABV as defined in design. On the other hand, radCHECK tool provides facilities for dynamic ABV verification of embedded system design developed in redCASE. Ulisse stimuli generation engine is used in radCHECK to produce effective stimuli for verification.

2

2014

Kapos et.al [2]

This paper first highlights problems of SysML model simulation in MDA. Then, the generation of executable simulation code from

SysML system models are presented.

Case study

(Discrete event simulation)

General

This paper highlights problems of SysML model simulation in MDA. Thereafter, the generation of executable simulation code from SysML system models is presented. Authors also provide comprehensive literature review about MDA Modeling in SysML, Model transformation techniques / tools and code generation methodologies. Authors use QVT to produce executable DEVS models from SysML models. MediniQVT tool [121] is used to develop DEVS [122] MOF 2.0 meta-model and QVT transformation

3

2013

Berrani et al. [3]

This paper proposes transformation of SysML requirement diagram in Modelica to improve WSN properties using MDA approach

Case Study

(Traffic lights)

General

This paper introduces transformation of SysML requirement diagram in Modelica to improve WSN properties using MDA approach. Authors introduces modeling scheme for wireless sensor network (WSN) where SysML model is developed in Topcased tool [62] using Block, internal block, parametric, state machine diagrams to specify behavioral aspects. Thereafter, ATL [63] tool is used to transform SysML model into Modelica [128] and then Modelica model is transform into text.

4

2012

Sakairi et al. [4]

This paper introduces concept of SysML model and Simulink integration for MBSE.

Example of Dual Clutch Transmission (DCT)

Simulation

This paper proposes a tool to integrate SysML with Simulink [65] simulation tool. Dual Clutch Transmission (DCT) model is developed in Rhapsody using SYSML and validation is performed through Simulink. Block diagram is used to specify simulation context and Simulink sub-models are referred through SysML.

.

5

2010

Stancescu et al. [5]

This paper proposes Verilog code generation from SysML model

Example (Reed-Solomon decoder)

General

This paper proposes scheme for mapping Verilog modules to SysML parts, Verilog ports & signal to SysML flow port and Verilog process to SysML allocations. The SYSML model is developed and exported in XMI format to generate Verilog code for validation.

6

2014

Tsadimas et al. [6]

This paper introduces the concept of Evaluation View (diagram) to integrate simulation capabilities into SysML for DEVS simulation environment.

Case Study (Registry application)

General

This paper proposes SYSML based Evaluation View to describe the system under verification and conditions under which performance should be evaluated. Thereafter, executable simulated code is generated through evaluation view. Authors also include the simulation results in Evaluation View to verify performance requirements.

7

2013

Ouchani et al. [7]

This paper proposes the verification of system design (SysML) through formal verification framework.

Case study (audio player system)

General

This paper proposes formal verification framework for the verification of SysML based system design. The requirements are specify in SYSML activity diagrams through PCTL properties. The SysML model is verified through PRISM [66]. Thereafter, novel algorithm is proposed to transform SysML model to BlueSpec SytemVerilog code.

8

2012

Bouquet et al. [8]

This paper proposes scheme to generate VHDL-ASM code from SysML model.

Case study (Smart Surface system)

General

This paper proposes scheme to generate VHDL-ASM code from SysML model. Topcased tool is used to develop SYSML model through block definition and internal block diagrams along with behavior and constraints in parametric diagram. Model to Model transformation is performed through ATL and code generation from model to text is performed through Xpand.

9

2013

Tommasi et al. [9]

This paper proposes SysML modeling scheme based on the MARTe framework for designing real time application

Case study (Control System FTU)

General

This paper proposes SysML modeling scheme based on the MARTe framework for designing real time application. Topcased tool has been used for Modeling and Acceleo [67] tool is used for model-to-text transformation for code generation.

10

2012

Gomez et al. [10]

This paper proposes multi-view modeling scheme for embedded systems using UML, SysML and MARTE

Examples and theoretical reasoning

Modeling

This paper proposes multi-view modeling scheme for embedded systems using UML, SysML and MARTE. Each domain of proposed scheme can be managed in various views interconnected with each other. MARTE is used to for hardware model and non-functional properties. SysML is used to define equations.

11

2009

Andrade et al. [11]

This paper proposes requirement validation scheme for embedded systems by mapping SysML activity diagram to time petri net.

Case Study

(pulse-oximeter)

General

This paper proposes SysML activity to specify requirements. MARTE notations are used for execution time / energy consumption constraints. The developed model is mapped into ETPN which is used to verify different behavioral and structural aspects of ERTS systems including execution time and energy consumption.

12

2012

Quadri et al. [12]

This paper proposes combined utilization of SysML / MARTE notations for modeling embedded system requirements by developing tools for design specifications, validation and simulation for MADES FP7 Project.

Case Study

(Car collision avoidance system)

General

This paper discuss various tools / techniques of MADES Project for design specifications, validation and simulation are discussed e.g., MADAS language, diagrams etc. Car-Collision-Avoidance case study is modeled in Open source Modelio Editor [68] using MADES language. Hardware code is generated according to specifications by using Xilinx ISE [119] and EDK tools. On the other hand, Software code is also generated as per design specifications by using Anvil J [69] and CTV [113]. Zot tool [118] is used for verification and simulation.

13

2

0
1

4

Bazydlo et al. [13]

This paper proposes novel methodology to transform UML state machine diagram into Verilog code.

Example

(Trolley Control System)

General

This paper transforms UML models based on state machine diagram into Verilog code. Firstly, UML model is exported in XMI and temporary HCFSM model is developed. Secondly, Verilog code is generated from HCFSM. Features of some important current MDE tools and techniques are also discussed by authors e.g., MODCO [83] and MODEASY[84] etc

14

2013

Doligslski et. al [14]

This paper proposes modeling scheme based on UML and Petri net. VHDL / Verilog code is generated.

Examples and theoretical reasoning

General

This paper proposes HCFSM based modeling scheme using UML state machine for reconfigurable logical controllers. HCfgPN is developed which is used to generate VHDL / Verilog code. Transformation is done using QVT and VHDL / Verilog code is automatically generated using Eclipse M2M engine. Simulation is done using Aldec ActiveHDL and in-circuit verification is performed throughVirtex II-Pro

15

2010

Mueller et al. [15]

This paper proposes UML / SysML profiles to support co-modeling of C / SystemC with code generation facility in ARTiSAN studio.

Case Studies

(Broadband wireless communication and ALPR)

General

This paper introduces UML/SysML profiles used in SATURN project for synthesizable C and SystemC in order to support SystemC / C co-modeling by customizing Artisan Studio [114] SysML editor. This provides co-simulation facilities in QEMU software. This further helps to generate VHDL code from SystemC which can be used in ISE / EDK framework for FPGA configuration. Brief description of Artisan Studio is given that have automatic code generation facilities in various languages e.g., Java, ADA, SystemC etc

16

2012

Durand et al. [16]

This paper introduces new tool for transformation of UML model into the code of Bluespec System Verilog.

Examples and theoretical reasoning

General

This paper introduces new tool to generate Bluespec System Verilog code from UML models comprise activity and state diagrams. Proposed tool accept XMI format and then parse the XMI to generate BSV code. Magic draw tool having XMI export facility is used to develop UML model. XMI file analysis including tags evaluation and information identification is accomplished using XMLtool[85]. Apache Velocity [86] software is used to generate BSV code through VTL templates.

17

2008

Wood et al. [17]

This paper proposes transformation of UML models (state diagrams) into VHDL code by developing MODEASY transformation tool.

Case Study (Early Warning System)

General

This paper proposes MODEASY tool to transform UML state diagram model into VHDL code. QVT alike language [88] is used to specify transformation rules. MODEASY tool is developed using Eclipse platform [87] along with GEF [89] for visual editors. OCL-based template language [90] is used for code generation.

18

2010

Moreira et al. [18]

This paper proposes methodology to automatically generate VHDL code from UML models with the help of GenERTiCA tool

Case Study (Valve component system)

General

This paper proposes new technique to automatically generate VHDL code form UML models. Script-based approach is used to generate code through GenERTiCA tool [94]. Authors also discuss tools and techniques for VHDL code generation from models. For Example, StateCAD [92] tool that generate VHDL and System Verilog code from its bubble diagrams model. Simulink HDL Coder [93] generates Verilog and VHDL code from Simulink models.

19

2009

Vidal et al. [19]

This paper proposes MoPCoM technique to automatically generate VHDL code from UML / MARTE models.

Case study

(Viterbi decoder)

General

This paper proposes MoPCoM techniques that define three design levels (AML, EML and DML) where DML design rules are used for automatic code generation. IBM Rhapsody is used for modeling. MDworkbench [95] tool is used for transformation.

20

2011

Linehan and Clarke [20]

This paper presents a domain-specific modeling language for

e HVL. The e

Modeling language meta model is implemented in UML / MARTE from which e code is generated automatically.

Example of automotive semiconductor industry

General

This paper introduces new UML / MARTE profile that support code template for automatic e HVL code generation. Magic Draw tool is used for modeling and XMI format is used for code generation through Xpand [97].

21

2013

Herrera et al [21]

This paper proposes novel UML/MARTE DSE framework for complex embedded systems

Example of EFR vocoder system

General

This paper introduces embedded systems UML / MARTE modeling and DSE framework. The main component of framework is MOST tool for automatic design space exploration. COMPLEX Eclipse Application (CEA) tool comprises Eclipse EMF [115] and Acceleo for Model-to-text transformation. PapyrusMDT [98] tool is used for modeling. SCoPE+ [99] tool is used for analysis.

22

2010

Lecomate et al. [22]

This paper proposes MOPCOM design technique for building UML/MARTE model and automatic VHDL source code generation from the model.

Example of wireless communication (MIMO decoder )

General

The propose MOPCOM uses three modeling levels (i.e. AML, EML and DML). MOPCOM uses KerMeta [100] language for formalization and validation of models. Rhapsody is used for modeling. Sodius MDWorkbench [101] tool is used for model-to-model transformation. Model-to-text transformation for code generation is performed using CatapultC [116] tool. VHDL, C/C++ and SystemC codes are generated.

23

2012

Quadri et al. [23]

This paper investigates the various aspects of UML/ MARTE modeling in embedded systems. Thereafter, Gaspard2 is proposed as an alternative solution

Examples and theoretical reasoning

General

This paper investigates different advantages and limitation of UML/MARTE models to specify embedded systems requirements. Authors prove with examples that Gaspard2 [102][103] framework resolve different issues discover in UML / MARTE models. QVTO [104] tool (QVT standard) and Acceleo [105] tool is used for code generation

24

2013

DeJin et al. [24]

This paper presents architectural centric methodology for verification and validation of embedded systems.

Case study

General

This paper introduces UML notations to specify behavioral / temporal constraints through EAST-ADL. The models are then transformed to SPIN models for verification.

25

2008

Vanderperren et al. [25]

This paper presents comprehensive overview of UML modeling capabilities in System-on-Chip (Soc) design. Furthermore, various UML modeling and transformation tools are also discussed.

Examples and theoretical reasoning

General

This paper investigates the various aspects of UML profiles (SysML and MARTE) in SoC design. Different approaches are presented to efficiently specify structural and behavioral requirements of SoC. Thereafter, different diagrams of SysML and MARTE profiles are discussed for SoC requirements specification. Finally, comprehensive analysis of modeling and transformation tools is presented.

26

2012

Elhaji et al. [26]

This paper presents new modeling technique by extending various notations in UML / MARTE. Thereafter, VHDL code is generated from the model and successfully used for the verification of the system.

Case studies ( Mesh & torus , honeycomb and GEXspidergon topologies)

General

This paper presents technique to design NoC (Network-on-Chip) by extending various UML / MARTE notations. Gspard2 tool [106] is used for code generation which is available as Eclipse plug-in. SoC design in Gaspard2 is associated to MOC [107] which is based on ArrayOL [108].

27

2012

Riccobene et al. [27]

This paper proposes the integration of SysML and SystemC UML profiles.

Case study

(Counter System)

General

This paper proposes integration of SysML and SystemC UML profiles by mapping structural aspects of SysML to SystemC UML profile. On the other hand, behavioral aspects are managed though SysML Control flow graphs and SystemC process state machine.

28

2009

Penil et al. [28]

This paper proposes novel technique to automatically generate SystemC code from UML/MARTE profile.

Examples and Experiments

Modeling

This paper proposes automatic source code generation of SystemC by extracting system hierarchy and structure from UML / MARTE design. Authors describe the set of designing rules for mapping UML/MARTE models with SystemC specifications. HetSC [109][110] is used for code generation

29

2013

Iqbal et al. [29]

This paper presents technique for modeling the environment using UML / MARTE and OCL. These models are used for simulator generation to enable black-box system testing of RTES (Real-time embedded systems)

Case Study

(automated bottle recycling system)

General

This paper propose RTES scheme to model constraints, structure and behavior of the environment in UML / MARTE and OCL [111]. Simulator code along with automated test cases is generated in Java using MOFScript[112] through Model-to-text transformation

30

2009

Huascar et al. [30]

This paper investigates challenges of combining both SYSML and MARTE profiles for embedded system design

Examples and theoretical reasoning

Modeling

This paper proposes various methodologies to integrate SYSML and MARTRE profiles. it also presents different scenarios where SYSML and MARTE profiles can be potentially combined together for the improvements of embedded systems design.

31

2013

Ling et al. [31]

This paper investigates the potential utilization of CCSL to model scheduling requirements.

Examples and theoretical reasoning

Property specification

This paper investigates the potential utilization of CCSL to model scheduling requirements. State based ccLTS semantics have been proposed for CCSL. This eases the model verification process. The requirements specified in CCSL are then transformed in NuSMV models.

32

2012

Frederic Mallet [32]

This paper proposes automatic observer generation technique from CCSL specification.

Examples and theoretical reasoning

Property specification

This paper proposes automatic observer generation technique from CCSL specification. The proposal is based on a novel state based semantics for CCSL operators.

33

2011

Samir and ahmed [33]

This paper presents a novel approach for the verification of interoperability between various system components.

CyCab example

General

The system is modeled in SYSML Block definition, internal block and sequence diagrams. It further presents algorithm for transformation of SysML models into interface automata for verification

34

2014

Milena et al. [34]

This paper proposes MDEReq to improve requirement specification and change management of embedded systems

Case study (ABS)

Modeling

This paper proposes MDEReq to improve requirement specification and change management of embedded systems by integrating UML models with SYSML and MARTE notations. MDEReqTraceTool has been developed to analyze models and generate traceability matrixes for change management.

35

2013

Frederic Mallet [35]

This paper introduces the novel safety mechanism of CCSL specification by transforming it into Marked Graphs for conditions verification

Examples and theoretical reasoning

Model Verification

This paper presents novel safety mechanism by transforming CCSL constraints into marked graph. Thereafter, classical results have been applied on marked graphs to evaluate the safety of CCSL.

36

2008

Naiyong et al. [36]

This paper proposes efficient technique for assertion based verification by making use of Alternating Finite Automata (AFA).

Examples and Experiments

Simulation

This paper introduces novel assertion based verification technique by making use of Alternating Finite Automata (AFA). PSLsimple –VDV (Verilog Dynamic Verifier) tool is developed by using two Opensource tools i.e. Icarus-Verilog [72] and the GTKWave [71].

37

2010

Joel and Ekkart [37]

This paper proposes QVT and TGGs based model transformation scheme.

Examples and theoretical reasoning

Model Transformation

This paper investigates the similarities and differences of QVT and TGGs. Thereafter, mapping scheme of QVT-Core and TGGs is presented. This leads to the combined utilization of both QVT and TGGs to improve model transformation process

38

2013

Jong et al. [38]

This paper presents novel scheme to verify the correctness of model transformation.

Experiments

Model Transformation

This paper proposes verification of Model transformation through Meta information, property matching scheme for similarity and graph comparison algorithm.

39

2009

Roy et al. [39]

This paper evaluates various transformation attributes of three model transformation languages.

Examples and theoretical reasoning

Model Transformation

This paper presents comprehensive comparison of model transformation languages i.e. CGT, AGG and ATL. The results reveal that CGT has certain advantages over other two in terms of transformation efforts and simplicity.

40

2012

Peter and Laszlo [40]

This paper evaluates various attributes of graph rewriting-based transformation languages.

Case study

Model Transformation

This paper investigates various attributes of some popular model transformation languages used in different graph rewriting-based model transformation. The investigation is performed through case study. Thereafter, critical attributes of such transformation languages have been proposed.

41

2010

Esther et al. [41]

This paper proposes graphical language for Model-to-Model transformation.

Examples and experiments

Model Transformation

This paper proposes visual language to specify M2M transformations along with their transformation assurance properties. The proposed language support both trace-based and traceless model-to-model transformations. Furthermore, it is also capable to be compiled in OCL. Proof of concept implementation has been developed using Eclipse framework.

42

2012

Louis et al. [42]

This paper proposes basic feature set for Model-to-Text transformation languages.

Example and theoretical reasoning

Model Transformation

This paper investigates various features of contemporary M2T languages and proposes the basic features model for M2T languages. Applicability of proposed feature model is presented using MOFM2T [77] and Microsoft T4 [78]. However, this research work only proposes basic set of features those should be provided by model-to-text languages.

43

2012

Anderson et al. [43]

This paper proposes novel technique MetaTT for M2T transformation

Scenarios

Model Transformation

This paper proposes novel technique MetaTT for M2T transformation. A tool is implemented as a Proof-of-concept using MOFScript and Ecore to support some steps of proposed MetaTT. Validation is performed through four scenarios by comparing M2T transformations of MetaTT with other informal approaches.

44

2014

Dionisio [44]

This paper proposes novel methodology HIPAO2 for embedded systems development using MDE approach

Case Study UAV

General

This paper proposes HIPAO2 for embedded systems development through MDE approach. Particularly, MDE Modeling and Model transformation (along with code generation) phases are supported by HIPAO2. SysML is used for modeling by employing papyrus editor. ATL is used for M2M transformation and Acceleo is used for M2T transformation

45

2014

Juan and Esther [45]

This paper proposes novel transformation approach to improve reusability of transformations between meta-models

Examples and theoretical reasoning

Model Transformation

This paper proposes new graph based transformation technique to improve the reusability of transformations between meta-models. Binding and adapters are used to resolve specified differences between concept and meta-models

46

2014

Kolahdouz et al. [46]

This paper proposes framework for evaluation of model transformation techniques.

Case Study

Model Transformation

This paper proposes framework for ISO/IEC 9126-1 quality-attributes based evaluation of model transformation techniques. Five different model transformation techniques (GrGen [73],Kermeta [74],QVT-R [75],ATL [76],UML-RSDS [79]) have been evaluated through proposed framework to show its applicability. Proposed framework facilitates the selection of most appropriate transformation technique for particular problem.

47

2010

Tuomas et al. [47]

This paper proposes model verification technique for PSL safety properties

Experiments

Model Verification

This paper proposes transducers encoding based methodology to check the model for PSL safety properties. Validation is performed through experiments where two PSL research practices have been compared with proposed methodology.

48

2009

Meng et al. [48]

This paper proposes HAPSL to verify PSL properties

Experiments

Model Verification

This paper proposes HAPSL for the verification of both statistical and temporal properties of PSL. Proposed HAPSL is extension of PSL by utilizing Hybrid Automata. Validation is performed through experimentation on two circuits.

49

2013

Uchevler and Kjetil [49]

This paper proposes assertion based verification approach.

Case study

Model Verification

This paper proposes novel assertion based verification approach by implementing PSL operations in Haskell using CLaSH tool

50

2013

Veronica et al. [50]

This paper proposes MeTHAGeM framework to support model transformations for MDD

Case studies

Model Transformation

This paper proposes MeTHAGeM framework to support model transformations for MDD. It incorporates the collection of DSLs to facilitate the modeling of model transformations to reduce the development efforts of model transformations. Furthermore, it also improves the interoperability problems among various model transformation languages.

51

2012

Adrian et al. [51]

This paper proposes model transformation technique for including constraints in transformation rules.

Examples and theoretical reasoning

Model Transformation

This paper proposes graph based model transformation technique that facilitates the inclusion of constraints in transformation rules. Proposed technique introduces three stages of model transformation i.e. combined meta-model, specification of transformation rules including constraints and finally, applying the model transformation

52

2014

Samir et al. [52]

This paper proposes model verification framework for the verification of behavioral aspects.

Case studies

General

This paper proposes framework for the verification of behavioral aspects specify in SysML activity diagrams. It provides mechanism to represent behavioral aspects modeled in SysML activity diagrams into PRISM model which is then used for verification of PCTL properties.

53

2013

Luciane et al [53]

This paper presents Brazilian survey to investigate the usage of UML and MDE for embedded systems

Survey

General

This paper performs survey in Brazil to highlight the potential utilization of UML and MDE for embedded systems. This survey investigates current industrial practices to highlight some critical statistics about UML and MDE utilization for embedded systems

54

2013

Bijan and Payman [54]

This paper proposes new approach for equivalence verification and error detection / removal mechanism of RTL designs

Experiments

Model Verification

This paper proposes novel methodology to improve the equivalence verification and error detection / removal mechanism for RTL designs. HED and SMT solvers are used to verify the equivalence among two models at RTL level. Furthermore, mutation based approach is used to improve error detection / removal mechanism. Validation is performed through experiments by comparing proposed methodology using various benchmarks.

55

2011

Daniel et al. [55]

This paper proposes TEPE language to graphically express temporal properties through parametric diagrams of SysML

Case study Elevator Ssytem

General

This paper proposes TEPE language to graphically express temporal properties through parametric diagrams of SysML. Moreover, TEPE is incorporated in SysML profile AVATAR which has rich capabilities to specify time-constraint properties for early verification. Furthermore, open source tool (TTool [117]) is customized to incorporate AVATAR-TEPE support for editing diagrams and their transformation to UPPAAL (up to some extent).

56

2012

Ning et al. [56]

This paper proposes novel methodology to formally specify and verify task-level time constraints.

Case study

General

This paper presents novel methodology to formally specify and verify task-level time constraints. It extends CCSL to include particular improvements for time constraints. TPN based verification method is develop for verification. Proposed methodology is incorporated in verification framework (Ge et al [120]).

57

2011

Razieh et al [57]

This paper proposes ExSAM profile for embedded systems.

Case studies

Modeling

This paper proposes ExSAM profile for embedded systems by integrating SYSML and AADL. The combination of SYSML and AADL leads to manage diverse modeling requirements for embedded systems.

58

2013

Luciano et al [58]

This paper MADES approach for model verification and validation of embedded systems

Case studies

General

This paper present model verification and validation approach which is used in MADES project. Various notations of UML and MARTE profiles are combined together in a systematic way to specify the requirements of embedded systems. These notations are further used for formal verification of model. Simulation capabilities are also incorporated in MADES using Modelica.

59

2012

Xiaopu et al [59]

This paper proposes a novel methodology to improve the model verification by integrating SYSML state machine diagram and MARTE notations.

Case Study (TS)

General

This paper introduces extension of SYSML state machine diagram by integrating MARTE time notations to improve the modeling of system behavioral aspects. Furthermore, a novel algorithm is introduced to transform extended SYSML state machine diagram into timed automata. The model is then verified through Uppaal [123].

60

2014

Minh et al [60]

This paper introduces novel approach to model timing aspects of embedded systems by integrating UML diagrams with MARTE notations.

Example (pacemaker)

General

This paper proposes methodology to improve the modeling of embedded systems timing aspects by making use of UML sequence and state machine diagrams with MARTE notations. The TMC [124] tool is developed which can be used with papyrus and Visual paradigm [126] eclipse plug-ins.

61

2012

Erwan et al. [61]

This paper presents novel model verification approach by specifying safety critical systems requirements in model through SYSML, OCL and Alf.

Case study

(Railway)

General

This paper first introduces SYSML block definition and state machine diagrams to specify requirements where OCL is used to specify constraints and Alf [127] is used to specify behavior. Thereafter, the developed model is transformed to B method to perform potential verification and validation activities through SYSML to B translator tool [125].





References

References

[1] Giuseppe Di Guglielmo, Luigi Di Guglielmo, Andreas Foltinek,, Masahiro Fujita, Franco Fummi, Cristina Marconcini and Graziano Pravadelli: On the integration of model-driven design and dynamic assertion-based verification for embedded software, Journal of Systems and Software, Volume 86, Issue 8, August 2013, Pages 2013–2033. DOI: 10.1016/j.jss.2012.08.061

[2] George-Dimitrios Kapos, Vassilis Dalakas, Anargyros Tsadimas, Mara Nikolaidou and Dimosthenis Anagnostopoulos: Model-based system engineering using SysML: Deriving executable simulation models with QVT, 8th Annual IEEE Systems Conference (SysCon) 2014, Pages 531-538. DOI: 10.1109/SysCon.2014.6819307

[3] Samir Berrani, Ahmed Hammad, Hassan Mountassir: Mapping SysML to Modelica to Validate Wireless Sensor Networks Non-Functional Requirements, 11th International Symposium on Programming and Systems (ISPS) 2013, Pages 177-186. DOI: 10.1109/ISPS.2013.6581484

[4] Takashi Sakairi, Eldad Palachi, Chaim Cohen, Yoichi Hatsutori, Junya Shimizu, and Hisashi Miyashita: Designing a control system using SysML and Simulink, Proceedings of SICE Annual Conference 2012, Pages 2011-2017.

[5] Stancescu,S. Neagoe, L. ; Marinescu, R. ; Enoiu, E.P.: A SysML model for code correction and detection systems, Proceedings of 33rd International Convention MIPRO 2010, Pages 189-191.

[6] Anargyros Tsadimas, George-Dimitrios Kapos, Vassilis Dalakas, Mara Nikolaidou and Dimosthenis Anagnostopoulos: Integrating simulation capabilities into SysML for enterprise information system design, 9th International Conference on System of Systems Engineering (SOSE) 2014, Pages 272-277. DOI: 10.1109/SYSOSE.2014.6892500

[7] Samir Ouchani, Otmane Ait Mohamed and Mourad Debbabi: A Formal Verification Framework for BlueSpec System Verilog, Forum on Specification and Design Languages (FDL) 2013, Pages 1-7.

[8] Fabrice Bouquet, Jean-Marie Gauthier, Ahmed Hammad and Fabien Peureux: Transformation of SysML Structure Diagrams to VHDL-AMS, Second Workshop on Design, Control and Software Implementation for Distributed MEMS (dMEMS) 2012, Pages 74-81, DOI: 10.1109/dMEMS.2012.12

[9] Gianmaria DeTommasi, Riccardo Vitelli, Luca Boncagni, and André C. Neto: Modeling of MARTe-Based Real-Time Applications With SysML, IEEE Transactions on Industrial Informatics 2013, Volume 9, Issue 4, Pages 2407-2415, DOI: 10.1109/TII.2012.2235073

[10] Carlos Gomez, Julien DeAntoni and Frederic Mallet: Multi-View Power Modeling based on UML MARTE and SysML, 38th EUROMICRO Conference on Software Engineering and Advanced Applications (SEAA) 2012, Pages 17-20, DOI: 10.1109/SEAA.2012.66

[11] Ermeson Andrade, Paulo Maciel, Gustavo Callou and Bruno Nogueira: A Methodology for Mapping SysML Activity Diagram to Time Petri Net for Requirement Validation of Embedded Real-Time Systems with Energy Constraints, Third International Conference on Digital Society ICDS 2009, Pages 266-271, DOI: 10.1109/ICDS.2009.19

[12] Imran R. Quadri, Etienne Brosse, Ian Gray, Nicholas Matragkas, Leandro Soares Indrusiak, Matteo Rossi, Alessandra Bagnato and Andrey Sadovykh: MADES FP7 EU Project: Effective High Level SysML/MARTE Methodology for Real-Time and Embedded Avionics Systems, 7th International Workshop Reconfigurable Communication-centric Systems-on-Chip (ReCoSoC) 2012, Pages 1-8, DOI: 10.1109/ReCoSoC.2012.6322882

[13] Grzegorz Bazydlo, Marian Adamski and Lukasz Stefanowicz: Translation UML diagrams into Verilog, 7th International Conference on Human System Interactions (HSI) 2014, Pages 267-271, DOI: 10.1109/HSI.2014.6860487

[14] Michal Doligalski and Marian Adamski: UML state machine implementation in FPGA devices by means of dual model and Verilog Translation UML diagrams into Verilog, 11th International Conference on Industrial Informatics (INDIN) 2013, Pages 177-184, DOI: 10.1109/INDIN.2013.6622878

[15] Wolfgang Mueller, Da He, Fabian Mischkalla Arthur Wegele, Paul Whiston, Pablo Penil and Eugenio Villar: The SATURN Approach to SysML-based HW/SW Codesign, IEEE Computer Society Annual Symposium on VLSI (ISVLSI) 2010, Pages 506-511, DOI: 10.1109/ISVLSI.2010.95

[16] Sergio H. M. Durand and Vanderlei Bonato: A tool to support Bluespec System Verilog coding based on UML diagrams, IEEE 38th Annual Conference on Industrial Electronics IECON 2012, Pages 4670-4675, DOI: 10.1109/IECON.2012.6389493

[17] Stephen K. Wood, David H. Akehurst, Oleg Uzenkov, W. Gareth J. Howells, and Klaus D. McDonald-Maier: A Model-Driven Development Approach to Mapping UML State Diagrams to Synthesizable VHDL, IEEE Transactions on Computers 2008, Volume 57, Issue 10, Pages 1357-1371, DOI: 10.1109/TC.2008.123

[18] Tomas G. Moreira, Marco A. Wehrmeister, Carlos E. Pereira, Jean-Francois Petin and Eric Levrat: Automatic Code Generation for Embedded Systems: From UML Specifications to VHDL Code, IEEE 8th International Conference on Industrial Informatics (INDIN) 2010, Pages 1085-1090, DOI: 10.1109/INDIN.2010.5549590

[19] Jorgiano Vidal, Florent de Lamotte, Guy Gogniat, Philippe Soulard and Jean-Philippe Diguet: A co-design approach for embedded system modeling and code generation with UML and MARTE, Conference and Exhibition Design Automation and Test in Europe (DATE) 2009, Pages 226-231, DOI: 10.1109/DATE.2009.5090662

[20] Eamonn Linehan and Siobhan Clarke: An aspect-oriented, model-driven approach to functional hardware verification, Journal of Systems Architecture, Elsevier 2012, Volume 58, Issue 5, Pages 195-208, DOI: 10.1016/j.sysarc.2011.02.001

[21] Fernando Herrera , Hector Posadas, Pablo Penil, Eugenio Villar, Francisco Ferrero, Raul Valencia and Gianluca Palermo: The COMPLEX methodology for UML/MARTE Modeling and design space exploration of embedded systems, Journal of Systems Architecture, Elsevier 2014, Volume 60, Issue 1, Pages 55-78, DOI: 10.1016/j.sysarc.2013.10.003

[22] Stephane Lecomte, Samuel Guillouard, Christophe Moy, Pierre Leray and Philippe Soulard : A co-design methodology based on model driven architecture for real time embedded systems, Mathematical and Computer Modelling, Elsevier 2011, Volume 53, Issue 3-4, Pages 471-484, DOI: 10.1016/j.mcm.2010.03.035

[23] Imran Rafiq Quadri, Abdoulaye Gamatie, Pierre Boulet, Samy Meftali and Jean-Luc Dekeyser: Expressing embedded systems configurations at high abstraction levels with UML MARTE profile: Advantages, limitations and alternatives, Journal of Systems Architecture, Elsevier 2012, Volume 58, Issue 5, Pages 178-194, DOI: 10.1016/j.sysarc.2012.01.001

[24] DeJiu Chen, Lei Feng, Tahir Naseer Qureshi, Henrik Lonn and Frank Hagl : An architectural approach to the analysis, verification and validation of software intensive embedded systems, Computing, SPRINGER 2013, Volume 95, Issue 8, Pages 649-688, DOI: 10.1007/s00607-013-0314-4

[25] Yves Vanderperren, Wolfgang Mueller and Wim Dehaene: UML for electronic systems design: a comprehensive overview, Design Automation for Embedded Systems, SPRINGER 2008, Volume 12, Issue 4, Pages 261-292, DOI: 10.1007/s10617-008-9028-9

[26] Majdi Elhaji, Pierre Boulet, Abdelkrim Zitouni, Samy Meftali, Jean-Luc Dekeyser and Rached Tourki: System level modeling methodology of NoC design from UML-MARTE to VHDL, Design Automation for Embedded Systems, SPRINGER 2012, Volume 16, Issue 4, Pages 161-187, DOI: 10.1007/s10617-012-9101-2

[27] Elvinia Riccobene and Patrizia Scandurra: Integrating the SysML and the SystemC-UML profiles in a model-driven embedded system design flow, Design Automation for Embedded Systems, SPRINGER 2012, Volume 16, Issue 3, Pages 53-91, DOI: 10.1007/s10617-012-9097-7

[28] P. Penil, J. Medina, H. Posadas and E. Villar: Generating heterogeneous executable specifications in SystemC from UML/MARTE models, Innovations in Systems and Software Engineering, SPRINGER 2010, Volume 6, Issue 1-2, Pages 65-71, DOI: 10.1007/s11334-009-0105-4

[29] Muhammad Zohaib Iqbal, Andrea Arcuri and Lionel Briand: Environment modeling and simulation for automated testing of soft real-time embedded software, Software and System Modeling, SPRINGER 2013, DOI: 10.1007/s10270-013-0328-6

[30] Huascar Espinoza, Daniela Cancila, Bran Selic and Sebastien Gerard: Challenges in Combining SysML and MARTE for Model-Based Design of Embedded Systems, LNCS SPRINGER 2009, Volume 5562, Page 98-113 DOI: 10.1007/978-3-642-02674-4_8

[31] Ling Yin, Jing Liu, Zuohua Ding ; Mallet, F., de Simone, R.: Schedulability Analysis with CCSL Specifications, 20th Asia-Pacific Software Engineering Conference (APSEC) 2013, Pages 414-421 DOI: 10.1109/APSEC.2013.62

[32] Frederic Mallet: Automatic Generation of Observers from MARTE / CCSL, 23rd IEEE Symposium on Rapid System Prototyping (RSP) 2012, Pages 86-92

DOI: 10.1109/RSP.2012.6380695

[33] Samir Chouali and Ahmed Hammad: Formal verification of components assembly based on SysML and interface automata, Innovations in Systems and Software Engineering, SPRINGER 2011, Volume 7, Issue 4, Pages 265-274 DOI: 10.1007/s11334-011-0170-3

[34] Milena Rota Sena Marques, Eliane Siegert and Lisane Brisolara: Integrating UML, MARTE and SysML to improve requirements specification and traceability in the embedded domain, 12th IEEE International Conference on Industrial Informatics (INDIN) 2014, Pages 176-181 DOI: 10.1109/INDIN.2014.6945504

[35] Frederic Mallet, Jean-Vivien Millo and Robert de Simone: Safe CCSL specifications and Marked Graphs, 11th IEEE / ACM International Formal Methods and Models for Codesign (MEMOCODE) 2013, Pages 157-166

[36] Naiyong Jin, Chengjie shen, Jun chen and Taoyong Ni: Engineering of An Assertion-based PSLSimple-Verilog Dynamic Verifier by Alternating Automata, Electronics Notes in Theoretical Computer Science 2008, Volume 207, Pages 153-169 DOI: 10.1016/j.entcs.2008.03.091

[37] Joel Greenyer and Ekkart Kindler: Comparing relational model transformation technologies: implementing Query/View/Transformation with Triple Graph Grammars, Software & Systems Modeling, SPRINGER 2010, Volume 9, Issue 1, Pages 21-46 DOI: 10.1007/s10270-009-0121-8

[38] Jong-Won Ko, Kyung-Yong Chung and Jung-Soo Han: Model transformation verification using similarity and graph comparison algorithm, Multimedia tools and applications, SPRINGER 2013, DOI: 10.1007/s11042-013-1581-y

[39] Roy Gronmo, Birger Moller-Pedersen and Goran K. Olsen: Comparison of Three Model Transformation Languages, Model Driven Architecture – Foundation and applications, SPRINGER 2009, Volume 5562, Pages 2-17 DOI: 10.1007/978-3-642-02674-4_2

[40] Peter Feher and Laszlo Lengyel: The challenges of a model transformation language, IEEE 19th International Conference and Workshops on Engineering of Computer Based Systems (ECBS) 2012, Pages 324-329 DOI: 10.1109/ecbs.2012.6487443

[41] Esther Guerra, Juan de Lara, Dimitris Kolovos and Richard Paige: A Visual Specification Language for Model-to-Model Transformations, IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC) 2010, Pages 119-126 DOI: 10.1109/VLHCC.2010.25

[42] Louis M. Rose, Nicholas Matragkas, Dimitrios S. Kolovos and Richard F. Paige: A Feature Model for Model-to-Text Transformation Languages, ICSE Workshop on Modeling in Software Engineering (MISE) 2012, Pages 57-63 DOI: 10.1109/MISE.2012.6226015

[43] Anderson Ledo, Franklin Ramalho and Nata Melo: MetaTT – A Metamodel Based Approach for Writing Textual Transformations, 6th Brazilian Symposium on Software Components Architectures and Reuse (SBCARS) 2012, Pages 61-70 DOI: 10.1109/SBCARS.2012.21

[44] Dionisio Doering: A Model Driven Engineering Methodology for Embedded System Designs - HIPAO2, 12th IEEE International Conference on Industrial Informatics (INDIN) 2014Pages 787-790 DOI: 10.1109/INDIN.2014.6945614

[45] Juan de Lara and Esther Guerra: Towards the flexible reuse of model transformations: A formal approach based on graph transformation, Journal of Logical and Algebraic Methods in Programming 2014, Volume 83, Issues 5-6, Pages 427-458 DOI: 10.1016/j.jlamp.2014.08.005

[46] S. Kolahdouz-Rahimi, K. Lano, S. Pillay, J. Troya and P. Van Gorp: Evaluation of model transformation approaches for model refactoring, Science of Computer Programming 2014, Volume 85, Part A, Pages 5-40 DOI: 10.1016/j.scico.2013.07.013

[47] Tuomas Launiainen, Keijo Heljanko and Tommi Junttila: Efficient Model Checking of PSL Safety Properties, 10th International Conference on Application of Concurrency to System Design (ACSD) 2010, Pages 95-104 DOI: 10.1109/ACSD.2010.27

[48] Meng Zhang, Deyuan Gao and Xiaoya Fan: Formal Verification of Mixed-signal Circuits using Extended PSL, 8th International Conference on ASIC 2009, Pages 1288-1293 DOI: 10.1109/ASICON.2009.5351231

[49] B.N. Uchevler and Kjetil Svarstad: Assertion Based Verification Using PSL-like Properties In Haskell, 16th International Symposium on Design and Diagnostics of Electronic Circuits & Systems (DDECS) 2013, Pages 254-257 DOI: 10.1109/DDECS.2013.6549828

[50] Veronica Andrea Bollati, Juan Manuel Vara, Alvaro Jimenez and Esperanza Marcos: Applying MDE to the (semi-)automatic development of model transformations, Information and Software Technology 2013, Volume 55, Issue 4, Pages 699-718 DOI: 10.1016/j.infsof.2012.11.004

[51] Adrian Rutle, Alessandro Rossini, Yngve Lamo and Uwe Wolter: A formal approach to the specification and transformation of constraints in MDE, The Journal of Logic and Algebraic Programming 2012, Volume 81, Issue 4, Pages 422-457 DOI: 10.1016/j.jlap.2012.03.006

[52] Samir Ouchani, Otmane Ait Mohamed and Mourad Debbabi: A formal verification framework for SysML activity diagrams, Experts Systems with Applications 2014, Pages 2713-2728.

[53] Luciane Telinski Wiedermann anger, Inali Wisniewski Soares and Paulo Cezar Stadzisz: A Brazilian survey on UML and model-driven practices for embedded software development, The Journal of systems and software 2013, Pages 997-1005

[54] Bijan Alizadeh and Payman Behnam: Formal equivalence verification and debugging techniques with auto-correction mechanism for RTL designs, Microprocessors and Microsystems 2013, Pages 1108-1121

[55] Daniel Knorreck and Ludovic Apvrille: TEPE: A SysML Language for Time-Constrained Property Modeling and Formal Verification, ACM SIGSOFT Software Engineering Notes 2011, Volume 36, Issue 1, Pages 1-8 DOI: 10.1145/1921532.1921556

[56] Ning Ge, Marc Pantel and Xavier Cregut: Formal Specification and Verification of Task Time Constraints for Real-Time Systems, LNCS SPRINGER 2012, Volume 7610, Pages 143-157 DOI: 10.1007/978-3-642-34032-1_16

[57] Razieh Behjati, Tao Yue, Shiva Nejati, Lionel Briand and Bran Selic: Extending SysML with AADL Concepts for Comprehensive System Architecture Modeling, LNCS SPRINGER 2011, Volume 6698, Pages 236-252 DOI: 10.1007/978-3-642-21470-7_17

[58] Luciano Baresi, Gundula Blohm, Dimitrios S. Kolovos, Nicholas Matragkas, Alfredo Motta, Richard F. Paige, Alek Radjenovic and Matteo Rossi: Formal verification and validation of embedded systems: the UML-based MADES approach, Software and Systems Modeling SPRINGER 2013, DOI: 10.1007/s10270-013-0330-z

[59] Xiaopu Huang, Qingqing Sun, Jiangwei Li, Minxue Pan and Tian Zhang: An MDE-Based Approach to the Verification of SysML State Machine Diagram, Proceedings of the Fourth Asia-Pacific Symposium on Internetware Software, Article 9, ACM 2012, DOI: 10.1145/2430475.2430484

[60] Minh Chau Nguyen, Eunkyoung Jee, Jinho Choi and Doo-Hwan Bae: Automatic Construction of Timing Diagrams from UML/MARTE Models for Real-Time Embedded Software, Proceedings of the 29th Annual ACM Symposium 2014, Pages 1140-1145, DOI: 10.1145/2554850.2555011

[61] Erwan Bousse, David Mentre, Benoit Combemale, Benoit Baudry and Takaya Katsuragi: Aligning SysML with the B Method to Provide V&V for Systems Engineering, Proceedings of the Workshop on Model-Driven Engineering, Verification and Validation, ACM 2012, Pages 11-16, DOI: 10.1145/2427376.2427379

[62] Topcased Tool, Last Accessed August 2014. http://www.topcased.org/

[63] Eclipse ATL, Last Accessed August 2014. www.eclipse.org/atl/

[64] B. Kitchenham, Procedures for Performing Systematic Reviews,TR/SE-0401/NICTA, Technical Report 0400011T, Keele University, 2004.

[65] Math works Simulink, Last Accessed August 2014. www.mathworks.com/products/simulink/

[66] M. Kwiatkowska, G. Norman, and D. Parker, “PRISM 4.0: Verification of Probabilistic Real-Time Systems,” in CAV, ser. LNCS. Springer, 2011, pp. 585–591

[67] Eclipse Acceleo, Last Accessed August 2014. https://wiki.eclipse.org/Acceleo/

[68] Modelio, “Open source UML Editor and MDE Workbench,” 2012, www.modelio.org.

[69] Ian Gray and Neil C. Audsley, “Developing Predictable Real-Time Embedded Systems Using AnvilJ,” in IEEE Real-Time and Embedded Technology and Applications Symposium. IEEE Computer Society, 2012, pp. 219–228.

[70] I. Beer et al. ‘‘The temporal logic sugar,’’ in Proc. Comput. Aided Verific 2001.

[71] Tony Bybell. Gtkwave. http://home.nc.rr.com/gtkwave/index.html

[72] Stephen Williams. Icarus verilog. http://www.icarus.com/eda/verilog/index.html

[73] E.Jakumeit, S .Buchwald, M.Kroll, GrGen.NET: The expressive, convenient and fast graph rewrite system,Int.J.Softw.ToolsTechnol.Transf.12(2010)263–271.

[74] Z.Drey, C.Faucher, F.Fleurey, V.Mahe, D.Vojtisek, Kermeta Language Reference Manual, https://www.kermeta.org/docs/KerMeta-Manual.pdf,April2009.

[75] ObjectManagementGroup,Query/View/TransformationSpecification,2010.

[76]F.Jouault, F.Allilaire, J.Bézivin, I.Kurtev, ATL: A model transformation tool, Sci.Comput.Program.72(1–2)(2008)31–39.

[77] OMG, “MOF Model to Text Transformation Language, v1.0 [online],” [Accessed 17 January 2012] Available at: http://www.omg.org/spec/MOFM2T/1.0/, 2008.

[78] Microsoft T4, Last Accessed September 2014. http://msdn.microsoft.com/en-us/library/bb126445.aspx

[79] K.Lano, S.Kolahdouz-Rahimi, TheUML RSDStoolset , http://www.dcs.kcl.ac.uk/staff/kcl/uml2web,2012.

[81] R. Armony et al. ‘‘The ForSpec temporal logic: A new temporal property-specification language,’’ Tools and Algorithms for Construct. Analy. Syst., 2002.

[82] N. Fedida, J. Havlicek, N. Levi, and H. Miller, CBV Semantics, 2002. [Online]. Available: http://www.vhdl.org/vfv/hm/att-0672/01-cbv_semantics.pdf.

[83] S. Wood, D. Akehurst, O. Uzenkov, W. Howells, K. McDonald-Maier, “A model-driven development approach to mapping UML state diagrams to synthesizable VHDL”, Computers, IEEE Transactions on, Vol. 57, No. 10, 2008, pp. 1357–1371.

[84] IEEE scientific database, Last Accessed, July 2014. http://ieeexplore.ieee.org/

[85] Sparx Systems Enterprise Architecture , http://www.sparxsystems.com/resources/mdg_tech/

[86] Apache Software Foundation. (2010, Nov.) The Apache Velocity Project. [Online]. Available: http://velocity.apache.org/

[87] IBM, “Eclipse Universal Tool Platform,” http://www.eclipse.org, 2008.

[88] D.H. Akehurst, W.G. Howells, and K.D. McDonald-Maier, “Kent Model Transformation Language,” Proc. Model Transformations in Practice Workshop, part of the ACM/IEEE Eighth Int’l Conf. Model Driven Eng. Languages and Systems (MoDELS), 2005.

[89] IBM, “Eclipse Modeling Framework,” http://www.eclipse.org/gef/ 2008.

[90] D.H. Akehurst and O. Patrascoiu, “Tooling Metamodels with Patterns and OCL,” Proc. First Int’l Workshop Metamodelling for MDA, A. Evans, P. Sammut, and J.S. Willans, eds., Nov. 2003.

[91] F. Coyle, and M. Thornton, “From UML to HDL: a Model-Driven Architectural approach to hardware-software co-design”. Information Systems: New Generations Conference (ISNG), Las Vegas, 2005.

[92] Xilinx official website, Last Accessed September, 2014. http://www.xilinx.com/

[93] Math Works HDL coder, Last Accessed October, 2014 http://www.mathworks.com/products/slhdlcoder/

[94] M. A. Wehrmeister, E. P. Freitas, C. E. Pereira, and F. Ramming, F., “GenERTiCA: A Tool for Code Generation and Aspects Weaving”. 11th IEEE Symposium on Object Oriented Real-Time Distributed Computing (ISORC), Orlando, 2008.

[95] “MDWorkbench platform,” www.mdworkbench.com, from SODIUS.

[96] L. Li, F.P. Coyle, M.A. Thornton, UML to SystemVerilog synthesis for embedded system models with support for assertion generation, in: Proceedings of the ECSI Forum on Design Languages, 2007.

[97] A. Bunker, G. Gopalakrishnan, S.A. Mckee, Formal hardware specification languages for protocol compliance verification, ACM Trans. Des. Autom. Electron. Syst. 9 (1) (2004) 1–32.

[98] Papyrus MDT. Available from: <http://www.eclipse.org/modeling/mdt/papyrus/>.

[99] H. Posadas, E. Villar, Automatic Communication Modelling for early exploration of HW/SW allocation based on native co-simulation, in: Proc. Of XXVI Conf. on Design of Circuits and Integrated Systems, DCIS’11, 2011.

[100] INRIA, KerMeta meta-programming environment, www.kermeta.org.

[101] SODIUS, MDWorkbench platform, www.mdworkbench.com.

[102] DaRT team, GASPARD SoC Framework, 2010. Available from: <http://www.gaspard2.org/>.

[103] A. Gamatié, S. Le Beux, E. Piel, A. Etien, R.B. Atitallah, P. Marquet, J.-L. Dekeyser, A model driven design framework for high performance embedded systems, Research Report RR-6614, INRIA, 2008. Available from: <http://hal.inria.fr/inria-00311115/en>.

[104] OMG, M2M/Operational QVT Language, 2007. Available from: <http://tiny.cc/tFGGx>.

[105] Acceleo, MDA code generator, 2009. Available from: <http://www.acceleo.org/pages/home/en>.

[106] Gamatié A, Le Beux S, Piel E, Ben Atitallah R, Etien A, Marquet P, Dekeyser JL (2011) A model driven design framework for massively parallel embedded systems. ACM Trans Embed Comput Syst 10(4):2–36

[107] Boulet P (2008) Formal semantics of Array-OL, a domain specific language for intensive multidimensional signal processing. INRIA res rep RR-6467

[108] Demeur A, Del Gallo Y (1998) An array approach for signal processing design. In: Proceedings of

Sophia-Antipolis conference on micro-electronics (SAME98)

[109] G. Taentzer, AGG: A Graph Transformation Environment for Modeling

and Validation of Software. Springer, 2004, vol. 3062, pp. 446–453.

[110] Herrera F, Villar E (2006) A framework for embedded system specification under different models of computation in SystemC. In: Annual ACM IEEE design automation conference proceedings of the 43rd annual conference on design automation

[111] OMG: Object Constraint Language Specification, Version 2.2. Object Management Group Inc. (2010). http://www.omg.org/spec/OCL/2.2/

[112] 68. Oldevik, J.: MOFScript user guide. Version 0.6 (MOFScript v 1.1. 11) (2006)

[113] I. Gray and N. Audsley, “Exposing non-standard architectures to embedded software using compile-time virtualisation,” in International conference on Compilers, architecture, and synthesis for embedded systems (CASES’09), 2009.

[114] Artisan Studio, Last Accessed October, 2014. http://www.atego.com/products/atego-modeler/

[115] Eclipse Modelling Framework. Available from: <http://www.eclipse.org/modeling/emf/>.

[116] Catapult Last Accessed, October, 2014. www.calypto.com/en/products/catapult/overview/

[117] Ttool Last Accessed, October 2014. http://ttool.telecom-paristech.fr/

[118] Zot tool, Last Accessed, October 2014. http://home.deib.polimi.it/pradella/Zot/

[119] Xilinx ISE, Last Accessed, October 2014. http://www.xilinx.com/products/design-tools/ise-design-suite.html

[120] Ge, N., Pantel, M.: Time Properties Verification Framework for UML-MARTE Safety Critical Real-Time Systems. In: Vallecillo, A., Tolvanen, J.-P., Kindler, E., Störrle, H., Kolovos, D. (eds.) ECMFA 2012. LNCS, vol. 7349, pp. 352–367. Springer, Heidelberg (2012)

[121] QVT Project Last Accessed October 2014. http://projects.ikv.de/qvt

[122] DEVS Last Accessed, September 2014. http://en.wikipedia.org/wiki/DEVS

[123] UPPAAL tool Last Accessed October 2014. http://www.uppaal.com/

[124] TMC, Last Accessed October, 2014 http://se.kaist.ac.kr/nmchau/tmc/

[125] SYSML to B tool. Last Accessed October 2014. http://www.irisa.fr/triskell/Software/protos/sysml2b/index_html

[126] Visual Paradigm, Last Accessed October 2014. http://www.visual-paradigm.com

[127] OMG. Action Language for Foundational UML (Alf), Concrete Syntax for a UML Action Language, FTF –Beta 1. Technical report, 2010.




Back to SLR page