NDLI: Automatic generation of symbolic model for parameterized synchronous systems

Content Provider	Springer Nature Link
Author	Xu, Wei Wen
Copyright Year	2004
Abstract	With the purpose of making the verification of parameterized system more general and easier, in this paper, a new and intuitive language PSL (Parameterized-system Specification Language) is proposed to specify a class of parameterized synchronous systems. From a PSL script, an automatic method is proposed to generate a constraint-based symbolic model. The model can concisely symbolically represent the collections of global states by counting the number of processes in a given state. Moreover, a theorem has been proved that there is a simulation relation between the original system and its symbolic model. Since the abstract and symbolic techniques are exploited in the symbolic model, state-explosion problem in traditional verification methods is efficiently avoided. Based on the proposed symbolic model, a reachability analysis procedure is implemented using ANSI C++ on UNIX platform. Thus, a complete tool for verifying the parameterized synchronous systems is obtained and tested for some cases. The experimental results show that the method is satisfactory.
Starting Page	812
Ending Page	819
Page Count	8
File Format	PDF
ISSN	10009000
Journal	Journal of Computer Science and Technology
Volume Number	19
Issue Number	6
e-ISSN	18604749
Language	English
Publisher	Science Press
Publisher Date	2008-10-11
Publisher Place	Beijing
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	parameterized system formal verification symbolic representation Computer Science Software Engineering Theory of Computation Data Structures, Cryptology and Information Theory Artificial Intelligence (incl. Robotics) Information Systems Applications (incl. Internet)
Content Type	Text
Resource Type	Article
Subject	Theoretical Computer Science Computational Theory and Mathematics Computer Science Applications Software Hardware and Architecture

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 Library 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

On Unknown Small Subsets and Implicit Measures: New Techniques for Parameterized Algorithms

Formal Verification of Temporal Properties for Reduced Overhead in Grid Scientific Workflows

Cooperative Software Testing and Analysis: Advances and Challenges

Structure-Based Deadlock Checking of Asynchronous Circuits

A Parallel Interval Computation Model for Global Optimization with Automatic Load Balancing

A Survey of Commonsense Knowledge Acquisition

Introduction to the Six Leading Editors

Parameterized Computation and Complexity: A New Approach Dealing with NP-Hardness

Software-Defined Cluster

Automatic generation of symbolic model for parameterized synchronous systems

Similar Documents

On Unknown Small Subsets and Implicit Measures: New Techniques for Parameterized Algorithms

Formal Verification of Temporal Properties for Reduced Overhead in Grid Scientific Workflows

Cooperative Software Testing and Analysis: Advances and Challenges

Structure-Based Deadlock Checking of Asynchronous Circuits

A Parallel Interval Computation Model for Global Optimization with Automatic Load Balancing

A Survey of Commonsense Knowledge Acquisition

Introduction to the Six Leading Editors

Parameterized Computation and Complexity: A New Approach Dealing with NP-Hardness

Software-Defined Cluster

Automatic generation of symbolic model for parameterized synchronous systems