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


We have selected the appropriate design techniques, tools and trends for multiple phases of the project through two different Systematic Literature Reviews (SLRs). Based on the findings, three different avenues have been taken for the development of a unified model that integrates structural aspects, behavioral aspects as well as the constraints for early design verification. The unified model is automatically transformed into the target SystemVerilog RTL code as well as SystemVerilog assertions for design verification. The students have been trained to the ideas of Model Based System Engineering (MBSE) through innovative ideas.

Description of Progress:

We have divided the progress into three parts: (1) evaluation of state-of-the-art (2) development of a model-based design and verification methodology (3) enhancement of educational infrastructure by incorporating the benefits of MBSE

1. Evaluation of State-of-the-art:

The first SLR (termed as SLR-1 in this project), performed during the first year of the project, focused on the identification and classification of the recent research practices in academia as well as in industry, pertaining to the embedded systems development through MBSE approach. Details of SLR-1 can be found Here

The second SLR (termed as SLR-2 in this project), performed during the second year of the project, focused on the exploration of techniques, tools and trends for early design verification of UML-based models. Details of SLR-2 can be found Here

Difference between SLR-1 and SLR-2:

1. While the SLR-1 enables to obtain a general overview of the entire MBSE domain for embedded systems development, the SLR-2 provides more specific results related to the early design verification.

2. As SLR-1 provides a broader overview of MBSE for embedded systems, any research work that deals with the modeling, either UML-based or domain-specific, is included. Similarly, it is not essential for the selected research works to include a property specification and/or verification technique.

3. On the other hand, SLR-2 is specific to early design verification techniques, tools and trends such that the selected research works must fulfill three major conditions (a) UML-based approach only (b) properties / constraint specification must be used, (c) static and / or dynamic verification must be performed

4. Consequently, selected research works (54) in SLR-2 are 80% different from the selected research works of SLR-1 (61). To summarize, the results of both SLR’s are significantly different form each other due to the dissimilarities of research context and objectives

2. Development of a model-based design and verification methodology:

Based on the findings of SLRs, three different avenues have been taken to develop a model-based development methodology for early design verification of embedded systems: (a) Expressing System Verilog Assertions (SVAs) in the UML-based models through an extension of OCL (Object Constraint Language), (2) Expressing SVAs in the UML-based models through CCSL (Clock Constraint Specification Language) and (3) Incorporating the concepts of Service-Oriented Computing in the context of MBSE.

2.1. Expressing SVAs in UML based models through OCL:

1. The detailed analysis is performed to investigate the major constructs of OCL and System Verilog so that the logical mapping of concepts can be performed. The analysis results have been published in: “Exploring the platform for expressing SystemVerilog assertions in model based system engineering”, Information Science and Applications (ICISA), Lecture Notes in Electrical Engineering, Vol. 376, Pages 533-544, 2016.

2. It has been analyzed that all the OCL constructs cannot be mapped directly to System Verilog constructs. Therefore, it is required to extend the OCL in order to support the basic constructs of System Verilog. An extension of OCL is developed, named as SVOCL (SystemVerilog in Object Constraint Language), to specify the embedded systems assertions. The initial results have been published in: “Expressing embedded systems verification aspects at higher abstraction level - SystemVerilog in Object Constraint Language (SVOCL)”, Accepted for publication in 10th IEEE SysCon, 2016.

3. While the SVOCL only deals with the representation of verification constraints at higher abstraction level and generation of SystemVerilog Assertions (SVAs), the representation of structural and behavioral aspects at higher abstraction level is equally important such that the low level SystemVerilog RTL code can be automatically generated.

4. The details can be found Here

2.2. Expressing SVAs in UML based models through CCSL:

1. The first attempt in this regard is to use SysML and the UML profile for MARTE to model the system structure. Design verification properties are embedded to structural models using the SysML parametric diagrams along with the Clock Constraint Specification Language (CCSL). The results have been accepted for publication in “Combining SysML and Marte/CCSL to Model Complex Electronic Systems”, International Conference on Information Systems Engineering, 2016.

2. Next, we advocate the use of CCSL to express the safety properties of UML/MARTE/SysML models and presents an automatic transformation of selected CCSL operators into equivalent SystemVerilog assertions. This contribution reduces the gap between the abstract CCSL specifications modeling causality relations and the RTL-based SystemVerilog assertions, hence achieving early design validation. The results have been accepted for publication in: “Generation of SystemVerilog Observers from SysML and Marte/CCSL”, 19th IEEE International Symposium on Real-Time Computing, 2016.

3. The next step is to capture the behavioral intent of the design by proposing graphical temporal patterns. Consequently, the proposed approach advocates a Formal Specification Level as an intermediate level from natural-language requirements to code synthesis. The results have been accepted for publication in: “Natural Interpretation of UML/MARTE Diagrams for System Requirements Specification”, 11th IEEE International Symposium on Industrial Embedded Systems, 2016.

4. Based on the aforementioned results, an end-to-end framework is proposed to specify the textual requirement graphically in standard modeling artifacts like UML and MARTE in the form of temporal patterns. The underlying formal semantics of these graphical models allow to eliminate ambiguity in speci?cations and automatic design veri?cation at di?erent abstraction levels. The semantics of these temporal operators are presented formally as state automatons and a comparison is made to the existing CCSL relational operators. To reap the bene?ts of model driven engineering, a software plugin TemPAC is presented as a part of the framework to transform the graphical patterns into CCSL and Verilog-based observers. The details can be found Here

2.3. Incorporating the concepts of Service-oriented Computing in the context of MBSE:

1. Service-Oriented Computing (SOC) has been used previously for embedded systems, at the implementation level, in an ad-hoc manner without any focus on system analysis and design. Consequently, a Service-Oriented Analysis and Design Approach (SOADA) for embedded systems is presented. The applicability of analysis and design phases is demonstrated through the Smart Home case study.

2. The SOADA approach is further extended to a unified mechanism for design and verification of embedded systems. For the modeling of structural and behavioral aspects, the work builds on the service-based meta-model for embedded system development and its implementation in terms of a UML profile.

3. Enhancement of educational infrastructure by incorporating the benefits of MBSE:

1. While the MBSE is becoming a standard in electronic design automation and the design of computing systems, we incorporated the concepts of MBSE (such as abstraction, separation of concerns, Y-chart methodology) into curriculum design. In our approach, a curriculum serves as a system to merge all the technical evolutions in a particular field into a unified course of study, forming an abstract but structured development cycle that proceeds from the concept to the final design experience. The results have been published in: “Holistic Development of Computer Engineering Curricula Using Y-Chart Methodology” Muhammad Rashid and Imran A. Tasadduq, IEEE Transactions on Education, Vol. 57, No. 3, pp. 193–200, August 2014.

2. Next step in this direction is to integrate the coherent delivery of concepts with problem-based learning. Coherent learning consists of integrated delivery of core concepts. During the problem-based learning, students worked in teams to identify and solve a problem relevant to the core contents. The results have been published in: “System Level Approach for Computer Engineering Education” Muhammad Rashid, International Journal of Engineering Education Vol. 31, No. 1(A), pp. 141–153, 2015.

3. An innovative model based system engineering course at undergraduate level has been designed and taught during Spring 2016. Students have been trained through lectures and laboratory practices. Evaluation results will be shared to the scientific community.