Model-based design verification for embedded systems through SVOCL: an OCL extension for System Verilog

被引:36
作者
Anwar, Muhammad Waseem [1 ]
Rashid, Muhammad [2 ]
Azam, Farooque [1 ]
Kashif, Muhammad [3 ]
机构
[1] NUST, Dept Comp Engn, CEME, H-12, Islamabad, Pakistan
[2] Umm Al Qura Univ, Comp Engn Dept, Coll Comp & Informat Syst, Mecca, Saudi Arabia
[3] Umm Al Qura Univ, Sci & Technol Unit, Mecca, Saudi Arabia
关键词
MBSE; SystemVerilog assertions; OCL extension; Embedded systems; SVOCL;
D O I
10.1007/s10617-017-9182-z
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
Model Based System Engineering (MBSE) is a renowned approach in the context of embedded systems development. It is frequently used to deal with the structural and behavioral aspects of system design. However, the verification of system design is generally performed in isolation. It is particularly true in the context of assertion based verification. Consequently, there is a huge gap between system design and its verification that seriously effects the productivity and time-to market objectives. Therefore, in this research, we target to reduce this gap by exploiting the features of MBSE and SystemVerilog assertions (SVA's). This article introduces a novel MBSE approach to model the design verification aspects of embedded systems, along with the system design (structural and behavioral aspects). We propose SystemVerilog in Object Constraint Language (SVOCL), an OCL temporal extension for SystemVerilog, to represent the design verification requirements by means of SVA's. As a part of research, SVOCL transformation engine has been developed to generate SVA's code in order to automate the design verification of embedded systems. The application of SVOCL has been validated through four case studies.
引用
收藏
页码:1 / 36
页数:36
相关论文
共 38 条
  • [1] Andrade E, 2009, THIRD INTERNATIONAL CONFERENCE ON DIGITAL SOCIETY: ICDS 2009, PROCEEDINGS, P266, DOI 10.1109/ICDS.2009.19
  • [2] [Anonymous], 2015, Formal Specification Level-Concepts, Methods, and Algorithms
  • [3] Translation UML diagrams into Verilog
    Bazydlo, Grzegorz
    Adamski, Marian
    Stefanowicz, Lukasz
    [J]. 2014 7TH INTERNATIONAL CONFERENCE ON HUMAN SYSTEM INTERACTIONS (HSI), 2014, : 267 - 271
  • [4] Timed automata: Semantics, algorithms and tools
    Bengtsson, J
    Yi, W
    [J]. LECTURES ON CONCURRENCY AND PETRI NETS: ADVANCES IN PETRI NETS, 2004, 3098 : 87 - 124
  • [5] Berrani S, 2013, 2013 11TH INTERNATIONAL SYMPOSIUM ON PROGRAMMING AND SYSTEMS (ISPS), P177, DOI 10.1109/ISPS.2013.6581484
  • [6] Besnard L, 2010, CORRECT BY CONSTRUCT
  • [7] Bill R, 2014, LECT NOTES COMPUT SC, V8706, P221, DOI 10.1007/978-3-319-11245-9_13
  • [8] Bousse E., 2012, P WORKSH MOD DRIV EN, P11
  • [9] Bradfield J, 2002, LECT NOTES COMPUT SC, V2306, P203
  • [10] Cengarle M. V., 2002, FME 2002: Formal Methods-Getting IT Right. International Symposium of Formal Methods Europe (Lecture Notes in Computer Science Volume 2391), P390