NDLI: Sizing and verification of communication buffers for communicating processes

Content Provider	IEEE Xplore Digital Library
Author	Kolks, T. Lin, B. de Man, H.
Copyright Year	1993
Description	Author affiliation: IMEC, Leuven, Belgium (Kolks, T.)
Abstract	A method is presented for minimal sizing and verification of communication buffers in an environment of communicating concurrent processes. Methods described in the literature based on lifetime analysis techniques are mainly suited for sizing buffers in a network of processes with non-conditional interactions. We consider a more general problem where the execution of each process inherently depends on complex interactions with other processes as well as its internal conditional behavior and propose the use of implicit state enumeration techniques to solve buffer sizing and verification for this case. A model of the network of processes and buffers is introduced that is transformed into a network of finite state machines by modeling communicating buffers as counters. The transformed network forms a finite state space model on which implicit state space exploration algorithms are applied. The model allows us to handle the buffer sizing and verification problems with processes that operate on different, but related clocks. To reduce the complexity of the state space, abstraction techniques can be used to produce simplified versions of finite state machines that hide away unnecessarily detailed information. The feasibility of the proposed approach is demonstrated by a practical example.
Starting Page	660
Ending Page	664
File Size	602213
Page Count	5
File Format	PDF
ISBN	0818644907
DOI	10.1109/ICCAD.1993.580157
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	1993-11-07
Publisher Place	USA
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	State-space methods Buffer storage Timing Automata Counting circuits Space exploration Communication system control Clocks Hardware Embedded software
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 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

Sizing of communication buffers for communicating signal processes

Verification and synthesis of counters based on symbolic techniques

Sizing and verification of communication buffers for communicating processes

An implementation of three algorithms for timing verification based on automata emptiness

Communication synthesis for distributed embedded systems

Scheduling constraint generation for communicating processes

Optimizing finite state machines for system-on-chip communication

Time-Predictable Task Preemption for Real-Time Systems with Direct-Mapped Instruction Cache

Design of WBDSO control circuit with state machine

Sizing and verification of communication buffers for communicating processes

Similar Documents

Sizing of communication buffers for communicating signal processes

Verification and synthesis of counters based on symbolic techniques

Sizing and verification of communication buffers for communicating processes

An implementation of three algorithms for timing verification based on automata emptiness

Communication synthesis for distributed embedded systems

Scheduling constraint generation for communicating processes

Optimizing finite state machines for system-on-chip communication

Time-Predictable Task Preemption for Real-Time Systems with Direct-Mapped Instruction Cache

Design of WBDSO control circuit with state machine

Sizing and verification of communication buffers for communicating processes