NDLI: A formal verification framework for Bluespec System Verilog

Content Provider	IEEE Xplore Digital Library
Author	Ouchani, Samir Mohamed, Otmane Ait Debbabi, Mourad
Copyright Year	2013
Description	Author affiliation: Hardware Verification Group (HVG), Concordia University, Montreal, Quebec, Canada H3G 1M8 (Mohamed, Otmane Ait) \|\| Computer Security Laboratory (CSL), Concordia University, Montreal, Quebec, Canada H3G 1M8 (Ouchani, Samir; Debbabi, Mourad)
Abstract	In systems engineering and hardware design, SysML activity diagrams are widely used for modeling and analyzing complex systems. In addition, Bluespec System Verilog gains recently more popularity in hardware synthesis. This paper proposes an efficient formal verification framework to verify the correctness of the systems' design. First, we verify a system modeled by SysML activity diagrams using PRISM probabilistic symbolic model checker. Then, we present an efficient algorithm that transforms the SysML activity diagrams to an equivalent BlueSpec code. To express easily the proposed algorithm, we formalize both SysML activity diagrams and BlueSpec language. Finally, we demonstrate the effectiveness of our approach by presenting a case study.
Starting Page	1
Ending Page	7
File Size	6983003
Page Count	7
File Format	PDF
ISBN	9782953050486
ISSN	16369874
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2013-09-24
Publisher Place	France
Access Restriction	Subscribed
Rights Holder	European Electronic Chips & Systems design Initiative - ECSI
Subject Keyword	Concurrent computing SysML Activity Diagram PRISM Model-Checker Unified modeling language Syntactics Probabilistic logic BlueSpec System Verilog Hardware Modeling Hardware design languages PCTL
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Libarray of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

A probabilistic verification framework of SysML activity diagrams

Formal verification of internal block diagram of SysML for modeling real-time system

Formal Specification and Probabilistic Verification of SysML Activity Diagrams

A Security Risk Assessment Framework for SysML Activity Diagrams

A probabilistic and timed verification approach of SysML state machine diagram

Improving design quality by automatic verification of activity diagram syntax

Formal Verification of Time Constrains SysML Internal Block Diagram Using PRISM

On the Meaning of SysML Activity Diagrams

Translation UML diagrams into Verilog

A formal verification framework for Bluespec System Verilog

Similar Documents

A probabilistic verification framework of SysML activity diagrams

Formal verification of internal block diagram of SysML for modeling real-time system

Formal Specification and Probabilistic Verification of SysML Activity Diagrams

A Security Risk Assessment Framework for SysML Activity Diagrams

A probabilistic and timed verification approach of SysML state machine diagram

Improving design quality by automatic verification of activity diagram syntax

Formal Verification of Time Constrains SysML Internal Block Diagram Using PRISM

On the Meaning of SysML Activity Diagrams

Translation UML diagrams into Verilog

A formal verification framework for Bluespec System Verilog