Nevertrace Claims for Model Checking

In this paper, we propose the nevertrace claim, which is a new construct for specifying the correctness properties that either finite or infinite execution traces (i.e., sequences of transitions) that should never occur. In semantics, it is neither similar to never claim and trace assertion, nor a simple combination of them. Furthermore, the theoretical foundation for checking nevertrace claims, namely the AsynchronousComposition B¨uchi Automaton Control System (AC-BAC System), is proposed. The major contributions of the nevertrace claim include: a powerful construct for formalizing properties related to transitions and their labels, and a way for reducing the state space in design stage.

• Type: Journal
• Year: 2010
• Where: SPIN
• Authors: Zhe Chen, Gilles Motet
• Keywords: B¨uchi Automaton Control, Execution Traces, Nevertrace Claim, SPIN 2010, Theoretical Computer Science