An Efficient Explicit-time Description Method for Timed Model Checking
Timed model checking, the method to formally verify real-time systems, is attracting increasing attention from both the model checking community and the real-time community. Explicit-time description methods verify real-time systems using general model constructs found in standard un-timed model che...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2009-12-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/0912.2553v1 |
| _version_ | 1818233282421063680 |
|---|---|
| author | Hao Wang Wendy MacCaull |
| author_facet | Hao Wang Wendy MacCaull |
| author_sort | Hao Wang |
| collection | DOAJ |
| description | Timed model checking, the method to formally verify real-time systems, is attracting increasing attention from both the model checking community and the real-time community. Explicit-time description methods verify real-time systems using general model constructs found in standard un-timed model checkers. Lamport proposed an explicit-time description method using a clock-ticking process (Tick) to simulate the passage of time together with a group of global variables to model time requirements. Two methods, the Sync-based Explicit-time Description Method using rendezvous synchronization steps and the Semaphore-based Explicit-time Description Method using only one global variable were proposed; they both achieve better modularity than Lamport's method in modeling the real-time systems. In contrast to timed automata based model checkers like UPPAAL, explicit-time description methods can access and store the current time instant for future calculations necessary for many real-time systems, especially those with pre-emptive scheduling. However, the Tick process in the above three methods increments the time by one unit in each tick; the state spaces therefore grow relatively fast as the time parameters increase, a problem when the system's time period is relatively long. In this paper, we propose a more efficient method which enables the Tick process to leap multiple time units in one tick. Preliminary experimental results in a high performance computing environment show that this new method significantly reduces the state space and improves both the time and memory efficiency. |
| first_indexed | 2024-12-12T11:19:42Z |
| format | Article |
| id | doaj.art-71941af1d5ce4d7996fe26c50096577c |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-12T11:19:42Z |
| publishDate | 2009-12-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-71941af1d5ce4d7996fe26c50096577c2022-12-22T00:26:03ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802009-12-0114Proc. PDMC 2009779110.4204/EPTCS.14.6An Efficient Explicit-time Description Method for Timed Model CheckingHao WangWendy MacCaullTimed model checking, the method to formally verify real-time systems, is attracting increasing attention from both the model checking community and the real-time community. Explicit-time description methods verify real-time systems using general model constructs found in standard un-timed model checkers. Lamport proposed an explicit-time description method using a clock-ticking process (Tick) to simulate the passage of time together with a group of global variables to model time requirements. Two methods, the Sync-based Explicit-time Description Method using rendezvous synchronization steps and the Semaphore-based Explicit-time Description Method using only one global variable were proposed; they both achieve better modularity than Lamport's method in modeling the real-time systems. In contrast to timed automata based model checkers like UPPAAL, explicit-time description methods can access and store the current time instant for future calculations necessary for many real-time systems, especially those with pre-emptive scheduling. However, the Tick process in the above three methods increments the time by one unit in each tick; the state spaces therefore grow relatively fast as the time parameters increase, a problem when the system's time period is relatively long. In this paper, we propose a more efficient method which enables the Tick process to leap multiple time units in one tick. Preliminary experimental results in a high performance computing environment show that this new method significantly reduces the state space and improves both the time and memory efficiency.http://arxiv.org/pdf/0912.2553v1 |
| spellingShingle | Hao Wang Wendy MacCaull An Efficient Explicit-time Description Method for Timed Model Checking Electronic Proceedings in Theoretical Computer Science |
| title | An Efficient Explicit-time Description Method for Timed Model Checking |
| title_full | An Efficient Explicit-time Description Method for Timed Model Checking |
| title_fullStr | An Efficient Explicit-time Description Method for Timed Model Checking |
| title_full_unstemmed | An Efficient Explicit-time Description Method for Timed Model Checking |
| title_short | An Efficient Explicit-time Description Method for Timed Model Checking |
| title_sort | efficient explicit time description method for timed model checking |
| url | http://arxiv.org/pdf/0912.2553v1 |
| work_keys_str_mv | AT haowang anefficientexplicittimedescriptionmethodfortimedmodelchecking AT wendymaccaull anefficientexplicittimedescriptionmethodfortimedmodelchecking AT haowang efficientexplicittimedescriptionmethodfortimedmodelchecking AT wendymaccaull efficientexplicittimedescriptionmethodfortimedmodelchecking |