Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-34281-3_28
Title: Symbolic model-checking of stateful timed CSP using BDD and digitization
Authors: Nguyen, T.K.
Sun, J.
Liu, Y. 
Dong, J.S. 
Issue Date: 2012
Source: Nguyen, T.K.,Sun, J.,Liu, Y.,Dong, J.S. (2012). Symbolic model-checking of stateful timed CSP using BDD and digitization. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 7635 LNCS : 398-413. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-34281-3_28
Abstract: Stateful Timed CSP has been recently proposed to model (and verify) hierarchical real-time systems. It is an expressive modeling language which combines data structure/operations, complicated control flows (modeled using compositional process operators adopted from Timed CSP), and real-time requirements like deadline and within. It has been shown that Stateful Timed CSP is equivalent to closed timed automata with silent transitions, which implies that the timing constraints of Stateful Timed CSP can be captured using explicit tick events, through digitization. In order to tackle the state space explosion problem, we develop a BDD-based symbolic model checking approach to verify Stateful Timed CSP models. Due to the rich language features, BDD-based system encoding and verification is highly nontrivial. In this work, we show how to systematically encode Stateful Timed CSP models in BDD. Our approach consists of two steps. The first step is to identify maximum primitive components of a given system and then generate finite state machines (FSMs) from them, applying a set of symbolic firing rules. These FSMs are then encoded in the standard way. The second step is to compose the encoded components using a set of BDD-based compositional functions. The proposed method has been implemented in the PAT model checker. It supports properties like reachability, linear temporal logic, etc. The effectiveness of our technique is evaluated with benchmark systems. © 2012 Springer-Verlag.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/43177
ISBN: 9783642342806
ISSN: 03029743
DOI: 10.1007/978-3-642-34281-3_28
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

3
checked on Dec 13, 2017

Page view(s)

46
checked on Dec 9, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.