NDLI: Using partial-order methods in the formal validation of industrial concurrent programs

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

Test and analysis of software architectures

An efficient state space generation for analysis of real-time systems

An incremental approach to structural testing of concurrent software

Improving the accuracy of Petri net-based analysis of concurrent programs

Generating functional test cases in-the-large for time-critical systems from logic-based specifications

Daistish: systematic algebraic testing for OO programs in the presence of side-effects

Structural specification-based testing with ADL

Issues in the full scale use of formal methods for automated testing

Experiences and lessons from the analysis of TCAS II

Predicting dependability by testing

Using perturbation analysis to measure variation in the information content of test sets

Linear and structural event sequence analysis

Separate computation of alias information for reuse

Critical slicing for software fault localization

The path-wise approach to data flow testing with pointer variables

Unconstrained duals and their use in achieving all-uses coverage

Software error analysis: a real case study involving real faults and mutations

Generation of multi-formalism state-space analysis tools

Beyond traditional program slicing

An approach to verification and validation of a reliable multicasting protocol

A semantic model of program faults

Towards a structural load testing tool

Automated test data generation for programs with procedures

Reachability analysis of feature interactions: a progress report

Compositional verification by model checking for counter-examples

Elements of style: analyzing a software design feature with a counterexample detector

Constructing abstract models of concurrent real-time software

Using partial-order methods in the formal validation of industrial concurrent programs

Formal specification and verification of the kernel functional unit of the OSI session layer protocol and service using CCS

A logic-model semantics for SCR software requirements

Why state-of-the-art is not state-of-the-practice (panel)

Using partial-order methods in the formal validation of industrial concurrent programs

Content Provider	ACM Digital Library
Author	Peled, Doron Godefroid, Patrice Staskauskas, Mark
Abstract	We have developed a formal validation tool that has been used on several projects that are developing software for AT&T's $5ESS^{™}$ telephone switching system. The tool uses Holzmann's supertrace algorithm to check for errors such as deadlock and livelock in networks of communicating processes. The validator invariably finds subtle errors that were missed during thorough simulation and testing; however, the brute-force search it performs can result in extremely long running times, which can be frustrating to users. Recently, a number of researchers have been investigating techniques known as partial-order methods that can significantly reduce the running time of formal validation by avoiding redundant exploration of execution scenarios. In this paper, we describe the design of a partial-order algorithm for our validation tool and discuss its effectiveness. We show that a careful compile-time static analysis of process communication behavior yields information that can be used during validation to dramatically improve its performance. We demonstrate the effectiveness of our partial-order algorithm by presenting the results of experiments with actual industrial examples drawn from a variety of $5ESS^{™}$ application domains, including call processing, signalling, and switch maintenance.
Starting Page	261
Ending Page	269
Page Count	9
File Format	PDF
ISBN	0897917871
DOI	10.1145/229000.226324
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1996-05-01
Publisher Place	New York
Access Restriction	Subscribed
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

Using partial-order methods in the formal validation of industrial concurrent programs

Using partial-order methods in the formal validation of industrial concurrent programs

Partial order reduction on concurrent probabilistic programs

Efficient verification using generalized partial order analysis

Reverse engineering concurrent programs using formal modelling and analysis

Semantics driven dynamic partial-order reduction of MPI-based parallel programs

Testing concurrent programs: a formal evaluation of coverage criteria

Reverse engineering concurrent programs using formal modelling and analysis

Towards a formal framework for developing concurrent programs: Modeling dynamic behavior

Using partial-order methods in the formal validation of industrial concurrent programs

Similar Documents

Using partial-order methods in the formal validation of industrial concurrent programs

Using partial-order methods in the formal validation of industrial concurrent programs

Partial order reduction on concurrent probabilistic programs

Efficient verification using generalized partial order analysis

Reverse engineering concurrent programs using formal modelling and analysis

Semantics driven dynamic partial-order reduction of MPI-based parallel programs

Testing concurrent programs: a formal evaluation of coverage criteria

Reverse engineering concurrent programs using formal modelling and analysis

Towards a formal framework for developing concurrent programs: Modeling dynamic behavior

Using partial-order methods in the formal validation of industrial concurrent programs