An Efficient Specification for System Verification

2006 ◽  
Vol 10 (6) ◽  
pp. 931-938
Author(s):  
Chikatoshi Yamada ◽  
◽  
Yasunori Nagata ◽  
Zensho Nakao ◽  
Keyword(s):  
Model Checking ◽  
Execution Time ◽  
Large Scale ◽  
Large Scale Systems ◽  
Computation Tree Logic ◽  
Computation Tree ◽  
Specification Method ◽  
System Verification ◽  
Temporal Formula ◽  
Temporal Specification

In design of complex and large scale systems, system verification has played an important role. In this article, we focus on specification process of model checking in system verifications. Modeled systems are in general specified by temporal formulas of computation tree logic, and users must know well about temporal specification because the specification might be complex. We propose a method by which specifications with temporal formulas are obtained inductively. We will show verification results using the proposed temporal formula specification method, and show that amount of memory, OBDD nodes, and execution time are reduced.

Inductive Temporal Formula Specifications for System Verification

2005 ◽  
Vol 9 (3) ◽  
pp. 321-328
Author(s):  
Chikatoshi Yamada ◽  
◽  
Yasunori Nagata ◽  
Zensho Nakao ◽  
Keyword(s):  
Model Checking ◽  
Complex Systems ◽  
Large Scale ◽  
Design Verification ◽  
Computation Tree Logic ◽  
Computation Tree ◽  
System Verification ◽  
Temporal Formula ◽  
Temporal Specification

Design verification has played an important role in the design of large scale and complex systems. In this article, we focus on model checking methods. Behaviors of modeled systems are in general specified by temporal formulas of computation tree logic, and users must know well about temporal specification because the specification might be complex. We propose a method temporal formulas are obtained inductively, and amounts of memory and time are reduced. We will show verification results using the proposed method.

Bounded Model Checking for Probabilistic Computation Tree Logic

2012 ◽  
Vol 23 (7) ◽  
pp. 1656-1668 ◽  
Author(s):  
Cong-Hua ZHOU ◽  
Zhi-Feng LIU ◽  
Chang-Da WANG
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
Probabilistic Computation ◽  
Computation Tree Logic ◽  
Computation Tree

Automatic Partitioning of Large Scale Simulation in Grid Computing for Run Time Reduction

2012 ◽  
pp. 225-252
Author(s):  
Nurcin Celik ◽  
Esfandyar Mazhari ◽  
John Canby ◽  
Omid Kazemi ◽  
Parag Sarfare ◽  
...  
Keyword(s):  
Execution Time ◽  
Large Scale ◽  
Time Synchronization ◽  
Computational Grid ◽  
Experimental Results ◽  
Time Interval ◽  
Computational Power ◽  
Large Scale Systems ◽  
Large Scale Simulations ◽  
Reduce Execution Time

Simulating large-scale systems usually entails exhaustive computational powers and lengthy execution times. The goal of this research is to reduce execution time of large-scale simulations without sacrificing their accuracy by partitioning a monolithic model into multiple pieces automatically and executing them in a distributed computing environment. While this partitioning allows us to distribute required computational power to multiple computers, it creates a new challenge of synchronizing the partitioned models. In this article, a partitioning methodology based on a modified Prim’s algorithm is proposed to minimize the overall simulation execution time considering 1) internal computation in each of the partitioned models and 2) time synchronization between them. In addition, the authors seek to find the most advantageous number of partitioned models from the monolithic model by evaluating the tradeoff between reduced computations vs. increased time synchronization requirements. In this article, epoch- based synchronization is employed to synchronize logical times of the partitioned simulations, where an appropriate time interval is determined based on the off-line simulation analyses. A computational grid framework is employed for execution of the simulations partitioned by the proposed methodology. The experimental results reveal that the proposed approach reduces simulation execution time significantly while maintaining the accuracy as compared with the monolithic simulation execution approach.

Automatic Partitioning of Large Scale Simulation in Grid Computing for Run Time Reduction

