This report is about Partial Order Reduction for PINS. There are plenty of diverse tools utilized for formal verification of hardware and software. For both the scientific purpose of reviewing methods and tools, plus the industrial use cases that might need combining different methods, a standard interface for state space generation would enhance the usefulness of model checkers. One such interface is the partitioned next state interface (PINS) which happens to be an abstraction layer between the model and the algorithms utilized for state space generation. Within this report we create a partial order algorithm which works employing a minimal extension of the PINS interface, and is also developed in a modular fashion……
Contents
1 Introduction
1.1 Background
1.2 Related work
1.3 Research questions
1.4 Summary of contributions
2 The PINS architecture
2.1 The Partitioned Next State Interface
2.1.1 The PINS front-end interface
2.1.2 PINS back-ends and algorithms
2.1.3 PINS wrappers
3 Partial Order Reduction for Deadlocks
3.1 Theory of partial order reduction
3.1.1 Semantic and structural transitions
3.1.2 Independence
3.1.3 Equivalence classes
3.1.4 Reduction function
3.1.5 Persistent set
3.2 A modular PINS POR wrapper
3.3 Conflicting transitions
3.3.1 Theory and algorithm
3.3.2 Modifications to PINS
3.3.3 Evaluation
3.4 Stubborn set
3.4.1 Theory
3.4.2 The algorithm
3.4.3 Modifications to PINS
3.4.4 Evaluation
3.5 Better necessary enabling sets
3.5.1 Modifications to the algorithm
3.5.2 Modifications to PINS
3.5.3 Evaluation
3.6 Necessary disabling sets
3.6.1 The algorithm
3.6.2 Modifications to PINS
3.6.3 Evaluation
3.6.4 Future optimizations
3.7 Partial order reduction with non-deterministic transitions
3.8 Partial order reduction v.s. symbolic reachability
3.9 Discussion and future work
3.10 Conclusion
iiiCONTENTS CONTENTS
4 Partial Order Reduction for LTL
4.1 Linear Temporal Logic (LTL)
4.1.1 LTL semantics
4.1.2 On the fly LTL model checking
4.2 The ignoring problem for partial order reduction
4.2.1 Preserving safety properties
4.2.2 Preserving liveness and LTL properties
4.3 Safety and liveness proviso
4.3.1 The stack/queue proviso
4.3.2 The closed set proviso
4.3.3 The color proviso
4.4 A PINS LTL wrapper
4.5 Observations
4.6 Implementation
4.6.1 General State Expanding Algorithms
4.6.2 Couvreur
4.6.3 Combining POR with LTL
4.6.4 Implementing the proviso
4.6.5 The closed set proviso
4.6.6 The stack proviso
4.6.7 The color proviso
4.7 Evaluation
4.8 Discussion and future work
4.9 Conclusion
Bibliography
Source: University of Twente
Download URL 2: Visit Now