NDLI: Behavioral automata composition for automatic topology independent verification of parameterized systems

Please wait, while we are loading the content...

Asserting and checking determinism for multithreaded programs

Darwin: an approach for debugging evolving programs

The massification and webification of systems' modeling and simulation with virtual worlds

Backward-compatible constant-time exception-protected memory

Cross-project defect prediction: a large scale experiment on data vs. domain vs. process

Qos-driven runtime adaptation of service oriented architectures

Refactoring for reentrancy

Api hyperlinking via structural overlap

Insights from expert software design practice

Fitting the pieces together: a machine-checked model of safe composition

Debugging debugging: acm sigsoft impact paper award keynote

Facilitating software refactoring with appropriate resolution order of bad smells

Verification and performance evaluation of aadl models

Software architecture: many faces, many places, yet a central discipline

Synthesizing partial component-level behavior models from system specifications

Probabilistic environments in the quantitative analysis of (non-probabilistic) behaviour models

Engineering search computing applications: vision and challenges

DebugAdvisor: a recommender system for debugging

The challenge of pervasive software to the conventional wisdom of software engineering

Static data race detection for concurrent programs with asynchronous calls

Capturing propagation of infected program states

Automated security testing of web widget interactions

On the relationship between process maturity and geographic distribution: an empirical analysis of their impact on software quality

Automatic synthesis of behavior protocols for composable web-services

Monitoring probabilistic properties

Learning from examples to improve code completion systems

Ensuring interoperable service-oriented systems through engineered self-healing

Software change dynamics: evidence from 35 java projects

Reo2MC: a tool chain for performance analysis of coordination models

Supporting automatic model inconsistency fixing

Automatic steering of behavioral model inference

Graph-based mining of multiple object usage patterns

IQ routes and HD traffic: technology insights about tomtom's time-dynamic navigation concept

Symbolic pruning of concurrent program executions

Saturation-based testing of concurrent programs

Improving bug triage with bug tossing graphs

Data flow testing of service choreography

MSeqGen: object-oriented unit-test generation via mining source code

Improving slice accuracy by compression of data and control flow paths

Practical framework constraints

Smart views for analyzing problem reports: tool demo

Behavioral automata composition for automatic topology independent verification of parameterized systems

Sireum/Topi LDP: a lightweight semi-decision procedure for optimizing symbolic execution-based analyses

Fair and balanced?: bias in bug-fix datasets

Whitening SOA testing

Evaluating recovery aware components for grid reliability

SCA: a semantic conflict analyzer for parallel changes

Towards accurate probabilistic models using state refinement

Test case comparison and clustering using program profiles and static execution

ReCrashJ: a tool for capturing and reproducing program crashes in deployed applications

Javalanche: efficient mutation testing for Java

ConcernMorph: metrics-based detection of crosscutting patterns

Srijan: a graphical toolkit for sensor network macroprogramming

Behavioral automata composition for automatic topology independent verification of parameterized systems

Content Provider	ACM Digital Library
Author	Basu, Samik Rajan, Hridesh Hanna, Youssef
Abstract	Verifying correctness properties of parameterized systems is a long-standing problem. The challenge lies in the lack of guarantee that the property is satisfied for all instances of the parameterized system. Existing work on addressing this challenge aims to reduce this problem to checking the properties on smaller systems with a bound on the parameter referred to as the cut-off. A property satisfied on the system with the cut-off ensures that it is satisfied for systems with any larger parameter. The major problem with these techniques is that they only work for certain classes of systems with specific communication topology such as ring topology, thus leaving other interesting classes of systems unverified. We contribute an automated technique for finding the cut-off of the parameterized system that works for systems defined with any topology. Given the specification and the topology of the system, our technique is able to automatically generate the cut-off specific to this system. We prove the soundness of our technique and demonstrate its effectiveness and practicality by applying it to several canonical examples where in some cases, our technique obtains smaller cut-off values than those presented in the existing literature.
Starting Page	325
Ending Page	334
Page Count	10
File Format	PDF
ISBN	9781605580012
DOI	10.1145/1595696.1595758
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2009-08-24
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Parameterized model checking
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

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