2010 ◽  
Vol 1 (2) ◽  
pp. 64-90 ◽  
Author(s):  
Nurcin Celik ◽  
Esfandyar Mazhari ◽  
John Canby ◽  
Omid Kazemi ◽  
Parag Sarfare ◽  
...  
Keyword(s):  
Execution Time ◽  
Large Scale ◽  
Time Synchronization ◽  
Computational Grid ◽  
Time Interval ◽  
Computational Power ◽  
Computing Environment ◽  
Large Scale Systems ◽  
Large Scale Simulations ◽  
Reduce Execution Time

Simulating large-scale systems usually entails exhaustive computational powers and lengthy execution times. The goal of this research is to reduce execution time of large-scale simulations without sacrificing their accuracy by partitioning a monolithic model into multiple pieces automatically and executing them in a distributed computing environment. While this partitioning allows us to distribute required computational power to multiple computers, it creates a new challenge of synchronizing the partitioned models. In this article, a partitioning methodology based on a modified Prim’s algorithm is proposed to minimize the overall simulation execution time considering 1) internal computation in each of the partitioned models and 2) time synchronization between them. In addition, the authors seek to find the most advantageous number of partitioned models from the monolithic model by evaluating the tradeoff between reduced computations vs. increased time synchronization requirements. In this article, epoch- based synchronization is employed to synchronize logical times of the partitioned simulations, where an appropriate time interval is determined based on the off-line simulation analyses. A computational grid framework is employed for execution of the simulations partitioned by the proposed methodology. The experimental results reveal that the proposed approach reduces simulation execution time significantly while maintaining the accuracy as compared with the monolithic simulation execution approach.

scholarly journals Incremental Construction of Counterexamples in Model Checking Web Documents

10.29007/c8jt ◽  
2018 ◽  
Author(s):  
Franz Weitl ◽  
Shin Nakajima
Keyword(s):  
Model Checking ◽  
Description Logic ◽  
Level Of Detail ◽  
Web Documents ◽  
Web Based ◽  
Computation Tree Logic ◽  
Computation Tree ◽  
Incremental Construction ◽  
Analysis Of Error

A new algorithm for incrementally generating counterexamples for the temporal description logic ALCCTL is presented. ALCCTL is a decidable combination of the description logic ALC and computation tree logic CTL that is expressive for content- and structure-related properties of web documents being verified by model checking. In the case of a specification violation, existing model checkers provide a single counterexample which may be large and complex. We extend existing algorithms for generating counterexamples in two ways. First, a coarse counterexample is generated initially that can be refined subsequently to the desired level of detail in an incremental manner. Second, the user can choose where and in which way a counterexample is refined. This enables the interactive step-by-step analysis of error scenarios according to the user's interest.We demonstrate in a case study on a web-based training document that the proposed approach reveals more errors and explains the cause of errors more precisely than the counterexamples of existing model checkers. In addition, we demonstrate that the proposed algorithm is sufficiently fast to enable smooth interaction even in the case of large documents.

Improved Checkpoint Using the Effective Management of I/O in a Cloud Environment

2019 ◽  
pp. 219-233
Author(s):  
Bakhta Meroufel ◽  
Ghalem Belalem
Keyword(s):  
Fault Tolerance ◽  
Execution Time ◽  
Large Scale ◽  
Fault Tolerant ◽  
Experimental Results ◽  
Cloud Environment ◽  
Large Scale Systems ◽  
Major Disadvantage ◽  
Reliability And Robustness ◽  
Effective Use

One of the most important points for more effective use in the environment of cloud is undoubtedly the study of reliability and robustness of services related to this environment. In this case, fault tolerance is necessary to ensure that reliability and reduce the SLA violation. Checkpointing is a popular fault tolerance technique in large-scale systems. However, its major disadvantage is the overhead caused by the storage time of checkpointing files, which increases the execution time and minimizes the possibility to meet the desired deadlines. In this chapter, the authors propose a checkpointing strategy with lightweight storage. The storage is provided by creating a virtual topology VRbIO and the use of an intelligent and fault tolerant I/O technique CSDS (collective and selective data sieving). The proposal is executed by active and reactive agents and it solves many problems of checkpointing with standard I/O. To evaluate the approach, the authors compare it with a checkpointing with ROMIO as I/O strategy. Experimental results show the effectiveness and reliability of the proposed approach.

Sign in / Sign up

Export Citation Format

Share Document