Model checking software systems

1995 ◽  
Author(s):  
Jeannette M. Wing ◽  
Mandana Vaziri-Farahani
Keyword(s):  
Model Checking ◽  
Software Systems

scholarly journals A Quantitative Partial Model-Checking Function and Its Optimisation

10.29007/rb2p ◽  
2018 ◽  
Author(s):  
Stefano Bistarelli ◽  
Fabio Martinelli ◽  
Ilaria Matteucci ◽  
Francesco Santini
Keyword(s):  
Model Checking ◽  
Modal Logic ◽  
Algebraic Structure ◽  
Process Algebra ◽  
Software Systems ◽  
Efficient Tool ◽  
Combinatorial Explosion ◽  
Loosely Coupled ◽  
Partial Model ◽  
Final Score

Partial Model-Checking (PMC) is an efficient tool to reduce the combinatorial explosion of a state-space, arising in the verification of loosely-coupled software systems. At the same time, it is useful to consider quantitative temporal-modalities. This allows for checking whether satisfying such a desired modality is too costly, by comparing the final score consisting of how much the system spends to satisfy the policy, to a given threshold. We stir these two ingredients together in order to provide a Quantitative PMC function (QPMC), based on the algebraic structure of semirings. We design a method to extract part of the weight during QPMC, with the purpose to avoid the evaluation of a modality as soon as the threshold is crossed. Moreover, we extend classical heuristics to be quantitative, and we investigate the complexity of QPMC.Keyword: Partial Model Checking, Semirings, Optimisation, Quantitative Modal Logic Quantitative Process Algebra, Quantitative Evaluation of Systems.

scholarly journals Formal verification of dynamic hybrid systems: a NuSMV-based model checking approach

2018 ◽  
Vol 17 ◽  
pp. 03026 ◽  
Author(s):  
Zhi Xu ◽  
Deming Zhong ◽  
Weigang Li ◽  
Hao Huang ◽  
And Yigang Sun
Keyword(s):  
Model Checking ◽  
Security Analysis ◽  
Symbolic Model Checking ◽  
Software Systems ◽  
Symbolic Model ◽  
Counter Example ◽  
Simplifying Assumptions ◽  
Dynamic Hybrid ◽  
The Individual ◽  
Computational Part

Software security is an important and challenging research topic in developing dynamic hybrid embedded software systems. Ensuring the correct behavior of these systems is particularly difficult due to the interactions between the continuous subsystem and the discrete subsystem. Currently available security analysis methods for system risks have been limited, as they rely on manual inspections of the individual subsystems under simplifying assumptions. To improve this situation, a new approach is proposed that is based on the symbolic model checking tool NuSMV. A dual PID system is used as an example system, for which the logical part and the computational part of the system are modeled in a unified manner. Constraints are constructed on the controlled object, and a counter-example path is ultimately generated, indicating that the hybrid system can be analyzed by the model checking tool.

Model checking software systems

1995 ◽  
Vol 20 (4) ◽  
pp. 128-139 ◽  
Author(s):  
Jeannette M. Wing ◽  
Mandana Vaziri-Farahani
Keyword(s):  
Model Checking ◽  
Software Systems

A Platform for Analyzing Behaviors of Service-Oriented Application Based on the Probabilistic Model Checking

2015 ◽  
Vol 3 (2) ◽  
pp. 24-38 ◽  
Author(s):  
Jinyu Kai ◽  
Huaikou Miao ◽  
Kun Zhao ◽  
Jiaan Zhou ◽  
Honghao Gao
Keyword(s):  
Model Checking ◽  
Web Service ◽  
Probabilistic Model ◽  
Probabilistic Model Checking ◽  
Software Systems ◽  
Model Checker ◽  
System Behavior ◽  
Service Oriented ◽  
The Web ◽  
Oriented System

Service oriented software systems running in a highly open, dynamic and unpredictable Internet environment are inevitable to face all kinds of uncertainty. To monitor the operation of the web services system behavior analysis and analysis whether the system behavior is consistent with the requirements is the basis to determine whether the system needs to be reconfigured. In this paper, an analytical platform for the behavior of a web service-oriented system based on the probabilistic model checking is introduced which provides the basis for judging whether a system needs to be reconfigured by applying the approach of probabilistic model checking to verify whether the behavior system model is satisfied requirement properties. This platform is implemented in Java language and using the dot tool that the Graphviz provides and the PRISM model checker to construct the behavior model of the web service-oriented system based on web log files, to view and edit behavior models visually, and to convert the model from one form to another to make it convenience for users to use the model checker PRISM. Finally, we can judge whether the model is satisfied the desired requirements according to the verification result.

scholarly journals A case study in model checking software systems

1997 ◽  
Vol 28 (2-3) ◽  
pp. 273-299 ◽  
Author(s):  
Jeannette M. Wing ◽  
Mandana Vaziri-Farahani
Keyword(s):  
Model Checking ◽  
Software Systems

scholarly journals Towards Support for Software Model Checking: Improving the Efficiency of Formal Specifications

2011 ◽  
Vol 2011 ◽  
pp. 1-13 ◽  
Author(s):  
Salamah Salamah ◽  
Ann Q. Gates ◽  
Steve Roach ◽  
Matthew Engskow
Keyword(s):  
Model Checking ◽  
Spin Model ◽  
Software Systems ◽  
Formal Specifications ◽  
Model Checker ◽  
Software Model Checking ◽  
Software Model ◽  
Property Specification ◽  
Büchi Automaton ◽  
Spin Model Checker

The Property Specification (Prospec) tool uses patterns and scopes defined by Dwyer et al., to generate formal specifications in Linear Temporal Logic (LTL) and other languages. The work presented in this paper provides improved LTL specifications for patterns and scopes over those originally provided by Prospec. This improvement comes in the efficiency of the LTL formulas as measured in terms of the number of states in the Büchi automaton generated for the formula. Minimizing the size of the Büchi automata for an LTL specification provides a significant improvement for model checking software systems using such tools as the highly acclaimed Spin model checker.

Sign in / Sign up

Export Citation Format

Share Document