NDLI: Composite model-checking: verification with type-specific symbolic representations

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

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 25

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 24

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 23

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 22

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 21

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 20

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 19

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 18

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 17

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 16

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 15

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 14

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 13

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 12

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 11

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 10

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 9

Composite model-checking: verification with type-specific symbolic representations

Using shape analysis to reduce finite-state models of concurrent Java programs

Abstracting dependencies between software configuration items

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 8

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 7

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 6

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 5

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 4

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 3

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 2

ACM Transactions on Software Engineering and Methodology (TOSEM) : Volume 1

Composite model-checking: verification with type-specific symbolic representations

Content Provider	ACM Digital Library
Author	League, Christopher Gerber, Richard Bultan, Tevfik
Copyright Year	2000
Abstract	There has been a surge of progress in automated verification methods based on state exploration. In areas like hardware design, these technologies are rapidly augmenting key phases of testing and validation. To date, one of the most successful of these methods has been symbolic model-checking, in which large finite-state machines are encoded into compact data structures such as Binary Decision Diagrams (BDDs), and are then checked for safety and liveness properties. However, these techniques have not realized the same success on software systems. One limitation is their inability to deal with infinite-state programs, even those with a single unbounded integer. A second problem is that of finding efficient representations for various variable types. We recently proposed a model-checker for integer-based systems that uses arithmetic constraints as the underlying state representation. While this approach easily verified some subtle, infinite-state concurrency problems, it proved inefficient in its treatment of boolean and (unordered) enumerated types—which are not efficiently representable using arithmetic constraints. In this article we present a new technique that combines the strengths of both BDD and arithmetic constraint representations. Our composite model merges multiple type-specific symbolic representations in a single model-checker. A system's transitions and fixpoint computations are encoded using both BDD (for boolean and enumerated types) and arithmetic constraints (for integers) representations, where the choice depends on the variable types. Our composite model-checking strategy can be extended to other symbolic representations provided that they support operations such as intersection, union, complement, equivalence checking, and relational image computation. We also present conservative approximation techniques for composite representations to address the undecidability of model-checking on infinite-state systems. We demonstrate the effectiveness of our approach by analyzing two example software specifications which include a mixture of booleans, integers, and enumerated types. One of them is a requirements specification for the control software of a nuclear reactor's cooling system, and the other one is a protocol specification.
Starting Page	3
Ending Page	50
Page Count	48
File Format	PDF
ISSN	1049331X
e-ISSN	15577392
DOI	10.1145/332740.332746
Volume Number	9
Issue Number	1
Journal	ACM Transactions on Software Engineering and Methodology (TOSEM)
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2000-01-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Presburger arithmetic Binary decision diagrams Symbolic model-checking
Content Type	Text
Resource Type	Article
Subject	Software

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

Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results

Composite Model Checking: Verification with Type-Specific Symbolic Representations (2000)

Model checking sequential software programs via mixed symbolic analysis

A symbolic manipulator for automated verification of reactive systems with heterogeneous data types

Probabilistic symbolic model checking with PRISM: a hybrid approach

Symbolic model checking for event-driven real-time systems

Hybrid decision diagrams

Optimizing symbolic model checking for statecharts

Improving efficiency of symbolic model checking for state-based system requirements

Composite model-checking: verification with type-specific symbolic representations

Similar Documents

Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results

Composite Model Checking: Verification with Type-Specific Symbolic Representations (2000)

Model checking sequential software programs via mixed symbolic analysis

A symbolic manipulator for automated verification of reactive systems with heterogeneous data types

Probabilistic symbolic model checking with PRISM: a hybrid approach

Symbolic model checking for event-driven real-time systems

Hybrid decision diagrams

Optimizing symbolic model checking for statecharts

Improving efficiency of symbolic model checking for state-based system requirements

Composite model-checking: verification with type-specific symbolic representations