Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

7

SNPD
2004

favoriteEmaildiscussreport

123views Artificial Intelligence» more SNPD 2004»

Addressing State Explosion in Behavior Protocol Verification

13 years 5 months ago

Addressing State Explosion in Behavior Protocol Verification

Download d3s.mff.cuni.cz

A typical problem formal verification faces is the size of the model of a system being verified. Even for a small system, the state space of the model tends to grow exponentially (state explosion). In this paper, we present a new representation of state spaces suitable for implementing operations upon behavior protocols of software components [1]. The proposed representation is linear in length of the source behavior protocol. By trading space for time, it allows handling behavior protocols of "practical size". As a proof of concept, a verification tool for behavior protocols is discussed.

Martin Mach, Frantisek Plasil

Real-time Traffic

Behavior Protocols | Problem Formal Verification | SNPD 2004 | SNPD 2007 | State Spaces |

claim paper

Related Content

» Compositional Verification of a Third Generation Mobile Communication Protocol

» On Accurate Automatic Verification of PublishSubscribe Architectures

» Partial Verification of Software Components Heuristics for Environment Construction

» AssumeGuarantee Verification of Source Code with DesignLevel Assumptions

» State Space Reduction Techniques for Component Interfaces

» A Partitioning Methodology for BDDBased Verification

» The state of the email address

» Parameterized Verification of Transactional Memories

» Lightweight object specification with typestates

Post Info
More Details (n/a)

Added	31 Oct 2010
Updated	31 Oct 2010
Type	Conference
Year	2004
Where	SNPD
Authors	Martin Mach, Frantisek Plasil

Comments (0)